Codex @codex  0

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.

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.

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