Inspired by this question, I was curious whether there was a reduction strategy for untyped SKI combinators that was known to be either normalizing or perpetual.
As described here (Twelfed here), the nondeterminstic rules of the combinator calculus are these:
$Ix \rightarrow x$
$Kxy \rightarrow x$
$Sxyz \rightarrow xz(yz)$
$xy \rightarrow x'y$ if $x \rightarrow x'$
$xy \rightarrow xy'$ if $y \rightarrow y'$
SKI combinators were used as the implementation technique for Miranda, a lazy functional language developed by David Turner. The reduction strategy you are after is simply to perform the reductions left to right (aka normal order or call-by-name reduction). This is called SKI combinator reduction, and it's naturally lazy. If a normalising reduction sequence exists, then this reduction strategy will find it.
One problem with SKI combinators is that they have the unfortunate property of resulting in an exponential blowout in code size during reduction.
See:
D.A. Turner. A new implementation technique for applicative languages. Soft. Pract. and Exper., 9, pp. 31-49, 1979.
Lambda-Calculus and Combinators: An Introduction, Second Edition by J. R. Hindley and J. P. Seldin
