Bracket Abstraction: Compiling Lambda Terms into Combinators

A lambda term binds variables. A combinator has no variables to bind: it is a term built from a fixed set of constants by application alone. The claim that these two systems express the same functions is Schönfinkel’s and Curry’s, and it is constructive. Every lambda term can be translated into a variable-free term over two constants, and the translation is a syntactic algorithm that a compiler can run. The algorithm is called bracket abstraction, and its history is the history of the first implementations of lazy functional languages, which used it to turn source programs into graphs of applications that a fixed set of reduction rules could execute.

The interest is not antiquarian. Bracket abstraction is the cleanest example of eliminating a binding form by a local rewrite, and the naive version of it has a size explosion that every real implementation has to fix. Both the theorem and the explosion are instructive.

The basis, and what it has to satisfy

Two constants suffice. K takes two arguments and returns the first; S takes three, applies the first to the third, and applies the result to the second applied to the third:

K = λx. λy. x
S = λx. λy. λz. x z (y z)

Read as reduction rules on combinator terms:

K a b   → a
S a b c → a c (b c)

A term built from S, K, and variables by application is a combinatory term. The claim is that for every lambda term M there is a combinatory term M* with no binders such that M* and M denote the same function. The proof is by induction, and the inductive step is the interesting one: it has to eliminate a binder from a term that has already had its inner binders eliminated.

The step is a function [x] that maps a combinatory term N (possibly containing x) to a term with no x such that ([x] N) x reduces to N. Three clauses suffice:

[x] x       = I            where I = S K K
[x] y       = K y          (y ≠ x)
[x] (P Q)   = S ([x] P) ([x] Q)

The first clause says the identity function returns its argument. The second says a constant function ignores its argument and returns y. The third distributes the abstraction over application, and it is the clause that makes the translation work: S ([x] P) ([x] Q) applied to a reduces to ([x] P) a (([x] Q) a), which by induction is P[x := a] Q[x := a], which is (P Q)[x := a]. The induction hypothesis is exactly the specification of [x], and S is the combinator that duplicates the argument so both halves can consume it.

I is not primitive; S K K behaves as the identity, since S K K a → K a (K a) → a. Including it as an abbreviation keeps the clauses readable.

The translation, traced

Take λx. x x, the self-application that drives divergence. Abstracting over x:

[x] (x x)
  = S ([x] x) ([x] x)
  = S I I

and indeed S I I a → I a (I a) → a a. Take λx. λy. x, the K combinator itself:

[x] (λy. x)   -- inner binder first
  = [x] ([y] x)
  = [x] (K x)              because [y] x = K x when y ≠ x
  = S ([x] K) ([x] x)
  = S (K K) I

So λx. λy. x translates to S (K K) I, which is beta-equivalent to K but not syntactically equal. Check: S (K K) I a b → (K K a) (I a) b → K (I a) b → I a → a. Correct, and several reduction steps longer than the primitive K, which contracts in one.

The order of abstraction matters for the size of the result. Abstracting the innermost binder first is the standard convention, because [x] then distributes over a structure that is already variable-free except for x. Abstracting outermost first forces the inner binders to be treated as opaque constants, which the general clauses handle by wrapping each of them in K.

The size growth is the problem. Each [x] clause on an application duplicates the abstraction of the left and right subterms, and the S inserted at every application node doubles the number of references to the abstracted variable’s occurrences. For a term where x occurs k times, the naive translation produces a term whose size is proportional to k times the size of the original, and for nested abstractions the growth compounds. A term of n nodes can translate to a term of size exponential in n. That is not an implementation detail; it is a property of the naive algorithm, and it is why the translation is not used in that form.

Optimising the abstraction

Three standard fixes reduce the growth, and each is a recognisable compiler optimisation under a different name.

The eta clause. If x does not occur free in P, then [x] (P x) can be P directly, because P already ignores its argument. Adding this clause as a special case before the general application clause avoids inserting an S whose second argument would be I. The clause is exactly eta-reduction applied during abstraction, and it removes the most common source of a redundant S.

The B combinator. A larger basis reduces duplication. B = λx. λy. λz. x (y z) satisfies B a b c → a (b c). When the abstracted variable does not occur in the function part P, the general clause can be replaced by [x] (P Q) = B P ([x] Q), since B P ([x] Q) a → P (([x] Q) a) → P (Q[x := a]), which is (P Q)[x := a] when x is absent from P. The K that the general clause would insert around P disappears, and with it one reduction step at every application.

The C combinator. C = λx. λy. λz. x z y satisfies C a b c → a c b. When the variable does not occur in the argument part Q, the clause becomes [x] (P Q) = C ([x] P) Q, since C ([x] P) Q a → ([x] P) a Q → P[x := a] Q, which is again the substitution instance of P Q when Q is free of x.

With a basis of S, K, B, C, and I, the translation can be made to grow more slowly for a large class of terms, because each clause avoids duplicating or discarding the subterm that does not contain the variable. The basis is no longer minimal, which matters if the target is a two-combinator machine and does not matter if the target is a compiler with a library of primitives.

Supercombinators. The industrial version abandons the fixed basis entirely. A supercombinator is a closed term with no free variables, and the translation of a program is a set of supercombinators plus a rule for applying them. Each lambda is lifted to top level with its free variables as extra parameters, and the resulting terms are compiled to native code rather than to combinator reductions. This is the approach taken by the early graph-reduction implementations and by later compiled lazy languages, and it removes the size problem at the cost of a more complicated runtime.

What the translation buys and costs

The gain is that reduction becomes a fixed set of rewrite rules on a graph with no binders, no substitution, and no alpha-conversion. A combinator term is a tree of applications of constants, and the only operation is replacing a redex K a b or S a b c by its contractum. That is a local graph rewrite, which is exactly what a graph reducer does, and it needs no environment because there are no variables.

The cost is step count. Every abstraction costs at least one S or K, and every application of an abstracted function costs the reduction steps that S and K introduce. Comparing the two accounts for λx. λy. x: as a lambda it applies in one beta step; as S (K K) I it takes four combinator steps. For a function called n times, the difference is a constant factor per call, but the constant is not small, and it compounds through nested abstractions.

There is a second cost that is worse. S duplicates its third argument, and in a graph reducer that means the argument’s graph is shared rather than copied — the two occurrences point at the same node, and the first reduction updates the node in place. That is the mechanism that makes combinator reduction viable, and it is also the mechanism that makes the step count hard to predict: a shared redex is reduced once, no matter how many references point at it. Without sharing, S would copy and the translation would be unusable. The graph reducer’s update-in-place is not an optimisation of the combinator calculus; it is what makes the calculus a viable execution model.

A third cost is diagnostics. A combinator term has no variables and no source positions, so an error message from a graph reducer is a dump of a term like S (S (K S) (K K)) ..., which corresponds to nothing a programmer wrote. Implementations keep a map from combinator nodes back to source, and the map is the only link between the two worlds.

Why the translation is still worth knowing

Bracket abstraction is the proof that binding is eliminable. That fact has consequences beyond the specific basis. It shows that a language with lexical scope can be compiled into a language without it, which is the theoretical justification for closure conversion: the environment that a closure carries is the runtime analogue of the K and S that the translation inserts. It shows that alpha-conversion is not essential to the calculus, only to its surface syntax. And it gives a normal form for the translation problem: every lambda term has a combinator representative, so a question about lambda terms can be answered by answering it about combinator terms.

The translation also makes the correspondence between the two systems precise. Combinatory logic has its own reduction relation, and the translation preserves it: if M →β N then M* and N* are related by combinator reduction. The converse fails in general, because combinator reduction can perform steps that correspond to no single beta step, which is why the two systems are equivalent as theories of functions but not step-for-step as reduction systems. The equivalence is at the level of the definable functions, and that is the level at which the Church encodings live.

The remaining question, after the translation is understood, is what the translation preserves. Two lambda terms that are beta-eta equivalent translate to combinator terms that are equivalent in the corresponding equational theory, and the translation of a normal form is a normal form. What it does not preserve is the structure of the term, and the sharper question is whether, for two terms that are not equivalent, there is always a context that distinguishes them. For terms with normal forms the answer is yes, and the proof is the subject of Böhm’s theorem and the limits of separability. The machines that execute the translated terms are the graph reducers described with the abstract machines, and the sharing they depend on is the reason the step counts differ from the lambda account.