<p>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 <em>SKI combinator reduction</em>, and it's naturally lazy. If a normalising reduction sequence exists, then this reduction strategy will find it. </p>

<p>One problem with SKI combinators is that they have the unfortunate property of resulting in an exponential blowout in code size during reduction.</p>

<p>See: </p>

<ul>
<li><p>D.A. Turner. A new implementation technique for applicative languages. Soft. Pract. and Exper., 9, pp. 31-49, 1979.</p></li>
<li><p>Lambda-Calculus and Combinators: An Introduction, Second Edition by J. R. Hindley and J. P. Seldin</p></li>
</ul>

CC BY-SA 2.5
2011-03-05T22:34:01.987Z
2011-03-05T22:55:02.430Z
2011-03-05T22:55:02.430Z
Dave Clarke
<p>Inspired by <a href="https://cstheory.stackexchange.com/questions/3792/are-innermost-reductions-perpetual-in-untyped-calculus">this question</a>, I was curious whether there was a reduction strategy for untyped SKI combinators that was known to be either normalizing or perpetual. </p>

<p>As described <a href="http://en.wikipedia.org/wiki/SKI_combinator_calculus" rel="nofollow noreferrer">here</a> (Twelfed <a href="http://twelf.plparty.org/wiki/Bracket_abstraction" rel="nofollow noreferrer">here</a>), the nondeterminstic rules of the combinator calculus are these:</p>

<p>$Ix \rightarrow x$</p>

<p>$Kxy \rightarrow x$</p>

<p>$Sxyz \rightarrow xz(yz)$</p>

<p>$xy \rightarrow x'y$ if $x \rightarrow x'$</p>

<p>$xy \rightarrow xy'$ if $y \rightarrow y'$</p>

<pl.programming-languages><combinatory-logic>
Is there a normalizing (or perpetual) reduction strategy for untyped combinators?
Rob Simmons
# Is there a normalizing (or perpetual) reduction strategy for untyped combinators?

(Asked by: username_0 on 2011-03-05)

Inspired by [this question](https://cstheory.stackexchange.com/questions/3792/are-innermost-reductions-perpetual-in-untyped-calculus), 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](http://en.wikipedia.org/wiki/SKI_combinator_calculus) (Twelfed [here](http://twelf.plparty.org/wiki/Bracket_abstraction)), 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'$

**Tags:** pl.programming-languages, combinatory-logic


---

## 1 answers

### Answer by username_1 on 2011-03-05. Score: 8 | Accepted answer

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


---

