2 Combinatory calculi

Since abstraction is the only way to manufacture functions in the lambda calculus, something must replace it in the combinatory calculus. Instead of abstraction, combinatory calculus provides a limited set of primitive functions out of which other functions may be built.

2.1 Combinatory terms

A combinatory term has one of the following forms:

V P (E1 E2)

where V is a variable, P is one of the primitive functions, or E1 and E2 are combinatorial terms. The primitive functions themselves are combinators, or functions that contain no free variables.

2.2 Examples of combinators

The simplest example of a combinator is I, the identity combinator, defined by

(I x) = x

for all terms x. Another simple combinator is K, which manufactures constant functions: (K x) is the function which, for any argument, returns x, so we say

((K x) y) = x

for all terms x and y. Or, following the same convention for multiple application as in the lambda-calculus,

(K x y) = x

A third combinator is S, which is a generalized version of application:

(S x y z) = (x z (y z))

S applies x to y after first substituting z into each of them.

Given S and K, I itself is unnecessary, since it can be built from the other two:

((S K K) x) = (S K K x) = (K x (K x)) = x

for any term x. Note that although ((S K K) x) = (I x) for any x, (S K K) itself is not equal to I. We say the terms are extensionally equal. Extensional equality captures the mathematical notion of the equality of functions: that two functions are 'equal' if they always produce the same results for the same arguments. In contrast, the terms themselves capture the notion of intensional equality of functions: that two functions are 'equal' only if they have identical implemenations. There are many ways to implement an identity function; (S K K) and I are among these ways. (S K S) is yet another. We will use the word equivalent to indicate extensional equality, reserving equal for identical combinatorial terms.

A more interesting combinator is the fixed point combinatorComputer science Lambda calculus Computability A fixed point combinator is a function which computes fixed points of other functions. A 'fixed point' of a function is a value left 'fixed' by that function; for example, 0 and 1 are fixed points of the squa or Y combinator, which can be used to implement recursionIn mathematics and computer science, recursion is a particular way of specifying (or constructing) a class of objects (or an object from a certain class) with the help of a reference to other objects of the class: a recursive definition defines objects in.

2.3 Completeness of the S-K basis

It is a perhaps astonishing fact that S and K can be composed to produce combinators that are extensionally equal to any lambda term, and therefore, by Church's thesis, to any computable function whatsoever. The proof is to present a transformation, T[ ], which converts an arbitrary lambda term into an equivalent combinator.

T[ ] may be defined as follows:

1. T[V] => V
2. T[(E1 E2)] => (T[E1] T[E2])
3. T[λx.E] => (K T[E]) (if x is not free in E)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
6. T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2])

2.3.1 Conversion of a lambda term to an equivalent combinatorial term

For example, we will convert the lambda term λx.λy.(y x)) to a combinator:

T[λx.λy.(y x)] = T[λx.T[λy.(y x)]] (by 5) = T[λx.(S T[λy.y] T[λy.x])] (by 6) = T[λx.(S I T[λy.x])] (by 4) = T[λx.(S I (K x))] (by 3) = (S T[λx.(S I)] T[λx.(K x)]) (by 6) = (S (K (S I)) T[λx.(K x)]) (by 3) = (S (K (S I)) (S T[λx.K] T[λx.x])) (by 6) = (S (K (S I)) (S (K K) T[λx.x])) (by 3) = (S (K (S I)) (S (K K) I)) (by 4)

If we apply this combinator to any two terms x and y, it reduces as follows:

(S (K (S I)) (S (K K) I) x y) = (K (S I) x (S (K K) I x) y) = (S I (S (K K) I x) y) = (I y (S (K K) I x y)) = (y (S (K K) I x y)) = (y (K K x (I x) y)) = (y (K (I x) y)) = (y (I x)) = (y x)

The combinatory representation, (S (K (S I)) (S (K K) I)) is much longer than the representation as a lambda term, λx.λy.(y x). This is typical. In general, the T[ ] construction may expand a lambda term of length n to a combinatorial term of length

ΘIn complexity theory, computer science, and mathematics the Big O notation is a mathematical notation used to describe the asymptotic behavior of functions. More exactly, it is used to describe an asymptotic upper bound for the magnitude of a function in(3ⁿ).

2.3.2 Explanation of the T[ ] transformation

The T[ ] transformation is motivated by a desire to eliminate abstraction. Two special cases, rules 3 and 4, are trivial: λx.x is clearly equivalent to I, and λx.E is clearly equivalent to (K E) if x does not appear free in E.

The first two rules are also simple: Variables convert to themselves, and applications, which are allowed in combinatory terms, are converted to combinators simply by converting the applicand and the argument to combinators.

It's rules 5 and 6 that are of interest. Rule 5 simply says that to convert a complex abstraction to a combinator, we must first convert its body to a combinator, and then eliminate the abstraction. Rule 6 actually eliminates the abstraction.

λx.(E1 E2) is a function which takes an argument, say a, and substitutes it into the lambda term (E1 E2) in place of x, yielding (E1 E2)[a/x]. But substituting a into (E1 E2) in place of x is just the same as substituting it into both E1 and E2, so

(E1 E2)[a/x] = (E1[a/x] E2[a/x])

(λx.(E1 E2) a) = ((λx.E1 a) (λx.E2 a)) = (S λx.E1 λx.E2 a) = ((S λx.E1 λx.E2) a)

By extensional equality,

λx.(E1 E2) = (S λx.E1 λx.E2)

Therefore, to find a combinator equivalent to λx.(E1 E2), it is sufficient to find a combinator equivalent to (S λx.E1 λx.E2), and

(S T[λx.E1] T[λx.E2])

evidently fits the bill. E1 and E2 each contain strictly fewer applications than (E1 E2), so the recursion must terminate in a lambda term with no applications at all---either a variable, or a term of the form λx.E.

2.4 Simplifications of the transformation

2.4.1 η-reduction

The combinators generated by the T[ ] transformation can be made smaller if we take into account the η-reduction rule:

T[λx.(E x)] = T[E] (if x is not free in E) λx.(E x) is the function which takes an argument, x, and

applies the function E to it; this is extensionally equal to the function E itself. It is therefore sufficient to convert E to combinatorial form.

Taking this simplification into account, the example above becomes:

T[λx.λy.(y x)] = ... = (S (K (S I)) T[λx.(K x)]) = (S (K (S I)) K) (by η-reduction)

This combinator is equivalent to the earlier, longer one:

(S (K (S I)) K x y) = (K (S I) x (K x) y) = (S I (K x) y) = (I y (K x y)) = (y (K x y)) = (y x)

Similarly, the original version of the T[] transformation transformed the identity function λf.λx.(f x) into (S (S (K S) (S (K K) I)) (K I)). With the η-reduction rule, λf.λx.(f x) is transformed into I.

2.4.2 Combinators B, C of Curry

The combinators S and K already figure in the work of SchönfinkelSchonfinkel, Moses Moses Schonfinkel was a Russian Logician. He invented combinatory logic independently of, and a little earlier than, Haskell Curry. Schonfinkel published his logic in a paper called ber die Bausteine der mathematischen Logik On the buil (although symbol C was used instead of present K), Curry introduced the use of B, C, W (and K), already in his doctoral thesis of 1930 (see B,C,K,W System). In Combinatory Logic V. I, we return to S, K but, (via Markov's algorithms) he uses B and C to simplify many reductions. This seems to have been used, much later, by David Turner, whose name has been bound to its computational use. Two new combinators are introduced:

(C a b c) = (a c b) (B a b c) = (a (b c))

Using these combinators, we can extend the rules for the transformation as follows:

1. T[V] => V
2. T[(E1 E2)] => (T[E1] T[E2])
3. T[λx.E] => (K T[E]) (if x is not free in E)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
6. T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2]) (if x is free in both E1 and E2)
7. T[λx.(E1 E2)] => (C T[λx.E1] E2) (if x is free in E1 but not E2)
8. T[λx.(E1 E2)] => (B E1 T[λx.E2]) (if x is free in E2 but not E1)

Using B and C combinators, the transformation of λx.λy.(y x) looks like this:

T[λx.λy.(y x)] = T[λx.T[λy.(y x)]] = T[λx.(C T[λy.y] x)] (by rule 7) = T[λx.(C I x)] = (C I) (η-reduction) = C_*(traditional canonical notation : X_* = X I) = I'(traditional canonical notation: X' = C X)

And indeed, (C I x y) does reduce to (y x):

(C I x y) = (I y x) = (y x)

The motivation here is that B and C are limited versions of S. Whereas S takes a value and substitutes it into both the applicand and its argument before performing the application, C performs the substitution only in the applicand, and B only in the argument.

2.5 Reverse conversion

The conversion L[ ] from combinatorial terms to lambda terms is trivial:

L[I] = λx.x L[K] = λx.λy.x L[C] = λx.λy.λz.(x z y) L[B] = λx.λy.λz.(x (y z)) L[S] = λx.λy.λz.(x z (y z)) L[(E1 E2)] = (L[E1] L[E2])

Note, however, that this transformation is not the inverse transformation of any of the versions of T[ ] that we have seen.

3 Undecidability of Combinatorial Calculus

It is undecidable whether a general combinatory term has a normal form; whether two combinatory terms are equivalent, etc. This is equivalent to the undecidability of the corresponding problems for lambda terms. However, a direct proof is as follows:

First, observe that the term

Ω = (S I I (S I I))

has no normal form, because it reduces to itself after three steps, as follows:

(S I I (S I I)) = (I (S I I) (I (S I I))) = (S I I (I (S I I))) = (S I I (S I I))

and clearly no other reduction order can make the expression shorter.

Now, suppose N were a combinator for detecting normal forms, such that

(N x) => T, if x has a normal form F, otherwise.

(Where T and F the transformations of the conventional lambda-calculus definitions of true and false, λx.λy.x and λx.λy.y. The combinatory versions have T = K and F = (K I).)

Now let

Z = (C (C (B N (S I I)) Ω) I)

now consider the term (S I I Z). Does (S I I Z) have a normal form? It does if and only if the following do also:

(S I I Z) = (I Z (I Z)) = (Z (I Z)) = (Z Z) = (C (C (B N (S I I)) Ω) I Z) (definition of Z) = (C (B N (S I I)) Ω Z I) = (B N (S I I) Z Ω I) = (N (S I I Z) Ω I)

Now we need to apply N to (S I I Z). Either (S I I Z) has a normal form, or it does not. If it does have a normal form, then the foregoing reduces as follows:

(N (S I I Z) Ω I) = (K Ω I) (definition of N) = Ω

but Ω does not have a normal form, so we have a contradiction. But if (S I I Z) does not have a normal form, the foregoing reduces as follows:

(N (S I I Z) Ω I) = (K I Ω I) (definition of N) = (I I) I

which means that the normal form of (S I I Z) is simply I, another contradiction. Therefore, the hypothetical normal-form combinator N cannot exist.

4 Combinatory terms as graphs

(TO DO: Add details with illustrations; don't forget to discuss the effect of fixed-point combinators.)

5 Applications

5.1 Compilation of functional languages

Functional programming languages are often based on the simple but

universal semantics of the lambda calculus. (Add details.)

David Turner used his combinators to implement the SASL language .

(Discuss strict vs. lazy evaluation semantics. Note implications of graph reduction implementation for lazy evaluation. Point out efficiency problem in lazy semantics: Repeated evaluation of the same expression, in, e.g. (square COMPLICATED) => (* COMPLICATED COMPLICATED), normally avoided by eager evaluation and call-by-value. Discuss benefit of graph reduction in this case: when (square COMPLICATED) is evaluated, the representation of COMPLICATED can be shared by both branches of the resulting graph for (* COMPLICATED COMPLICATED), and evaluated only once.)

5.2 Logic

The Curry-Howard isomorphism implies a relationship between logic and programming: Every valid proof of a theorem of logic corresponds directly to a reduction of a lambda term, and vice versa. Theorems themselves are identified with function type signatures. Specifically, typed combinatory logics correspond to Hilbert system s in proof theory.

(Add: Demonstration that the axioms

(a -> a) (a -> b -> a) (a -> b -> c) -> (a -> b) -> (a -> c)

are complete for the intuitionistic fragment of propositional logic.)

See also:

• graph reduction machine
• supercombinator s

6 References

• Functional Programming. Field, Anthony J. and Peter G. Harrison. Addison-Wesley, 1998. BooksEnthsiast.com
• "Foundations of Functional Programming". Lawrence C. Paulson. University of Cambridge, 1995.
• "Lectures on the Curry-Howard Isomorphism". Sørensen, Morten Heine B. and Pawel Urzyczyn. University of Copenhagen and University of Warsaw, 1999.
• 1920-1931 Curry's block notes

Logic in computer science Mathematical logic Lambda calculus Computability Functional programming

<Hide>