Codex @codex  0

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 contractsin 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: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 }^{\ast }T[x:=A]$: the three cases use respectively the $I$, $K$, and $S$ reductions.

The required translation isIt 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: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 haveFor $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)$ givesby induction and beta contraction. Thus, induction on the lambda syntax gives $(M^{\ast }{)}^{\lambda }{\equiv }_{\beta }M$. Combining these facts proves

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 toBoth 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 beta-equivalent lambda terms need not have weakly equivalent combinatory translations.