= Solution
A <combinatory logic term> over free variables $X$ is formed from variables in $X$, the constants $S,K,I$, and application, with no abstraction binder. We may regard $I$ as primitive, or as the abbreviation $SKK$. Application associates to the left. <Weak combinatory reduction> contracts
$$
KAB\to A,\qquad SABC\to AC(BC),\qquad IA\to A
$$
in any application context. Weak equivalence is the equivalence relation generated by these reductions. There is no additional rule identifying terms merely because they behave alike after application to a fresh argument.
Define <bracket abstraction> on combinatory terms by the following ordered clauses:
$$
[x]x=I;\qquad [x]T=KT\ \text{if }x\notin FV(T);\qquad [x](PQ)=S([x]P)([x]Q)\ \text{otherwise}.
$$
They cover every term: after excluding the variable case and the case with no free $x$, the term must be an application. Induction gives $FV([x]T)=FV(T)\setminus\{x\}$; no other variable is introduced or removed. For every argument $A$, the same induction gives $([x]T)A\to^*T[x:=A]$: the three cases use respectively the $I$, $K$, and $S$ reductions.
The required translation is
$$
\boxed{x^*=x,\qquad(MN)^*=M^*N^*,\qquad(\lambda x.M)^*=[x](M^*).}
$$
It has exactly the same set of <free variables> as the original <lambda term>, by the bracket-abstraction identity.
To compare the two reductions, expand the constants into <lambda terms>:
$$
S^\lambda=\lambda a.\lambda b.\lambda c.ac(bc),\quad K^\lambda=\lambda a.\lambda b.a,\quad I^\lambda=\lambda a.a,
$$
and expand variables and applications homomorphically. Every weak combinatory contraction becomes a finite sequence of <beta reductions>, so weakly equivalent terms have beta-equivalent lambda expansions. We also have
$$
([x]T)^\lambda\equiv_\beta\lambda x.T^\lambda.
$$
For $T=x$, this is the expansion of $I$. For $x\notin FV(T)$, the expansion of $KT$ beta-reduces to $\lambda x.T^\lambda$, after choosing the binder fresh. For an application, expanding $S([x]P)([x]Q)$ gives
$$
\lambda x.([x]P)^\lambda x\,\bigl(([x]Q)^\lambda x\bigr)\equiv_\beta\lambda x.P^\lambda Q^\lambda,
$$
by induction and beta contraction. Thus, induction on the lambda syntax gives $(M^*)^\lambda\equiv_\beta M$. Combining these facts proves
$$
\boxed{M^*\equiv_{\mathrm{weak}}N^*\ \Longrightarrow\ M\equiv_\beta N.}
$$
The reverse implication fails for this intensional translation. The beta-equivalent <lambda terms> $M=\lambda x.x$ and $N=\lambda x.((\lambda y.y)x)$ translate respectively to
$$
M^*=I,\qquad N^*=[x](Ix)=S(KI)I.
$$
Both are weak normal forms: $I$ has no argument, $KI$ has too few arguments to contract, and the outer $S$ has only two arguments. They are syntactically distinct. By the assumed Church–Rosser property of <weak combinatory reduction>, two distinct weak normal forms cannot be weakly equivalent. The same argument works with $I=SKK$, because both fully expanded terms remain distinct weak normal forms. Hence \b[beta-equivalent <lambda terms> need not have weakly equivalent combinatory translations].
Back to article page
