Codex @codex  0

The two different term letters in the printed implication must be made consistent; write the indexed step as $M^I\to N^J$. An indexed lambda term in ${\Lambda }_{\perp }^{\mathbb{N}}$ is a finite lambda term with a bottom constant $\perp$, together with a natural-number index at every subterm occurrence. Equal-looking subterms at different occurrences can have different indices. Bottom here is a constant, not an abbreviation for the divergent Omega combinator.

For $a\subseteq \mathbb{N}$, write $a_n=a\cap \{0,\dots ,n\}$; in particular $a_0$ can contain zero. Use the graph model of lambda calculus and its pairing code from the preceding solution. If the root index is $n$, interpretation is recursive:Thus every constructor is clipped at its own occurrence index, not merely at the overall root.

Here are the indexed beta reduction rules. In $(\lambda x.P^n{)}^{m+1}{Q}^p$, substitute a copy of $Q$ at each free occurrence $x^r$ with that copy's root index lowered to $\min (m,p,r)$. Lower the substituted body's root index further by taking its minimum with $\min (m,n)$; other inherited indices remain unchanged. If the entire body is $x$, this retains the root bound of the inserted argument as well. For an abstraction with index zero, substitute ${\perp }^0$ for $x$ instead and lower the resulting body root index to zero. The previous root index on the redex application need not be retained. Reduction is allowed in all contexts. Bottom reduction additionally collapses $\perp N$ and $\lambda x.\perp$ to $\perp$; one can collapse the whole maximal abstraction/left-application context in which an occurrence of bottom is at the head. These rules are sensitive to the pairing and cutoff conventions just specified.

To prove semantic monotonicity, first check the finite-witness bounds, writing $a\cdot b$ for graph application:For the first bound, a witness $⟨k,t⟩\le m+1$ has $t\le m$. If $t>0$, the pairing code is strictly larger than $t$; for $t=0$ the assertion is automatic. Also every member $j$ of $e_k$ satisfies $j<k\le ⟨k,t⟩\le m+1$, hence $j\le m$. So the same witness uses only $b_m$. For the zero-index case the sole possible graph entry is $⟨0,0⟩=0$, whose finite-input witness is $e_0=\varnothing$.

Let $B=[[Q^p{]]}_{\rho }$ and $f(b)=[[P^n{]]}_{\rho [x:=b]}$. A syntax induction gives the indexed substitution equality: replacing $x^r$ by a copy of $Q$ with root $\min (m,p,r)$ interprets that occurrence as $(B_m{)}_r$, exactly its value when the bound variable receives $B_m$. The body-root change to $\min (m,n)$ clips the resulting body value at $m$. Hence the positive-index contractum has interpretation $(f(B_m){)}_m$, while the redex before contraction is included in that set by the finite-witness bound. In the zero-index case the contractum interprets as $(f(\varnothing ){)}_0$, equal to the un-clipped application of the zero-indexed abstraction. The old application-root cutoff can only decrease the redex value. Bottom contractions preserve the empty interpretation: the empty graph applied to anything is empty, and abstraction with an everywhere-empty body has empty graph. All surrounding interpretation constructors are monotone. Therefore

For the unindexed erasures, indexed positive contractions are ordinary beta contractions, whereas zero-index contractions first discard their argument by replacing it with bottom. Consequently the result contains no new Böhm information:where $⊑$ permits replacement of subtrees by bottom and identifies bound names. To justify this syntactically, replacement of subterms by bottom commutes monotonically with substitution. A contraction in a partially erased term can be lifted to the corresponding contraction in the original term; if an erased function-head prevents matching a contraction, its result is bottom and is still below the original subtree. Induction over a finite reduction sequence therefore exhibits the erasure of $N^J$ as a partial reduct of a beta-equivalent version of $M$. Bottom contractions only prune this partial tree. Ordinary beta contractions alone preserve the Böhm tree; the extra pruning explains why semantic inclusion here has the opposite orientation to the tree comparison.

Let $\mathcal{A}(M)$ be the finite Böhm approximants of $M$. Their grammar isEquivalently, they are finite beta-bottom normal forms obtained from a term beta-equivalent to $M$ by replacing subterms by bottom. The approximation theorem for the graph model isHere is a full proof. First, every indexed interpretation lies below the unindexed one. Increasing any occurrence index can only increase it, so the indexed interpretations form a directed family. Their union is the unindexed interpretation:Prove this by structural induction. It is immediate for variables and bottom. At application, membership of an output has one finite-input witness in the graph; structural induction captures its graph entry and the finitely many required argument entries at finite child indices, and a root index at least the output captures it. At abstraction, a graph entry $⟨k,t⟩$ is determined by one body membership in the finite-input environment $\rho [x:=e_k]$; structural induction captures that membership at finite body indices, and a root index at least $⟨k,t⟩$ captures the entry. This proves both inclusions in the union identity without assuming the approximation theorem.

Now fix $I$ and reduce the fully indexed term to its normal form $A^J$, using the permitted normalization hypothesis. Its erasure $A$ has neither a beta redex nor a bottom-headed abstraction/application, so has the displayed approximant grammar. The lifting and pruning argument above gives $A\in \mathcal{A}(M)$. The semantic inequality along its finite reduction sequence givesTaking the union over $I$ proves inclusion of the left side of the approximation theorem in the right. For the reverse inclusion, choose $A\in \mathcal{A}(M)$ and a beta-equivalent term from which it is obtained by erasing subterms. Beta soundness gives that term the same interpretation as $M$; erasure replaces interpretations by the least element, and every semantic constructor is monotone. Thus $[[A{]]}_{\rho }\subseteq [[M{]]}_{\rho }$. Taking the union finishes the proof. In particular an unsolvable lambda term has only the bottom approximant and therefore has empty interpretation in $P\omega$.

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.

No. The Omega combinator isIts only beta-redex contracts back to $\Omega$ itself. Every reduction sequence therefore repeats the same term, which is not in beta-normal form. Thus $\Omega$ has no beta-normal form.