SKI combinator calculus

Summary

The SKI combinator calculus is a model of computation built from three constants $\mathbf{S}$, $\mathbf{K}$ and $\mathbf{I}$ and application, without bound variables. Its rules are $\mathbf{I}\, x \to x$, $\mathbf{K}\, x\, y \to x$ and $\mathbf{S}\, x\, y\, z \to x\, z\, (y\, z)$. Every term of the lambda calculus can be translated into it, so it is Turing complete. It goes back to Moses Schönfinkel and Haskell Curry, and it is the basis of combinatory logic.