# S and K Turing-completeness proof

Many esoteric programming languages in the functional paradigm use the S and K combinators to demonstrate that they are Turing-complete. This page outlines a proof that the S and K combinators are Turing-complete, by showing that any expression in Lambda calculus can be converted into these combinators.

Currently missing is an argument that the conversion preserves the respective reduction/evaluation semantics of the computation models.

## Conversion

We begin by observing the following equivalences:

- Ky = (λ x.y)
- (SKK) = (λ x.x)
- (S(λ x.f)(λ x.g)) = (λ x.fg)
- y = (λx.yx) (Eta conversion)

We can apply these in reverse to convert a lambda expression into combinators. Note that the final rule can convert longer expressions - for example, λ x.abcdeg can be converted by setting f = abcde. This will eventually terminate as the third rule reduces the number of applications, so that eventally one of the other rules will take effect and remove the lambdas.

## Example

Consider the following lambda expression, which raises one Church numeral to the power of a second:

λ mn.nm

Recall that this is short-hand for:

λ m.(λ n.nm)

Which by the third rule becomes:

λ m.S(λ n.n)(λ n.m)

Which by the first and second rules becomes:

λ m.S(SKK)(Km)

Which by the third rule becomes:

S(λ m.S(SKK))(λ m.Km)

Then by the fourth rule, the last statement becomes K:

S(λ m.S(SKK))K

Then by the first rule, the statement becomes:

S(K(S(SKK)))K

Which is the combinator form of (λmn.nm).

## See Also

## External resources

- wikipedia:SKI combinator calculus
- David Madore's original description of the Unlambda language
- Raymond Smullyan,
*To Mock a Mockingbird*