Ess And Kay Combinators

SKI calculus (CombinatoryLogic) is an (independently and earlier invented, see below) "identifier-free" variant of the LambdaCalculus. Every LambdaCalculus expression can be compiled into an expression that only consists of function application and the three basic functions S, K and I.

 I returns its argument: (I x) -> x

 K throws away its 2nd argument and returns the first: (K x y) -> x

 S is a sort of generic substitution operator: (S x y z) -> (x z (y z))

Even I can be dispensed with as I = (S K K) :

(S K K x) -> (K x (K x)) -> x

These are enough to do math because the LambdaCalculus is sufficient to model arithmetic and predicate logic, and the combinators are sufficient to model lambda calculus.

Here are the mappings that Schonfinkel, of CurryingSchonfinkelling fame, found (there are others)

\x.x = I
\x.c = (K c) (c is a constant)
\x.(p q) = (S \x.p \x.q)

For example, let's convert the ChurchNumeral '2' into a combinator:

  2
= \f.\x.(f (f x))
= \f.(S \x.f \x.(f x))
= \f.(S (K f) (S \x.f \x.x))
= \f.(S (K f) (S (K f) I))
= (S \f.(S (K f)) \f.(S (K f) I))
= (S (S \f.S \f.(K f)) (S \f.(S (K f)) \f.I))
= (S (S (K S) (S \f.K \f.f)) (S (S \f.S \f.(K f)) (K I)))
= (S (S (K S) (S (K K) I))   (S (S (K S) (S \f.K \f.f)) (K I)))
= (S (S (K S) (S (K K) I))   (S (S (K S) (S (K K) I)) (K I)))

And indeed, if you apply this expression to f and then to x, and reduce the result, you get (f (f x)).

The expansion in size is typical; if the original lambda-term has length n, the corresponding combinatorial term will have length O(n^2). The size of the combinatorial term is doubled or tripled for each variable eliminated from it.

There is also a very handy rule similar to lambda calculus' eta reduction, which makes many abstraction eliminated formulas shorter:

\x.(c x) = c (if x is not free in c)

Using this rule shortens the derivation above to:

  2
= \f.\x.(f (f x))
= \f.(S \x.f \x.(f x))
= \f.(S (K f) f)
= (S \f.(S (K f)) \f.f)
= (S (S \f.S \f.(K f)) I)
= (S (S (K S) K) I)

The construction can be made more efficient by adding extra combinators B and C (first introduced by DavidTurner):

 (B x y z) -> (x (y z))
 (C x y z) -> (x z y)

, and extra mapping:

\x.(p q) = (B p \x.q) if x does not occur free in p
\x.(p q) = (C \x.p q) if x does not occur free in q

Using Turner's combinators, the derivation above goes like this:

  2
= \f.\x.(f (f x))
= \f.(C f \x.(f x))
= \f.(C f f)
= (S \f.(C f)) \f.f)
= (S C I)

And indeed, (S C I f x) reduces to (f (f x)):

  (S C I f x) 
= (C f (I f) x)    (reduce the S)
= (f (I f x))      (reduce the C)
= (f (f x))        (reduce the I)

A "combinator base" is a set of combinators sufficient for TuringCompleteness. Combinator bases include (S, K), (C, B, W, K) where W x y -> x y y, and (C, B, S, I) for lambda i calculus.

This was originally envisaged as a way to implement FunctionalProgramming languages efficiently. However, it turned out to be a rather bad representation for implementation on stock hardware. Nowadays, industrial-strength FPL implementations rewrite LambdaCalculus expressions into SuperCombinators.

See http://www.cwi.nl/~tromp/cl/cl.html for a Java applet that lets you try your hand as SKI'ing. This page also presents a combinator evaluator written in terms of S and K combinators.

The UnLambdaLanguage (http://www.eleves.ens.fr:8080/home/madore/programs/unlambda/) is based on the SKI calculus. (But the output model is based on side effects.)

Lazy K is an even more pure implementation of SKI: http://homepages.cwi.nl/~tromp/cl/lazy-k.html

Iota and Jot use a simpler basis combinator upon which S and K can be constructed. You can try them out using JavaScript interpreters on http://ling.ucsd.edu/~barker/Iota/. Syntax errors are impossible in Jot, since any binary integer is a well-formed Jot program (handy for GoedelNumbering).

I recently heard that both S and K can be made from the X combinator, though I forget the details. --ShaeErisson

X is not a pure combinator, because it must be expressed using inner lambda constructions. One possible definition is, IIRC,

 X = \x.xKSK
where K = \xy.x
 S = \xyz.xz(yz)

(as above).

I believe that the definitions of C and B above are reversed from those that DavidTurner proposed.

 B = \fgx.f(gx)
 C = \fxy.fyz

It is possible to construct a one-combinator base:

 X = \f.fS(\xyz.x)

This combinator can be used to construct the (S, K) base:

 K = XX
 S = X(XX)

The paper describing the derivation of this one-combinator base can be found at http://www.cs.uu.nl/people/jeroen/article/combinat/index.html

Jeroen Fokker's article quotes four different ways to define an X that gives a complete basis for combinators, and in addition derives a fifth one, that is still the shortest AFAIK.

Combinator in many programming languages:

The book To Mock a Mockingbird, by RaymondSmullyan, consists of logic puzzles and text which cover the basics of combinators, rather more elegantly than any formal treatment I've seen, and rather more thoroughly than any informal treatment I've seen.

HaskellCurry had ideas that he felt were validated upon reading a 1924 paper by M. Schönfinkel "Uber die Bausteine der mathematischen Logik" which used combinators in a similar way to his own ideas. Haskell then wrote "An analysis of logical substitution" which appeared in the American Journal of Mathematics in 1929.

Compare with the later LambdaCalculus by Kleene and Church; the proof of the nonexistence of solutions to the EntscheidungsProblem pre-dated the more famous HaltingTheorem.

Stephen Kleene, A theory of positive integers in formal logic, American Journal of Mathematics, 57 (1935), pp 153 - 173 and 219 - 244. Contains the lambda calculus definitions of several familiar functions.

AlonzoChurch, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp 345 - 363. This paper contains the proof that the equivalence of lambda expressions is in general not decidable.

Curry has historic precedence in the areas where his combinatoric logic and lambda calculus are equivalent, not the other way around, as is often thought.

CategoryFunctionalProgramming