SKI combinator calculus

Remarks

Example: $\mathbf{S}\, \mathbf{K}\, \mathbf{K}$ behaves like $\mathbf{I}$. For every term $M$, $\mathbf{S}\, \mathbf{K}\, \mathbf{K}\, M \to_w \mathbf{K}\, M\, (\mathbf{K}\, M) \to_w M$.

Non-example: $\mathbf{K}\, M$ alone is not a redex. The rule for $\mathbf{K}$ needs two arguments, so $\mathbf{K}\, M$ is in normal form whenever $M$ is.

Combinatory completeness: for each term $M$ and variable $x$ there is a term $[x]M$ without $x$ such that $([x]M)\, N \twoheadrightarrow_w M[x := N]$ for all $N$. One can take $[x]x = \mathbf{I}$, $[x]M = \mathbf{K}\, M$ if $x$ does not occur in $M$, and $[x](M\, N) = \mathbf{S}\, ([x]M)\, ([x]N)$ otherwise. This translates every term of the lambda calculus into an SKI term with the same behavior on arguments.