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.

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.

Choose mutually inverse maps $i:D^D\to D$ and $j:D\to D^D$. This is an extensional reflexive object in the Cartesian closed category. Define its application morphismFor endomorphisms $f,g:D\to D$, application in the underlying set $\mathrm{End}(D)$ is $f\cdot g=\mathrm{app}\circ ⟨f,g⟩$.

It is useful to define term interpretation uniformly over any context object $A$. An environment assigns each free variable $x$ a morphism $\rho (x):A\to D$. Variables are interpreted by their assigned maps, and application is interpreted by $\mathrm{app}$ and pairing. For lambda abstraction, lift the old environment along ${\pi }_A:A\times D\to A$, interpret the new variable by ${\pi }_D$, and let $h:A\times D\to D$ interpret the body. Then setTaking $A=D$ gives interpretations in the requested set of endomorphisms. Other context objects are needed in the recursive definition to handle bound variables correctly.

The beta reduction rule follows from $ji={\mathrm{id}}_{D^D}$ and the evaluation identity for currying. Applying the interpreted abstraction to a map $g:A\to D$ givesInduction on terms identifies this with interpretation of the capture-avoiding substitution of the argument for $x$.

For eta conversion, suppose $x$ is not free in $M$ and write $f:A\to D$ for the interpretation of $M$. The body $Mx$ on $A\times D$ is the uncurried form of $jf$. HenceThus beta-eta-equivalent terms have equal interpretations in $\mathrm{End}(D)$. The full isomorphism, rather than just a retract of the function object, provides the inverse law used in the eta step.

Write $Q=(A\to B)\to A$ and $P=Q\to A$. The displayed formula is $(P\to B)\to B$. A proof of logical implication may use its temporary assumption more than once; this is ordinary natural deduction, not a linear proof system.

Assume $h:P\to B$, then $f:Q$, then $a:A$, then $g:Q$. The identity weakening rule derives $a:A$ from the hypotheses $a:A$ and $g:Q$. Discharging $g$ by the implication introduction rule gives $\lambda g^Q.a:P$. Applying $h$ by the implication elimination rule gives $h(\lambda g^Q.a):B$. Discharge $a$ to obtain $\lambda a^A.h(\lambda g^Q.a):A\to B$. Applying $f$ gives an $A$; discharge $f$ to obtain a $P$; apply $h$ once more to obtain $B$, and finally discharge $h$.

Here is the complete decorated natural deduction derivation, split at its intermediate $A\to B$ conclusion to keep the tree readable. Superscript labels mark which assumption occurrences are discharged; both occurrences labelled $1$ are discharged together.To avoid an excessively wide final tree, continue the same derivation as follows, using the right-hand derived premise above:followed byThus the concise lambda term, with bound-variable types determined by the displayed tree, isUnder the Curry-Howard correspondence, implication introduction rules correspond to lambda abstractions, implication elimination rules to applications, and the identity weakening rule retains the first term while allowing an unused second hypothesis. No other inference rule or classical axiom is required.

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.

In the simply typed lambda calculus, types are generated from base types by the arrow constructor $A\to B$. A context $\Gamma$ assigns types to variables. Its basic rules areThus lambda abstraction creates a function type and lambda application consumes its input type. For example, $\lambda x.x$ has type $A\to A$, and $\lambda f.\lambda x.fx$ has type $(A\to B)\to A\to B$.

The untyped self-application $xx$ would require one finite type to satisfy $A=A\to B$, which is impossible in this type grammar. This excludes the familiar looping term $(\lambda x.xx)(\lambda x.xx)$; more generally the Strong normalization theorem for simply typed lambda calculus says that every reduction sequence from a well-typed term terminates. The typing rules also correspond to implication rules through the Curry-Howard correspondence.

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.

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.

A type variable is a placeholder for a type. In a function type $\alpha \to \alpha$, the repeated type variable requires the argument and result types to agree; $\alpha \to \beta$ does not impose that agreement. A type substitution replacing $\alpha$ by int changes $\alpha \to \alpha$ to $\mathrm{int}\to \mathrm{int}$ everywhere within that instance.

For the identity function written as the lambda abstraction $\lambda x.x$, assume $x:\alpha$ in the body. Looking up $x$ gives result type $\alpha$, so the abstraction rule gives $\lambda x.x:\alpha \to \alpha$. In the pure Hindley-Milner type system, let identity = λx.x in ... gives identity the type scheme $\forall \alpha .\alpha \to \alpha$ by let polymorphism. Each use receives fresh type variables: identity 3 chooses int for its instance, and identity true chooses bool for a separate instance. These choices do not change the original type scheme.

For example, let identity = λx.x in let a = identity 3 in identity true is valid and has type bool. By contrast, (λf. let a = f 3 in f true) (λx.x) is rejected by the Hindley-Milner type system: the lambda abstraction binds f to one monomorphic function type. The first call requires its argument type to be int, and the second requires that same type to be bool. Naming the first result with let a does not generalize f. The distinction makes reusable code possible while keeping the assumptions about a supplied argument consistent.

// Target: computer-science.bigb

A typing context records the types assumed for available program names. In $\Gamma =\{x:\mathrm{int},y:\mathrm{int}\}$, looking up either name yields int. Checking a lambda abstraction extends the typing context with its argument's type for the body. In the Hindley-Milner type system, a typing context can also hold type schemes for names introduced by let polymorphism.