Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

In my continuing quest to try to learn lambda calculus, Hindley & Seldin's "Lambda-Calculus and Combinators an Introduction" mentions the following paper (by Bruce Lercher) which proves that the only reducible expression that is the same (modulo alpha conversion) to itself is: $(\lambda x.xx)(\lambda x.xx)$.

While I believe the result, I do not follow the argument at all.

It is quite short (less than one paragraph). Any explanations would be most welcome.



share|cite|improve this question

First, note that the result states that the only beta redex where the right-hand side is equal (modulo alpha-conversion) to the left-hand side is $(\lambda x. x x) (\lambda x. x x)$. There are other terms that reduce to themselves, having this redex in a context.

I can see how most of Lercher's proof work, though there are points where I can't get past without modifying the proof slightly. Suppose that $(\lambda x. A) B = [B/x] A$ (I use $=$ for alpha equivalence), and as per the variable convention suppose that $x$ does not occur free in $B$.

Count the number of $\lambda$'s in the left-hand side and the right-hand side. The reduction removes one from the redex, plus those of $B$, and adds as many as there are in $B$ times the number of occurrences of $x$ in $A$. In other words, if $L(M)$ is the number of $\lambda$'s in $M$ and $\#_x(M)$ is the number of free occurrences of $x$ in $M$ then $1 + L(B) = \#_x(A) \times L(B)$. The only solution to that Diophantine equation is $\#_x(A) = 2$ (and $L(B)=1$ but we won't use that fact).

I don't understand Lercher's argument for the paragraph above. He counts the number of $\lambda$'s and atomic terms; let's write this $\#(M)$. The equation is $\#(B) + 1 = \#_x(A) \times (\#(B) - 1)$, which has two solutions: $\#_x(A)=2, \#(B)=3$ and $\#_x(A)=3, \#(B)=2$. I don't see an obvious way to eliminate the second possibility.

Let us now apply the same reasoning to the number of subterms equal to $B$ on both sides. The reduction removes one near the top, and adds as many as there are substituted occurrences of $x$ in $A$, i.e. 2. Hence one more occurrence of $B$ must disappear; since the ones in $A$ remain (because $B$ contains no free $x$), the extra occurrence of $B$ on the left-hand side must be $\lambda x. A$.

I don't understand how Lercher deduces that $A$ does not have $B$ as a subterm, but this is not in fact relevant for the proof.

From the initial hypothesis, $[(\lambda x. A)/x] A$ is an application. This cannot be the case if $A = x$, therefore $A$ itself is an application $M N$, with $\lambda x.M N = [(\lambda x. M N)/x] M = [(\lambda x. M N)/x] N$. Since $M$ can't have itself as a subterm, $M$ cannot have the form $\lambda x.P$, so $M = x$. Similarly, $N = x$.

I prefer a proof with no counting arguments. Suppose that $(\lambda x. A) B = [B/x] A$.

If $A = x$ then we have $(\lambda x. A) B = B$, which is not possible since $B$ cannot be a subterm of itself. Thus, since the right-hand side of the hypothesis is equal to an application, $A$ must be an application $A_1 A_2$, and $\lambda x. A = [B/x] A_1$ and $B = [B/x] A_2$.

From the former equality, either $A_1 = x$ or $A_1 = \lambda x. [B/x] A$. In the second case, $A_1 = \lambda x. (\lambda x. A_1 A_2) B$, which is not possible since $A_1 cannot be a subterm of itself.

From the latter equality, either $A_2 = x$ or $A_2$ has no free $x$ (otherwise $B$ would be a subterm of itself). In the latter case, $A_2 = B$.

We have shown that $A = x x$. The right-hand side of the initial hypothesis is thus $B B$, and $B = \lambda x. A$ = $\lambda x. x x$.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.