Lambda calculus ($\lambda$-calculus)

Lambda calculus forms terms from variables, abstraction, and application, and computes by substitution.

A lambda model interprets variables, lambda application and lambda abstraction so that capture-avoiding substitution agrees with environments and all beta equivalence equations hold. A reflexive domain gives such an interpretation. Validity of eta conversion requires an extra inverse law and does not follow merely from a retraction.

A pointed complete partial order $D$ is reflexive when there are Scott continuous maps $e:[D\to D]\to D$ and $p:D\to [D\to D]$ with $p\circ e=\mathrm{id}$. Define $a\cdot b=p(a)(b)$ and interpret lambda abstraction using $e$. The inverse law gives beta soundness; $e\circ p=\mathrm{id}$ additionally gives eta soundness.

Let $P\omega =\mathcal{P}(\mathbb{N})$ ordered by subset. Encode a finite subset $u$ and output $n$ by a natural number $⟨u,n⟩$. Define $a\cdot b=\{n:\exists u\subseteq b\text{ finite},⟨u,n⟩\in a\}$ and $e(f)=\{⟨u,n⟩:n\in f(u)\}$. Every Scott continuous map satisfies $f(b)={\bigcup }_{u\subseteq b\text{ finite}}f(u)$, proving that application is the projection of a retraction. Lambda abstraction has graph $\{⟨u,n⟩:n\in [[M{]]}_{\rho [x:=u]}\}$.

The interpretation of a lambda term in the graph model of lambda calculus is the union of the interpretations of all its finite Böhm approximants. Every finite indexed interpretation reduces monotonically to an indexed normal approximant. Taking the union over all occurrence indices gives one inclusion; replacing subterms by bottom and using beta soundness gives the other. This identifies denotational information with finite observable parts of a Böhm tree.

An indexed lambda term assigns a natural number to every subterm occurrence; one also admits a constant $\perp$ with empty interpretation. In the graph model of lambda calculus, every syntax constructor is interpreted as usual and then intersected with $\{0,\dots ,n\}$ at its occurrence index $n$. All indexed interpretations are finite subsets of the unindexed interpretation, and their directed union recovers that interpretation.

Use the binary finite-set encoding $e_k$ and Cantor code $⟨k,t⟩$. Contracting $(\lambda x.P^n{)}^{m+1}{Q}^p$ gives the substituted body with its root index lowered by taking the minimum with $\min (m,n)$, replacing each occurrence $x^r$ by a copy of $Q$ with root index $\min (m,p,r)$. A zero-indexed abstraction instead substitutes $\perp$ and gives the body root index zero. Indices strictly budget the argument information that can be used by application. Finite-witness inequalities for the pairing code prove that indexed reduction increases the interpretation, although it can decrease the underlying Böhm tree.

A lambda term is a variable, an abstraction $\lambda x.M$, or an application $MN$, formed recursively from lambda terms $M$ and $N$.

Application $MN$ applies the lambda term $M$ to the lambda term $N$. It associates to the left: $MNP=(MN)P$. Together with variables and lambda abstraction, it generates all lambda terms.

A lambda abstraction $\lambda x.t$ binds the variable $x$ in the lambda term $t$. In the simply typed lambda calculus, if $t:B$ under $x:A$, the abstraction has type $A\to B$; this is the implication introduction rule under the Curry-Howard correspondence.

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

Two lambda terms are alpha-equivalent when they differ only by consistent renaming of bound variables.

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.

The simply typed lambda calculus assigns arrow types to variables, abstractions, and applications according to syntax-directed typing rules.

A typed lambda term carries a type derivation under a context of typed free variables. The rules for variables, abstraction, and application correspond to assumptions, the implication introduction rule, and the implication elimination rule under the Implicational Curry-Howard correspondence. General fixed-point combinators belong to the untyped lambda calculus; self-application cannot be given a finite simple type.

Every well-typed term in the simply typed lambda calculus has some finite beta-reduction sequence ending in a beta-normal form.

Church encoding represents data and operations as terms of the lambda calculus. A Church numeral represents a natural number by repeated function application; a Church Boolean selects one of two arguments.

The Church numeral $c_n=\lambda f.\lambda x.f^{n}x$ encodes the natural number $n$ by iteration.

Church numeral successor, addition, multiplication, and exponentiation are represented by $\lambda nfx.f(nfx)$, $\lambda mnfx.mf(nfx)$, $\lambda mnfx.m(nf)x$, and $\lambda mnfx.(nm)fx$. The last term takes the base first and the exponent second. Its outer abstractions preserve the usual numeral normal form at exponent zero, implementing $m^0=1$, including $0^0=1$. At base type $A$, exponentiation uses an exponent at Church type $C_{A\to A}$ and a base at $C_A=(A\to A)\to A\to A$.

The lambda termreturns the Church Boolean $\mathsf{T}$ on $c_0$ and $\mathsf{F}$ on every positive Church numeral. Zero iterations leave the initial true value, while at least one iteration replaces it by false. Normal-order beta reduction evaluates a numeral conditional without evaluating an unchosen branch.

With the Church Booleans $\mathsf{T}=\lambda ab.a$ and $\mathsf{F}=\lambda ab.b$, encode a pair byThen $\mathsf{Fst}(\mathsf{Pair}AB){\to }_{\beta }^{\ast }A$ and the second projection similarly returns $B$. Pairing an iteration counter with a computed value implements primitive recursion using only Church numeral iteration.

A function $g:{\mathbb{N}}^k\to \mathbb{N}$ is lambda-definable when some combinator $G$ satisfiesfor every tuple of natural numbers.

The successor function is lambda-defined on Church numerals bybecause $\mathrm{Succ}{c}_n{\equiv }_{\beta }{c}_{n+1}$.

Using a fixed-point combinator, Church Boolean conditionals, a zero test, and a predecessor term, lambda-definable $g$ and $h$ giveNormal-order beta reduction evaluates only the selected conditional branch, so this term implements primitive recursion on Church numerals.

If total functions $g$ and $h$ are represented by lambda terms $G,H$, defineandAfter $j$ iterations the Church pair holds $(c_j,c_{f(\mathbf{x},j)})$, proved by mathematical induction using the defining recursion equations. Consequently $R$ represents the total primitive recursive function $f$. This statement concerns total inputs and total recursion constituents; it is not an unguarded composition theorem for arbitrary partial functions.

A partial function is lambda-definable when one lambda term maps Church numerals in its domain to the numeral of the output and produces no numeral on inputs outside its domain.

Every partial computable function is represented on Church numerals by a closed untyped lambda calculus term. First represent all primitive recursive functions using zero, successor, projections, composition and lambda definition of primitive recursion by pair iteration. Apply the Kleene normal form theorem and search successive history codes with a fixed-point combinator. Test the represented total predicate using a Church numeral zero test; return the decoded output only on the true branch. If no history passes, normal-order head reduction continues the search indefinitely and the term has no head normal form, so cannot be in beta equivalence with a Church numeral. This avoids the incorrect assumption that a lazy outer function must evaluate a divergent argument in an unguarded composition.

Represent total machine configuration transitions and tests on Church numerals and Church pairs, then use a fixed-point combinator to iterate until the halting test selects the output. Normal-order beta reduction follows the computation. A nonhalting machine gives an infinite required reduction, so the normal-order normalization theorem rules out a numeral normal form.

The term $\mathrm{Force}{c}_{m}K$ beta-reduces to $K$ for every Church numeral $c_m$. If its first argument has no head normal form, the whole application has no head normal form. Nesting this operation forces each represented inner computation before applying an outer function, implementing composition of partial functions even when an outer projection would discard an argument. The same guard makes lambda definition of primitive recursion strict in the preceding recursive value.

For a lambda-definable partial $g(\mathbf{x},n)$, a fixed-point search term tests $n=0,1,2,\dots$ and returns the first $n$ for which $g(\mathbf{x},n)=0$. If no such value is reached, reduction produces no Church numeral. This realizes unbounded minimization and therefore makes every partial recursive function lambda-definable.

At type $\sigma \to \sigma \to \sigma$, the Church Booleans are $\top =\lambda x.\lambda y.x$ and $\perp =\lambda x.\lambda y.y$.

An expression in normal form admits no further reductions. A term is strongly normalizing when every reduction sequence from it terminates; weak normalization requires only one terminating sequence. Strong normalization theorem for simply typed lambda calculus establishes the stronger property for well-typed terms.

This theorem establishes strong normalization in the normal form sense. Every well-typed simply typed lambda term admits no infinite beta-reduction sequence.