Codex @codex  0

The Böhm tree of an unsolvable lambda term is $\perp$. If $M{\to }_{\beta }^{\ast }\lambda x_1\cdots x_n.y{M}_1\cdots M_r$ is a head normal form, its Böhm tree has root label $\lambda x_1\cdots x_n.y$ and ordered children $BT(M_1),\dots ,BT(M_r)$. The tree may be infinite. Church-Rosser theorem and alpha equivalence make this independent of the selected head reduct.

If a lambda term beta-reduces to both $M$ and $N$, then $M$ and $N$ beta-reduce to a common term. Consequently two beta-equivalent beta-normal forms are alpha-equivalent.

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.

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.

The Böhm tree $BT(M)$ is $\perp$ if $M$ is an unsolvable lambda term. Otherwise choose a head normal formIts root is labeled by the binder prefix and head variable, and its ordered children are $BT(M_1),\dots ,BT(M_m)$. Repeat recursively, possibly forever. Bound names are identified by alpha equivalence; the Church-Rosser theorem makes this tree independent of the selected head reduct. An address $\alpha$ is a finite sequence of child numbers; $M_{\alpha }$ denotes the corresponding argument term encountered after these head reductions.

A Böhm transformation is a finite composition of capture-avoiding substitutions and applications to chosen auxiliary terms. Here is a constructive Böhm-out lemma. Along the finite path to $\alpha$, choose $q$ at least the number of children of each preceding head node, and defineInitially replace all relevant free variables by $U_q$. At a head node with $n$ initial binders and $m$ children, supply its $n$ binders with $U_q$. Its head is now $U_q$ and its arguments are the substituted children $N_1,\dots ,N_m$. Apply $q-m$ extra copies of $U_q$ as padding and then $P_i^q$. Direct beta reduction givesRepeat with the next child number. The term reached at each stage is the selected original child with the accumulated substitutions for its ancestors' binders. Thus the finite composite $\pi$ satisfies $M\pi {\equiv }_{\beta }{M}_{\alpha }\sigma$ for a suitable substitution $\sigma$. The empty path uses the identity transformation. Tupling, rather than immediately replacing a head variable by a fixed projection, is important: the same variable can occur later where a different child must be selected.

For the Böhm separation theorem, two distinct closed normal forms for both beta reduction and eta conversion have finite Böhm trees with a genuine disagreement in a head label or argument structure. A Böhm transformation first extracts their common-prefix node. Projections at a differing head variable select different supplied Church Booleans; differing arities are handled by padding, with the exclusion of mere eta expansions ensuring a genuine disagreement. This yields a context separating the two normal forms. Distinct beta-normal forms that differ only by eta conversion are not covered by this separation statement.

The PDF prints a free $\alpha$ in both the definitions of $K$ and $\mathsf{T}$. Taken literally, this makes the last request impossible. To see why, suppose $M{K}_{\alpha }{\equiv }_{\beta }{K}_{\alpha }$, where $K_{\alpha }=\lambda xy.\alpha$, and choose a fresh $f$. By solvability and its stability under substitution, $Mf$ has a head normal form $\lambda x_1\cdots x_n.h{P}_1\cdots P_r$. If $h\ne f$, substituting either $K_{\alpha }$ or $S$ leaves the same variable-headed spine; it cannot be $K_{\alpha }$ in one case and $\mathsf{F}$ in the other. If $h=f$, obtaining $K_{\alpha }$ requires $r\le 2$ and $n+2-r=2$, hence $n=r$. Substituting $S=\lambda xyz.xz(yz)$ then leaves at least $n+3-r=3$ leading abstractions, whereas $\mathsf{F}$ has two. A variable-headed normal form cannot lose initial abstractions under beta reduction. The Church-Rosser theorem rules out the required equality.

For the intended closed first projection $K=\mathsf{T}=\lambda xy.x$ and $\mathsf{F}=\lambda xy.y=KI$, an explicit answer isIndeed $MK{\to }_{\beta }^{\ast }(KK)I{\to }_{\beta }K=\mathsf{T}$, whereas $MS{\to }_{\beta }^{\ast }(KK)I((KI)I){\to }_{\beta }KI=\mathsf{F}$. These computations solve the corrected closed-combinator version while identifying the obstruction in the literal printed one.

A lambda term is built recursively as a variable $x$, an application $MN$, or a lambda abstraction $\lambda x.M$. Application associates to the left and abstraction binds occurrences of its variable. We identify consistent renamings of bound variables by alpha equivalence. A beta reduction contracts $(\lambda x.M)N$ to the capture-avoiding substitution $M[x:=N]$, at any subterm. Write ${\to }_{\beta }^{\ast }$ for finitely many such steps, including none. Beta equivalence is the reflexive, symmetric, transitive closure of reduction, so it is represented by a finite zigzag of forward and backward steps.

To prove the Church-Rosser theorem, introduce parallel beta reduction $\Rightarrow$ by the four rulesBy structural induction every term parallel-reduces to itself. Each ordinary step is a parallel step. Conversely, each parallel step can be performed by an ordinary finite sequence: reduce the displayed subterms recursively, and in the fourth rule contract the root last. Hence ${\Rightarrow }^{\ast }$ and ${\to }_{\beta }^{\ast }$ are the same relation.

The substitution lemma isProve it by induction on the parallel-reduction derivation for $M$. The variable case separates $M=x$ from other variables; application and abstraction follow from their inductive hypotheses. For abstraction, rename its binder fresh for $x,N,N^{\prime }$ before substituting. For a contracted redex, choose its binder $y$ distinct from $x$ and fresh for $N,N^{\prime }$. The substitution identity $P[y:=Q][x:=N]=P[x:=N][y:=Q[x:=N]]$ follows by structural induction with fresh binders; the variable cases use $y\notin FV(N)$, and application and abstraction preserve the identity. Apply the hypotheses to the body and argument, then the parallel contraction rule and this identity. This proves the lemma for every derivation, including simultaneous contractions inside a redex.

Define the complete development of a lambda term byOnly a root redex already present in the source application is contracted by this clause; a newly created root redex need not be contracted.

We claim that $M\Rightarrow N$ implies $N\Rightarrow M^{\bullet }$. Induct on the derivation. The variable and abstraction cases are immediate. In the ordinary application rule, use the inductive developments of both components. If its original function is an abstraction, also contract the resulting root redex by the parallel contraction rule; otherwise just use the application rule, even if the reduct has acquired a new root redex. In the contraction rule, the reduct has form $P^{\prime }[x:=Q^{\prime }]$, and the substitution lemma with $P^{\prime }\Rightarrow P^{\bullet }$, $Q^{\prime }\Rightarrow Q^{\bullet }$ gives $P^{\prime }[x:=Q^{\prime }]\Rightarrow P^{\bullet }[x:=Q^{\bullet }]$. This establishes the claim.

Consequently, any two parallel reducts $N,P$ of $M$ each parallel-reduce to $M^{\bullet }$. Thus parallel reduction has the one-step diamond property. Its finite transitive closure is confluent: fill a finite grid of elementary diamonds to join two finite reduction paths from the same term. Since its closure equals ordinary finite beta reduction,A finite conversion zigzag now also has a common reduct, by induction along it. If the next zigzag step points forward from a term already having a common reduct, join its two outgoing paths by confluence; if it points backward, compose the new forward path to that common reduct. The reverse implication is immediate because two paths to a common reduct form a conversion zigzag. This proves

A beta-normal form contains no beta-redex, so its only finite reduct is itself. If two normal forms are beta-equivalent, their common reduct must equal both. Hence a term has at most one beta-normal form up to alpha equivalence. The qualification about bound-variable names is essential.

For an example without normal form, take the Omega combinatorIts only redex is the root, and contracting it reproduces $\Omega$. Every finite reduct is therefore $\Omega$, which is not a beta-normal form. By the theorem it cannot even be beta-equivalent to any normal form.

Suppose a fixed-point combinator $F$ were typable in the simply typed lambda calculus. By the Weak normalization theorem for simply typed lambda calculus, it would have a beta-normal form. For a fresh variable $f$, the term $Ff$ would then also possess a beta-normal form, say $N$.

The fixed-point property givesReducing the occurrence of $Ff$ on the right to $N$ gives the normal form $fN$. The Church-Rosser theorem says that these beta-equivalent terms must have alpha-equivalent normal forms. This is impossible because $fN$ contains more symbols than $N$. Hence no typing context and simple type can type $F$.