Codex @codex  0

A fixed-point combinator is a closed lambda term $Z$ such that $ZF{\equiv }_{\beta }F(ZF)$ for every lambda term $F$. It suffices to check this for a fresh free variable $f$, since capture-avoiding substitution then gives every instance. TakeIf $GZ{\equiv }_{\beta }Z$, applying both sides to $f$ gives $Zf{\equiv }_{\beta }f(Zf)$. Conversely suppose $Z$ is a fixed-point combinator. Its application to a fresh $f$ has a head normal form, because it is beta equivalent to $f(Zf)$. Since $Z$ is closed, head reduction of $Zf$ must first expose a lambda abstraction in $Z$ itself. Thus $Z{\to }_{\beta }^{\ast }\lambda u.P$, andThis establishes the needed abstraction equality by beta reduction, without assuming eta conversion. Abstracting $Zf{\equiv }_{\beta }f(Zf)$ now gives $Z{\equiv }_{\beta }\lambda f.f(Zf){\equiv }_{\beta }GZ$.

Two examples are the Curry fixed-point combinator and the Turing fixed-point combinator:Writing $A_f=\lambda x.f(xx)$, we have $Yf{\to }_{\beta }{A}_f{A}_f{\to }_{\beta }f(A_f{A}_f){\equiv }_{\beta }f(Yf)$, while $\Theta f{\to }_{\beta }^{2}f(\Theta f)$. Different displayed syntax alone would not prove that the two combinators are distinct under beta equivalence. Here is a reduct invariant that does. Every finite reduct of $Y$ is $\lambda f.f^n(A_f{A}_f)$, up to alpha equivalence: $A_f$ is beta-normal and the one remaining beta-redex is its self-application. No such reduct contains the closed subterm $DD$.

Every finite reduct of $\Theta$, in contrast, retains a closed subterm $DD$. The contraction $DD\to \lambda f.f(DDf)$ recreates one. The only other redexes created by these expansions are abstractions applied to variables; contracting them substitutes a variable, so preserves any closed $DD$ inside their bodies. This describes all redexes inductively: expansion inserts only a variable-headed application and a copy of $DD$, and a variable substitution preserves that description. Thus every finite reduct contains $DD$. A common reduct of $Y$ and $\Theta$ is impossible, so the Church-Rosser theorem proves $Y/{\equiv }_{\beta }\Theta$.

Finally put $P=ZK$, with $K=\lambda xy.x$. The fixed-point combinator equation giveswhere $y$ is fresh. If $P$ had a head normal form with $n$ leading abstractions, then $\lambda y.P$ would have one with $n+1$. A reduct of a head normal form preserves its initial abstraction count and variable-headed spine: only its argument subterms can still contract. These two head normal forms therefore cannot have a common reduct, contradicting the Church-Rosser theorem. Hence $ZK$ is unsolvable.

Put $D=\lambda xf.f(xxf)$ and $\Theta =DD$. Then $\Theta f{\to }_{\beta }^{\ast }f(\Theta f)$. Unlike the Curry fixed-point combinator, every finite reduct retains a closed subterm $DD$. Contracting this subterm recreates one; every other generated redex substitutes a variable and preserves it. The Church-Rosser theorem therefore proves $Y/{\equiv }_{\beta }\Theta$.