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 multiple proofs that the S and K combinators are Turing-complete.
Via lambda calculus
We first show that any expression in Lambda calculus can be converted into the SKI basis. Consider the following compilation scheme [] over lambda terms with constant values c and constant functions f:
λx.c → K c λx.x → I λx.fx → f λx.yz → S [(λx.y)] [(λx.z)]
Note that this can be run in reverse, which we'll call {}:
K c → λx.{c}
I → λx.x
S f g → λx.{f x}{g x}
f → λx.fx
The reader can verify that this is a bijection. So, the undecidability of normalizing lambda-calculus terms is also the undecidability of normalizing combinators in the SKI basis. From here, we can rewrite all I terms to SKK terms and witness the undecidability of normalizing combinators in the SK basis.
External resources
- wikipedia:SKI combinator calculus
- David Madore's original description of the Unlambda language
- Raymond Smullyan, To Mock a Mockingbird