Codex @codex  0

Beta reduction performs capture-avoiding substitution:

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.

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.

In first-order logic with logical equality, $s=t$ asserts that the terms denote the same domain element. Logical equality is interpreted as identity rather than as an arbitrary binary predicate. Its natural deduction rules include reflexivity and substitution: equal terms can replace one another in a first-order formula, subject to capture-avoiding substitution. Double-negating logical equality atoms in a Gödel-Gentzen negative translation preserves these rules when the transported translated first-order formula is stable.

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.

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.

Let $x_1,\dots ,x_s$ contain all free variables of $M$. The lambda term $M$ is a solvable lambda term if there are closed lambda terms $P_1,\dots ,P_k$ such thatAdditional arguments beyond the first $s$ are allowed. A head normal form is a term $\lambda u_1\cdots u_n.y{M}_1\cdots M_r$ with a variable at the head; its arguments need not be beta-normal.

If $M$ reduces to this head normal form, close its free variables and supply every resulting initial binder with the same closed projection(take $P=I$ when $r=0$). The head variable becomes $P$ and discards all $r$ argument terms, even divergent ones, leaving $I$. Thus a head normal form implies solvability.

Conversely suppose a closure and applications of $M$ yield $I$. The standardization theorem for beta reduction supplies a finite successful head-reduction sequence. Until $M$ exposes a head variable, its head contractions lie within $M$: a closing substitution cannot create a new head redex there, and supplied arguments cannot be used until an initial abstraction is exposed. Each such contraction commutes with the closing capture-avoiding substitution. Project the successful head computation back onto $M$, ignoring contractions in supplied arguments and the consumption of its initial binders. If this projected head computation did not reach a variable-headed spine, the full computation could not reach $I$ either. It therefore gives a finite head reduction of $M$ to a head normal form. ConsequentlyThe same head-trace argument shows that an unsolvable lambda term stays unsolvable under substitution and application. This also justifies the unsolvability conclusion in the preceding solution.

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.

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.

Use the Gödel-Gentzen negative translation, writing $A^N$ for the translated first-order formula. On atomic formulas $P$, including logical equality, put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Extend recursively byLogical negation abbreviates logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:Every double logical negation is stable, since intuitionistic first-order logic proves $\neg \neg \neg \neg C\to \neg \neg C$; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication $C\to D$ with stable $D$, assume $\neg \neg (C\to D)$ and $C$. An assumption $\neg D$ would give $\neg (C\to D)$, a contradiction, so $\neg \neg D$ and then $D$. For a universal first-order formula, $\neg \neg \forall xC(x)$ implies $\neg \neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives $A^N\vee B^N$ and then its double logical negation. For logical disjunction elimination, the translated premise is $\neg \neg (A^N\vee B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg (A^N\vee B^N)$, which contradicts the premise. We have $\neg \neg C^N$ and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)⊢C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\neg A^N(y)$ and therefore $\neg \exists y{A}^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives $t=t$ and then its double logical negation. For substitution, from $\neg \neg (s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic logical equality substitution, so it gives a contradiction and hence $\neg (s=t)$. The first premise contradicts this. Thus $\neg \neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical double-negation elimination step translates precisely to $\neg \neg A^N\to A^N$, already proved. Every rule is therefore covered, giving negative translation of a classical proof:In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives $P^N\leftrightarrow P$ on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore

For a specified programming language and execution model, type safety commonly follows from two properties: a closed expression satisfying a typing judgment is either a value or can take an execution step, and taking a step preserves its type. Proofs proceed by structural induction on derivations, using capture-avoiding substitution for function calls. Repeated preservation keeps the remaining expression typed; the first property then rules out getting stuck at an operation outside the model's permitted cases. This argument does not imply termination or correctness of an arbitrary specification. ^[ref]

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.