2

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?

Soham Saha
  • 1,204
  • They are not (α, β, ...)-equivalent. – sparusaurata Oct 02 '23 at 13:38
  • 1
    For example, if you apply the two terms with $f$ being the identity function and $x$ being the Church numeral zero, then the first gives the Church numeral zero, while the second gives the Church numeral one. – Daniel Schepler Oct 02 '23 at 14:51
  • @DanielSchepler That was exactly my problem. Then the website must be malfunctioning. Is it common for lambda calculus simplifiers to do so? – Soham Saha Oct 02 '23 at 15:39
  • Hmm, when I tried what you said for the second one, I got $\lambda f.\lambda x. f x$ in the end. (I did get the incorrect answer if I just entered the reduction of your term as it appeared; but after inserting some spaces, in particular in f x, that fixed the issue.) – Daniel Schepler Oct 02 '23 at 16:35
  • @DanielSchepler yes, tried what you said. It seems that there may be some error when the software places the hidden parenthesis. Also, is it valid for a lambda term to contain two bound and binding variables with the same name? As in $\lambda{f}. \lambda{x}.f(\lambda{x}.x)$ – Soham Saha Oct 02 '23 at 16:58
  • @DanielSchepler could you suggest any website which is less prone to these kinds of errors? Till now I have settled on using javascript for it, as in http://tpcg.io/_S8BWHF – Soham Saha Oct 02 '23 at 16:59
  • 1
    It's usually considered valid (though it's generally discouraged in manually written lambda calculus terms, as "variable shadowing"). – Daniel Schepler Oct 02 '23 at 17:01
  • I'm still convinced the website you gave has at most presentation issues, in producing terms that smash together variables, whereas in entering the same term you need to separate the variables from each other or it will interpret it them as a single term. – Daniel Schepler Oct 02 '23 at 17:09
  • @DanielSchepler Let us continue this discussion in chat. – Soham Saha Oct 02 '23 at 17:09

1 Answers1

1

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.

Dan Doel
  • 3,715
  • That was exactly my problem. Then the website must be malfunctioning. Is it common for lambda calculus simplifiers to do so? – Soham Saha Oct 02 '23 at 15:38
  • I'm not familiar with the web site you're pointing to. Assuming they're using named variables and α conversion, it is very common for such implementations to contain errors. But, I don't actually know what the website is doing, or whether it has problems. – Dan Doel Oct 02 '23 at 17:36
  • Could you suggest some other online website suitable for simplifying lambda terms? As of now I am using javascript for the it. – Soham Saha Oct 02 '23 at 18:09