<p>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.</p>

<p>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$.</p>

<p>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).</p>

<p><em>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.</em></p>

<p>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$.</p>

<p><em>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.</em></p>

<p>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$.</p>

<hr>

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

<p>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$.</p>

<p>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.</p>

<p>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$.</p>

<p>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$.</p>

CC BY-SA 3.0
2011-11-20T17:10:51.107Z
2011-11-20T17:10:51.107Z
Gilles 'SO- stop being evil'
<p>In my continuing quest to try to learn lambda calculus, Hindley &amp; Seldin's "Lambda-Calculus and Combinators an Introduction" mentions the following <a href="http://www.google.com/url?sa=t&amp;rct=j&amp;q=&amp;esrc=s&amp;source=web&amp;cd=1&amp;ved=0CB4QFjAA&amp;url=http%3A%2F%2Fprojecteuclid.org%2FDPubS%2FRepository%2F1.0%2FDisseminate%3Fhandle%3Deuclid.ndjfl%2F1093887539%26view%3Dbody%26content-type%3Dpdf_1&amp;ei=v_3ITvbRA8jy0gGW1LQs&amp;usg=AFQjCNFIVn8CNnq7e9GBZpcYZw2zJjXeOw&amp;sig2=CXacHISl76Tizw7zQ5FzPQ">paper (by Bruce Lercher)</a> which proves that the only reducible expression that is the same (modulo alpha conversion) to itself is: $(\lambda x.xx)(\lambda x.xx)$.</p>

<p>While I believe the result, I do not follow the argument at all.</p>

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

<p>Thanks,</p>

<p>Charlie</p>

<lo.logic><lambda-calculus>
Lambda-Calculus terms that reduce to themselves
Charles R
# Lambda-Calculus terms that reduce to themselves

(Asked by: username_0 on 2011-11-20)

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)](http://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&ved=0CB4QFjAA&url=http%3A%2F%2Fprojecteuclid.org%2FDPubS%2FRepository%2F1.0%2FDisseminate%3Fhandle%3Deuclid.ndjfl%2F1093887539%26view%3Dbody%26content-type%3Dpdf_1&ei=v_3ITvbRA8jy0gGW1LQs&usg=AFQjCNFIVn8CNnq7e9GBZpcYZw2zJjXeOw&sig2=CXacHISl76Tizw7zQ5FzPQ) 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.

Thanks,

Charlie

**Tags:** lo.logic, lambda-calculus


---

## 1 answers

### Answer by username_1 on 2011-11-20. Score: 16

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$.


---

