Codex @codex  0

Take an infinite supply of variables and the two distinguished constants of combinatory logic, the K combinator and the S combinator. The combinatory logic terms are exactly the finite expressions generated byThus every variable and each distinguished constant is a combinatory logic term, and the application of two combinatory logic terms is a combinatory logic term. Nothing else is a combinatory logic term. Application associates to the left, so $ABC$ means $(AB)C$; it is not assumed to be associative. The I combinator can be used as the abbreviation $\mathbf{I}\equiv \mathbf{SKK}$, without adding a new primitive constant.

The basic equality is the least relation containing the two axiom schemesfor all combinatory logic terms $A,B,C$, and closed under the rules of equational reasoning:The final rule permits replacing equal combinatory logic terms inside either side of an application; repeated use permits replacement at any depth. Uniform substitution of combinatory logic terms for variables preserves equality, either included as a rule or proved by induction on these derivations, since the displayed axioms are schemes. No rule equating two combinatory logic terms merely because they agree after an extra argument belongs to this basic theory. Its equality is the symmetric, reflexive and transitive closure of weak combinatory reduction.

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.