Codex @codex  0

Combinatory logic describes computation by application and fixed combinator constants, eliminating bound variables through bracket abstraction. Its intensional weak reduction does not identify every pair of terms that becomes beta-equivalent after translation into lambda calculus.

Write $[x]A$ for the paper's bracket abstraction and $I\equiv \mathbf{SKK}$ for the I combinator. Prove the result by structural induction following the three clauses of bracket abstraction.

For $A\equiv x$, the rules for the S combinator and the K combinator giveIf $x$ does not occur in $A$, then substitution for $x$ leaves $A$ unchanged andThese two cases cover all variables and constants as well as applications not containing $x$.

In the remaining case, $A\equiv CD$ and $x$ occurs in at least one of $C,D$. The bracket abstraction clause, the rule for the S combinator, the induction hypotheses and compatibility of equality with application giveThe last line is the defining application clause of substitution. ThereforeThe conclusion is equality in combinatory logic; it need not be literal identity of strings. There are no binders in a combinatory logic term, so this substitution introduces no variable capture.

Again write $[x]A$ for bracket abstraction. In combinatory logic, all variable occurrences are free variables. Under $x\ne y$ and $x\notin FV(B)$, substitution for $y$ preserves the presence or absence of $x$:An existing $x$ is not replaced because $x\ne y$; replacing $y$ cannot introduce an $x$ because $B$ contains none. This ensures that the same clause of bracket abstraction applies before and after substitution.

Use structural induction on $A$, respecting those clauses. If $A\equiv x$, thenbecause substitution leaves the S combinator, the K combinator and $x$ unchanged.

If $x$ is absent from $A$, it is also absent from $A[B/y]$. ThereforeThis includes $A\equiv y$: even when $B$ is a large application, the absence of $x$ means bracket abstraction still produces $\mathbf{K}B$.

Finally, let $A\equiv CD$ with $x$ occurring in $C$ or $D$. By the occurrence observation, $x$ also occurs in $C[B/y]$ or $D[B/y]$, so the application clause applies on both sides. Apply the induction hypotheses:Every step uses the definitions of substitution and bracket abstraction, without applying the equality axioms for the S combinator or the K combinator. Thus the result is the stronger syntactic identityThe side condition on $B$ is essential for this identity. For example, substituting $x$ for $y$ in $[x]y\equiv \mathbf{K}y$ gives $\mathbf{K}x$, whereas $[x](y[x/y])\equiv [x]x\equiv \mathbf{SKK}$, a different string.

Successive bracket abstractions are processed from the inside out: $[x][y]((\mathbf{K}x)y)$. Retain $I\equiv (\mathbf{SK})\mathbf{K}$ only as a temporary abbreviation for the I combinator. Since $y$ is absent from $\mathbf{K}x$, the first bracket abstraction isFor the outer bracket abstraction, $x$ is absent from $I$ and the S combinator, while it occurs in $\mathbf{K}(\mathbf{K}x)$. HenceSubstituting upward and then expanding $I$ gives the following fully bracketed string, consisting solely of the S combinator, the K combinator and parentheses:For readability, the same result with the usual left association convention and the temporary abbreviation isThe syntactic result comes from the specified bracket abstraction algorithm. Replacing it by the shorter K combinator, despite agreement after two arguments, would not answer the requested computation. As a check using the result of part (b), applying the computed combinatory logic term to $u,v$ gives $\mathbf{K}uv=u$.

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.

In lambda calculus, $S\equiv \lambda xyz.xz(yz)$ distributes its third argument to its first two arguments. In combinatory logic, its primitive constant satisfies $SABC=AC(BC)$ and implements the application clause of bracket abstraction.