S and K Turing-completeness proof

From Esolang
Jump to navigation Jump to 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

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

Retrieved from "https://esolangs.org/w/index.php?title=S_and_K_Turing-completeness_proof&oldid=50517"