<p>In the Wikipedia page on the SKI combinator calculus, an example is given of two equivalent reductions of the expression <code>SKI(KIS)</code> [0].</p>
<p>In both cases, <code>SKI(KIS)</code> reduces to <code>I</code>. However, in the first reduction, an additional value <code>x</code> is introduced to &quot;complete&quot; the arguments for the <code>K</code> combinator. That is reduction proceeds:</p>
<ol>
<li><code>SKI(KIS)</code></li>
<li><code>K(KIS)(I(KIS))</code></li>
<li><code>K(KIS)x</code> &lt;- introduction of <code>x</code></li>
<li><code>KIS</code></li>
<li><code>I</code></li>
</ol>
<p><strong>What reduction rule permits the introduction of this additional value?</strong> Without it, the reduction would end with <code>KI</code> (the inner <code>KIS</code> term would reduce to <code>I</code>, but the outer <code>K</code> would not have a second argument to complete its evaluation).</p>
<p>In the second reduction, all combinators have fully populated arguments at every step of the deduction.</p>
<p>When considered as lambda terms, <code>K</code> = <code>\x.\y(x)</code>. <code>K(KIS)</code> in turn is <code>\x.\y(x)(KIS)</code>, which reduces to <code>\y(KIS)</code>, thence <code>\y(I)</code>. This abstraction over <code>I</code> then requires an additional application, against any value, to force the lambda function to yield <code>I</code>. 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).</p>
<p>This same question of when the arguments of a combinator are &quot;fully populated&quot;, 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.</p>
<p>[0] <a href="https://en.wikipedia.org/wiki/SKI_combinator_calculus#Examples_of_reduction" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/SKI_combinator_calculus#Examples_of_reduction</a></p>

CC BY-SA 4.0
2024-07-06T03:39:39.873Z
There is no reduction there, they just rename `I(KIS)` to `x`
Command Master
CC BY-SA 4.0
2024-07-06T07:33:05.763Z
Indeed. But it’s confusing, nonstandard, and unhelpful, hence I’ll remove it.
Emil Jeřábek
<combinatory-logic>
What rules govern when combinators (e.g. S, K, and I) can be only partially applied?
jpt4
# What rules govern when combinators (e.g. S, K, and I) can be only partially applied?

(Asked by: username_0 on 2024-07-06)

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>

**Tags:** combinatory-logic
> **Comments:**
> **username_1**: There is no reduction there, they just rename `I(KIS)` to `x`  
> **username_2**: Indeed. But it’s confusing, nonstandard, and unhelpful, hence I’ll remove it.  

---

## 0 answers

