S and K Turing-completeness proof

From Esolang
Jump to: navigation, search

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[edit]

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[edit]

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[edit]

External resources[edit]