I was trying to develop an alternative to the Church encoding for the predecessor function for Church numerals. What I came up with was:
$$pred := λn.first (n (λp.second (p)(pair (succ (first (p))) true) (pair (0 )(true))) (pair (0 )(false))) $$which uses the terms used on the wikipedia site for Church Encodings. Now to check if my algorithm was working or not, I used this site. The test that I run was $(pred)(2)$. I tried beta and delta reduction in 2 different ways: first I simply passed the term on the website, and ran it. The $\beta$-normal form that I got was: $$\lambda{f}. \lambda{x}.fx$$ which was all right, since that was what the Church numeral for $1$ should look like. However, I also tried it in a different way.
First I ran just $pred$ on the website and copied the $\beta$-normal form. Let what I copied be $c$. Then I ran $(c)(2)$. The final result I got was: $$\lambda{f}. \lambda{x}.f(\lambda{x}.x)$$ Since $c$ and $pred$ are equivalent terms, the final $\beta$-normal forms should also be equivalent. However, it can be clearly seen that there is naming-clash problem in the second output. Can it be that the website is facing problems with $\alpha$ conversions? So, my question is whether $\lambda{f}. \lambda{x}.fx$ and $\lambda{f}. \lambda{x}.f(\lambda{x}.x)$ are equivalent. Actually to me they don’t appear to be, but according to the website, they should be. Can there be a glitch on the website, or is it in my reasoning?
Best Answer
As was mentioned in a comment, they are not equivalent lambda terms.
The way you can tell this is that both are in (β) normal form, and they are not α-equivalent. Normal forms of lambda terms are unique if they exist, so there cannot be a sequence of β conversions that relates these two different normal forms.