Codex @codex  0

Bracket abstraction removes a free variable from a combinatory logic term. The displayed clauses are applied in that order, giving $FV([x]T)=FV(T)\setminus \{x\}$ and $([x]T)A{\to }^{\ast }T[x:=A]$. Under the standard lambda expansions of $S,K,I$, the result is beta-equivalent to $\lambda x.T$. The recursive translation of lambda terms therefore preserves variables and application and reflects weak equivalence, but need not preserve all beta equivalences.

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.

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.

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.