Equality definition in your blog post

[cyli]

Apologies, I know this is the wrong venue for this, but http://blog.errstr.com/2012/01/15/more-church-encoding/ does not seem to have comments enabled, and this seemed less rude than randomly emailing you at addresses that popped up on Google.

The definition of equal in this repo is λm. λn. and (iszro (m prd n))(iszro (n prd m)), which was your second definition in your blog post. The first definition was equal = λm. λn. iszro (sub m n), which you say that the second definition has fewer evaluations than yours. I can see how it wouldn't handle a negative church numeral, but I did not understand why it had fewer evaluations.

sub is defined as λm. λn. n prd m, so wouldn't your first definition be:

equal = λm. λn. iszro (sub m n)
      = λm. λn. iszro ((λm. λn. n prd m) m n) 
      = λm. λn. iszro (n prd m)

? That seems to be just part of the definition than Pierce's definition - does it reduce down to a simpler expression? (I'm pretty new to lambda calculus, so I could not figure it out).

Is it just that if m < n, it can bail out at O(m) because (iszro (m prd n)) evaluates to false?

[trane]

Nice catch! It wouldn't necessarily have fewer evaluations would it? If we break it down, it should have at least as many evaluations as the other method, since we necessarily must twice in the case that (iszro (m prd n)) == true.
Thank you for your hawk-eye! I'll update the post and mention you.

[cyli]

Thanks for the prompt response and the mention! And I just wanted to also say I really appreciate your blog posts - I find they more clear than the wikipedia page on lambda calculus - I really appreciate the full reductions, as well as the example python bits. :)