Evaluating SKI-combinators with not enough arguments

Question

I was tasked with showing that

S(KK)I = K

Now since S takes three arguments, I was simply stuck at the beginning not knowing how to tackle this. I see two arguments, namely (KK) and I but there is no third one I can "spot". What happens in this situation? It sort of worked for me already by just leaving out the z in S x y z = xz(yz), which yielded KK(I) and as a consequence K. It just seems wrong to me though so I want to ask here. Is this the right way of going about it?

I also dont understand what happens with KI for example as K also needs two arguments and only gets I. Is my solution right or do I have to go about it differently?

Answer 1

The simplest way to solve your question is the use of eta-conversion. Namely, every term M behaves like a term (λx.M x) (of course, x cannot be free in M). Thus, if the combinators you want to evaluate lack some arguments, you can eta-convert the term and then apply these combinators.

Given your example, you need two eta-conversions. The reductions after the first one are given below.

S(KK)I -> λx.S(KK)Ix -> λx.KKx(Ix) -> λx.K(Ix) 

Now you have the outer combinator K that lacks the second argument. If you eta-convert the outermost term: λy.(λx.K(Ix)) y, you will get λy.K(Iy), which is not very amusing. But you can apply eta-conversion to a subterm of the term, e.g. a body of lambda abstraction. Thus, you can convert λx.K(Ix) to λx.(λy.K(Ix) y). That results in λx.λy.Ix, which reduces to λx.λy.x, and this term is a definition of K combinator. Voila!

In fact, you can prove equivalence of combinators without using eta-conversion, but then you need to use some not-very-friendly axioms as rewriting rules (for details, see Chapter 7 of Henk P. Barendregt (1984). The Lambda Calculus: Its Syntax and Semantics).

Answer 2

The way I think of this is that S(KK)I is a function that takes a single argument - call it z. What happens when we invoke this function with an arbitrary z?

S(KK)Iz -> KKz(Iz) -> Kz

So invoking S(KK)I with z is exactly the same as invoking K with z. Therefore, S(KK)I and K are the same function.

Answer 3

This is, in effect, what Combo (which I put up on GitHub) does when it's run with extensionality turned on:

    S (K K) I
    = λx·S (K K) I x        ⇒       λx·K K x (I x)  ⇒       λx·K (I x)      
    = λx·λy·K (I x) y       ⇒       λx·λy·I x       ⇒       λx·λy·x
    = λx·K x
    = K

The steps it actually shows are:

    S (K K) I #0 => K K #0 (I #0)
    K K #0 => K
    K (I #0) #1 => I #0
    I #0 => #0
    K