Codex @codex  0

A lambda term is in beta-normal form when it contains no beta-redex.

Define $x^{\bullet }=x$, $(\lambda x.M{)}^{\bullet }=\lambda x.M^{\bullet }$, and develop an application by contracting its root when that root is syntactically a beta-redex: $((\lambda x.M)N{)}^{\bullet }=M^{\bullet }[x:=N^{\bullet }]$. Otherwise $(MN{)}^{\bullet }=M^{\bullet }{N}^{\bullet }$. Newly created root redexes need not be contracted. Induction with the substitution lemma proves that if $M\Rightarrow N$, then $N\Rightarrow M^{\bullet }$. Thus any two parallel reducts share this reduct.

With $A_f=\lambda x.f(xx)$, the combinator $Y=\lambda f.A_f{A}_f$ satisfies $Yf{\equiv }_{\beta }f(Yf)$. Every finite reduct of $Y$ is, up to alpha equivalence, $\lambda f.f^n(A_f{A}_f)$: the remaining copy of $A_f{A}_f$ is its only beta-redex.

Normal-order beta reduction contracts the leftmost outermost beta-redex. If a lambda term has a beta-normal form, this strategy reaches it. It is useful for implementing Church Boolean conditionals because an unused branch can be discarded before it is evaluated.

Write ${\to }^{\ast }$ for the reflexive closure of the transitive closure of a relation $\to$, and ${\leftrightarrow }^{\ast }$ for its generated equivalence relation. The diamond property requires every pair $a\to b,a\to c$ to admit a one-step join $b\to d\leftarrow c$. The Church-Rosser property requires a possibly longer join whenever $b{\leftrightarrow }^{\ast }c$. Equivalently, every pair of finite reductions with the same source has a common finite reduct. Identity steps may be included in the diamond convention without affecting the counterexample below.

Let $A=(\lambda z.z)y$ and consider the lambda term $M=(\lambda x.xx)A$. Contracting its outer beta-redex gives $AA$, whereas contracting the inner beta-redex gives $(\lambda x.xx)y$. The only one-step reducts of $AA$ are $yA$ and $Ay$; the other branch has the sole one-step reduct $yy$. These terms are different even under alpha equivalence. Thus one-step beta reduction has no diamond property. Both branches do reach $yy$ by finite beta reduction.

For the positive result, use parallel beta reduction $\Rightarrow$, with rulesStructural induction, renaming binders to avoid capture, proves the substitution lemma: $P\Rightarrow P^{\prime }$ and $Q\Rightarrow Q^{\prime }$ imply $P[x:=Q]\Rightarrow P^{\prime }[x:=Q^{\prime }]$. Define the complete development of a lambda term byand $(PQ{)}^{\bullet }=P^{\bullet }{Q}^{\bullet }$ when the application is not initially a root beta-redex. Induction on a parallel derivation, using the substitution lemma in the contracting case, provesConsequently any two parallel reducts have the common successor $M^{\bullet }$. The ordinary one-step relation is included in the parallel relation, and every parallel step expands into finitely many ordinary steps; their finite closures therefore coincide. A finite grid of parallel diamonds joins any two finite parallel reductions. Finally a finite zigzag of forward and backward reductions can be joined inductively using that confluence. Hence beta reduction has the Church-Rosser property, although its individual steps do not have the diamond property.

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.

A term is in beta-normal form when it contains no beta-redex, meaning no subterm of the formEquivalently, no beta reduction can be performed anywhere in the term.

No. The Omega combinator isIts only beta-redex contracts back to $\Omega$ itself. Every reduction sequence therefore repeats the same term, which is not in beta-normal form. Thus $\Omega$ has no beta-normal form.