Why SKI when SK is complete

170 Views Asked by At

Why people talk about SKI calculus when S and K combinators can be used to create any other combinator including I?

1

There are 1 best solutions below

2
On

As was mentioned in comments, S, K and I correspond exactly to what is needed to prove abstraction elimination, in the nice tidy sense that each case syntactical case in the induction step has exactly one combinator that handles that case alone.

Apart from that, however, one can also argue that I is more fundamental than the two other operators. It would be a very strange logic that didn't prove $A\to A$, but logics that reject S or K do exist. Linear logic, for example, rejects both; S because it corresponds to duplication of resources and K because it throws resources away.

So when describing a set of combinators, it is easier and more convenient to say, "yes of course we have I" than to let the reader spend energy on figuring out how I can be made from other available combinators.