S and K Turing-completeness proof
From Esolang
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.
[edit] Conversion
We begin by observing the following equivalences:
- Ky = λ x.y
- SKK = λ x.x
- S(λ x.f)(λ x.g) = λ x.fg
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.
[edit] 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(SSK))(λ m.Km)
Several further applications of the third rule result in:
S(S(λ m.S)(S(S(λ m.S)(λ m.S))(λ m.K)))(S(λ m.K)(λ m.m))
Which by the first and second rules becomes:
S(S(KS)(S(S(KS)(KS))(KK)))(S(KK)(SSK))
Which is the combinator form of the original lambda expression.
