In the Wikipedia page on the SKI combinator calculus, an example is given of two equivalent reductions of the expression SKI(KIS) [0].

In both cases, SKI(KIS) reduces to I. However, in the first reduction, an additional value x is introduced to "complete" the arguments for the K combinator. That is reduction proceeds:

  1. SKI(KIS)
  2. K(KIS)(I(KIS))
  3. K(KIS)x <- introduction of x
  4. KIS
  5. I

What reduction rule permits the introduction of this additional value? Without it, the reduction would end with KI (the inner KIS term would reduce to I, but the outer K would not have a second argument to complete its evaluation).

In the second reduction, all combinators have fully populated arguments at every step of the deduction.

When considered as lambda terms, K = \x.\y(x). K(KIS) in turn is \x.\y(x)(KIS), which reduces to \y(KIS), thence \y(I). This abstraction over I then requires an additional application, against any value, to force the lambda function to yield I. However, it is not clear to me why this additional value introduction is allowed, given that it was not a part of the original expression, and combinator calculus terms are supposed to be closed (i.e., containing no free variables).

This same question of when the arguments of a combinator are "fully populated", and what to do when they are not, has arisen in several places in my reading about the system; if there is a standard convention, or additional evaluation rules usually elided for purposes of clarity, making such explicit would be greatly appreciated.

[0] https://en.wikipedia.org/wiki/SKI_combinator_calculus#Examples_of_reduction

  • 3
    $\begingroup$ There is no reduction there, they just rename I(KIS) to x $\endgroup$ Commented Jul 6 at 3:39
  • 1
    $\begingroup$ Indeed. But it’s confusing, nonstandard, and unhelpful, hence I’ll remove it. $\endgroup$ Commented Jul 6 at 7:33


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.