Introduction - Simple Kombinator Interpreter

Preamble

Welcome to the wonderful world of combinatory logic, a lovechild of lisp and brainfuck, developed by Moses Schönfinkel and Haskell Curry in the 1930s.

A combinator is a one-argument function that accepts a one-argument function and returns a one-argument function. Everything here is a function - numbers, booleans, lists, and even free variables stand for functions we don't know how to compute just yet.

The tradition is to depict the combinators as birds, and we won't be stepping too far away from it.

How computations work

Given that x and y are combinators, then so is x y; if z is also a combinator, then x y z is calculated as (x y) z. x y z, x(y)(z), (x y)(z), (x(y))(z) are all the same thing. x (y z), however, is not the same as (x y) z (at least not for arbitrary terms).
If a reduction rule is known for the leftmost term in an (sub-)expression, it is applied. Reduction rules are given in the form of "X a b c = b (c a)" and are interpreted as follows: X a returns a function f1 such that f1 b returns a function f2 such that f2 c returns expression b (c a). This technique is known as currying.
A computation terminates when no more reductions can be made.

With a right set of initial terms this is enough for Turing completeness, and at least one such set exists, as we'll see shortly.

On the notation

On the notation: we'll be typically using single capital letters for common combinators, lowercase letters for free variables, and lowercase words for compound expressions. Uppercase letters can be lumped together and lowercase terms must be separated with spaces.

E.g. CBx foo (y z) (SII) - here only C and S are reduction candidates

The S, K, I basis

I, the Ibis, or Identity, has a very simple reduction rule: for any term x, I x = x. Thus IIx, I(II)x, II(Ix) and so on all converge to x. Note, however, that x I does not equal x and x I y does not equal x y.

K, the Kestrel, or Konstant, is defined as K x y = x. Here's where currying happens for real: K x returns a function which in turn discards its argument and returns x and nothing else. Note again that x K y z does not become x y because K is not in the first place and the reduction rule is not applicable.

S, the Starling, adheres S f g x = f x (g x). That is, given two functions and an argument (which is also a function given the setup, but it's not important here), it applies both functions to the argument and fuses the results together.

Connection to lambda calculus

An arbitrary lambda expression can be converted to SKI via the following rules:

λ x . x becomes I;
λ x . f(x) (where f is independent of x) becomes f;
λ x . y (where y does not depend on x) becomes K y;
λ x . y(z) becomes S(λ x . y)(λ x . z), where y and z may or may not depend on x.
The process is repeated from the innermost lambda expression outwards and is guaranteed to terminate. (proof?..)

As a matter of fact, I can be derived from S and K and those two thus form a basis together.

In place of a conclusion