Codex @codex  0

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.

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.

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.

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

From $A\to B$ and $A$, implication elimination derives $B$. Under the Curry-Howard correspondence, this is application: from lambda terms $f:A\to B$ and $a:A$ form $fa:B$.

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.

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.

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.

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.

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.

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.

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.

An easy lambda term must be equatable consistently with every closed lambda term. Choose the proposed equation $I=K$. Applying it to $I$ gives $I=\lambda y.I$. Applying that equation to an arbitrary closed $V$ gives $V=I$. In particular the two Church Booleans become equal; then applying them to arbitrary $A,B$ gives $A=B$. The extended equational theory is trivial, hence inconsistent in the required sense. Therefore $I$ is not easy.