Untyped lambda calculus

The untyped lambda calculus forms terms from variables, abstraction, and application without assigning types.

Eta conversion expresses extensionality for a lambda abstraction whose fresh argument is only passed to a function. The side condition prevents removal of a genuine dependency. In a categorical model with $D\cong D^D$, the inverse laws for currying and evaluation validate this conversion as well as beta reduction.

Combinatory logic describes computation by application and fixed combinator constants, eliminating bound variables through bracket abstraction. Its intensional weak reduction does not identify every pair of terms that becomes beta-equivalent after translation into lambda calculus.

Bracket abstraction removes a free variable from a combinatory logic term. The displayed clauses are applied in that order, giving $FV([x]T)=FV(T)\setminus \{x\}$ and $([x]T)A{\to }^{\ast }T[x:=A]$. Under the standard lambda expansions of $S,K,I$, the result is beta-equivalent to $\lambda x.T$. The recursive translation of lambda terms therefore preserves variables and application and reflects weak equivalence, but need not preserve all beta equivalences.

A finite applicative expression over free variables and the combinator constants $S,K,I$, with application associating to the left. One may instead take $I$ as the abbreviation $SKK$. There is no variable binder in this syntax.

Weak combinatory reduction closes the displayed contractions under application contexts. Weak equivalence is its reflexive, symmetric, transitive closure. The adjective distinguishes this syntactic reduction from an extensional rule equating functions that agree after an extra argument. A weak normal form has no subexpression matching a contraction rule; a partially applied combinator can be such a normal form.

A lambda term has head normal form when it beta-reduces to a term $\lambda x_1\cdots x_k.y{M}_1\cdots M_r$ with a variable $y$ at the head. The argument terms need not be in beta-normal form. A term with no head normal form cannot be beta-equivalent to a Church numeral.

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.

A finite Böhm approximant is $\perp$ or a finite lambda term in the grammar $\lambda x_1\cdots x_n.y{A}_1\cdots A_r$, obtained by pruning a Böhm tree. Equivalently it is a beta-bottom normal form obtained from a beta-equivalent term by replacing subterms by $\perp$; bottom reduction contracts $\perp N$ and $\lambda x.\perp$ to $\perp$. Its interpretation in the graph model of lambda calculus is included in that of the original term.

A Böhm transformation is a finite composition of capture-avoiding substitutions and lambda applications to chosen auxiliary terms. It can extract a finite-address subtree of a Böhm tree as a substitution instance of the corresponding argument term.

For a finite path in a Böhm tree, choose $q$ at least the head arity at every preceding node. Replace relevant variables by $U_q=\lambda z_1\cdots z_{q}w.w{z}_1\cdots z_q$. After exposing each node, supply its initial bound variables with $U_q$, pad its $m$ arguments to $q$, and apply the projection $\lambda z_1\cdots z_q.z_i$ selecting the next child. Each step returns that child with accumulated substitutions, so iteration reaches a substitution instance of the chosen subtree. Tupling preserves all children until selection, even when the same variable occurs at several nodes.

Two distinct closed lambda terms in normal form for both beta reduction and eta conversion admit a separating context that maps them respectively to the two Church Booleans. Finite Böhm trees and the Böhm-out lemma isolate their first genuine head disagreement. The qualification about eta conversion matters: distinct beta-normal forms that are eta-equivalent cannot be separated this way.

An unsolvable lambda term has no head normal form, equivalently it is not a solvable lambda term. Capture-avoiding substitution and lambda application preserve unsolvability: until a head variable appears, head contractions proceed within the original term and cannot inspect the supplied terms.

A closed lambda term $E$ is easy if adjoining $E=M$ to the equations of beta equivalence remains nontrivial for every closed lambda term $M$. If $E$ is easy, then $ET$ is easy for every closed $T$: use the consistent equation $E=\lambda x.M$ to obtain $ET=M$. Since $I$ is not easy and solvability produces $I$ by applications, easy terms are unsolvable. The converse need not hold.

A lambda term is solvable if its closure by lambda abstractions over its free variables can be applied to finitely many closed lambda terms to obtain $I=\lambda x.x$ in beta equivalence. This is equivalent to having a head normal form. A head variable in a head normal form can be replaced by a projection returning $I$; conversely standardization theorem for beta reduction traces any successful head computation back to a head variable of the original term.

Beta reduction performs capture-avoiding substitution:

A reduction relation $\to$ has the diamond property if $a\to b$ and $a\to c$ imply a common one-step successor $b\to d\leftarrow c$. For relations allowing an identity step, the same definition includes zero-length joins. A finite grid of these diamonds proves confluence of ${\to }^{\ast }$. Ordinary one-step beta reduction fails this property because contracting before duplication can save two separate contractions.

A reduction relation has the Church-Rosser property when its equivalence relation generated by forward and backward steps satisfies $b{\leftrightarrow }^{\ast }c\Rightarrow \exists d(b{\to }^{\ast }d{\leftarrow }^{\ast }c)$. It is equivalent to confluence of ${\to }^{\ast }$. The Church-Rosser theorem establishes it for beta reduction.

Parallel beta reduction permits simultaneous reduction in the body of a lambda abstraction and both sides of an application, together with $(\lambda x.M)N\Rightarrow M^{\prime }[x:=N^{\prime }]$ when $M\Rightarrow M^{\prime }$ and $N\Rightarrow N^{\prime }$. Variables reduce to themselves. Its capture-avoiding substitution lemma is $M\Rightarrow M^{\prime },N\Rightarrow N^{\prime }\Rightarrow M[x:=N]\Rightarrow M^{\prime }[x:=N^{\prime }]$. Its transitive closure equals ordinary finite beta reduction, while its one-step diamond property yields the Church-Rosser theorem.

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.

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.

A finite beta reduction can be rearranged into standard order, contracting earlier residual redexes before later ones. In particular, a lambda term with a head normal form reaches one by head reduction, and a term with a beta-normal form reaches it by normal-order beta reduction. Head reduction contracts the outermost redex on the left application spine, including under initial lambda abstractions.

If an untyped lambda term has a beta-normal form, leftmost outermost beta reduction reaches a normal form. Thus an infinite normal-order computation certifies the absence of a beta-normal form. This is the normalization result needed to make a lambda simulation respect undefined outputs.

Capture-avoiding substitution $M[x:=N]$ replaces the free occurrences of $x$ in $M$ by $N$, renaming bound variables when necessary so that free variables of $N$ do not become bound.

Beta equivalence is the smallest equivalence relation containing beta reduction; equivalently, $M{\equiv }_{\beta }N$ when a finite sequence of beta reductions and reversed beta reductions connects $M$ and $N$.

Beta equivalence is semidecidable: enumerate finite conversion proofs. It is not decidable. A proposed total numeral-valued classifier of two nonempty disjoint beta equivalence classes can be reversed by a Church Boolean selector; a self-quoting fixed point of this reversal then belongs to the opposite class from the classifier output.

A beta-redex is a subterm of the form $(\lambda x.M)N$, to which beta reduction can be applied.

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

A combinator is a lambda term with no free variables.

The omega combinator is the divergent untyped lambda calculus termwhose only beta reduction reproduces $\Omega$.

An untyped lambda term $Y$ is a fixed-point combinator when $Yf{\equiv }_{\beta }f(Yf)$ for every term $f$.

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

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.

Every lambda term $F$ has a fixed point: the termsatisfies $X{\equiv }_{\beta }F(X)$. Equivalently, a fixed-point combinator such assatisfies $YF{\equiv }_{\beta }F(YF)$ for every $F$.

The set of fixed-point combinators is recursively enumerable. Enumerate closed lambda terms and finite proofs of beta equivalence, and output $Y$ whenever a proof of $Yf{\equiv }_{\beta }f(Yf)$ appears for a fresh variable $f$.