= Solution
The <Böhm tree> $BT(M)$ is $\bot$ if $M$ is an <unsolvable lambda term>. Otherwise choose a <head normal form>
$$
M\to_\beta^*\lambda x_1\cdots x_n.yM_1\cdots M_m.
$$
Its root is labeled by the binder prefix and head variable, and its ordered children are $BT(M_1),\ldots,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 define
$$
U_q=\lambda z_1\cdots z_q w.wz_1\cdots z_q,\qquad P_i^q=\lambda z_1\cdots z_q.z_i.
$$
Initially 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,\ldots,N_m$. Apply $q-m$ extra copies of $U_q$ as padding and then $P_i^q$. Direct <beta reduction> gives
$$
U_qN_1\cdots N_m\underbrace{U_q\cdots U_q}_{q-m}\,P_i^q\to_\beta^*N_i.
$$
Repeat 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 \b[$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.hP_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\le2$ 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 is
$$
\boxed{M=\lambda f.f(KK)(KI)I.}
$$
Indeed $MK\to_\beta^*(KK)I\to_\beta K=\mathsf T$, whereas $MS\to_\beta^*(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.
Back to article page
