Doesn't lambda K-calculus include lambda I-calculus?

87 Views Asked by At

To mock a mockingbird, chapter 18:

From just S and K you can derive any combinatorial bird whatsoever!

Same book, chapter 19

[…] with just the two birds J and I, we would ultimately get the same birds as if we started with B, T, M, and I. The kestrel K would never appear, […], nor would a whole host of birds derivable from S and K.

The theory of combinators derivable from […] J and I -- is technically known as the $\lambda$I-calculus. The theory of combinators derivable from S and K is known as the $\lambda$K-calculus. Neither theory can be said to be "better" than the other; each has applications which the other does not.

So from S and K we can derive any combinatorial bird, whereas from J and I we can derive a lot of birds, but at least not K (nor some birds derivable from S and K). So how is it possible that $\lambda$K-calculus is not better than $\lambda$I-calculus?

1

There are 1 best solutions below

2
On

The $\lambda K$-calculus is actually better because you have the $K$-combinator, so it's much easier to work with since you can discard variables easily. That said, the $\lambda I$-calculus is still Turing equivalent. It can define all computable functions, this is proved in The Calculi of Lambda Conversion - Alonzo Church in the chapter Combinations, Godel Numbers by a recursive translation from lambda terms to the I,J combinator set.