Using Combinators in Lambda Calculus

Question

K $\equiv$ $\lambda$xy.x

S $\equiv$ $\lambda$xyz.((xz)(yz))

Prove that the identify function I $\equiv$ $\lambda$x.x is equivalent to ((S K) K)

I have no clue where to even start for this problem, could someone possibly guide me into solving this problem, it is for final preparation.

Answer 1

Well, start by writing down $((SK)K)$. Then, replace 'S' and 'K' with those definitions above. You'll get some lambda term, like this one: $([λxyz.((xz)(yz))][λxy.x])[λxy.x]$. The task is then to reduce that term until you get $[λx.x]$. Here's a way it might be reduced. Start with the initial term:

$$([λxyz.((xz)(yz))]~[λxy.x])~[λxy.x]$$

We want to reduce $([λxyz.((xz)(yz))]~[λxy.x])$, but $y$ is bound in $[λxyz.((xz)(yz))]$ and free in $[λxy.x]$, so we don't want it to be captured when we substitute the terms. Therefore, we rename things to avoid that, obtaining the following equivalent term ($w$ substituted for the bound $y$):

$$([λxwz.((xz)(wz))]~[λxy.x])~[λxy.x]$$

Now we can evaluate the first redex to obtain:

$$([λwz.(([λxy.x]z)(wz))])~[λxy.x]$$

One way of proceeding now is to reduce that inner redex on the left, obtaining:

$$([λwz.([λy.z](wz))])~[λxy.x]$$

Once more we reduce the inner redex, obtaining:

$$([λwz.z])~[λxy.x]$$

If you're surprised what happened, notice that $[λy.z]$ was a constant function. Final reduction:

$$(λz.z) \equiv_{\alpha} (λx.x)$$

Again, $([λwz.z])$ was a constant function, so the argument got discarded.

Answer 2

Here's another way to think about these sorts of problems. This is basically the same as Hunan's solution but I think it helps to be able to keep things in the S K notation when possible; I get a better intuition about the solution that way.

Pick any combinator, say, A. What is ((SK)K)A?

Start from the inside. What is SK? Substitute K for x in $\lambda$xyz.((xz)(yz)) and we get

SK = $\lambda$yz.((Kz)(yz)).

What is Kz? It's the combinator that takes anything and gives you back z. What are we supplying as the argument to that combinator? We don't care! The result is z regardless. So

SK = $\lambda$yz.z.

OK, that's the interior. What argument are we giving to that combinator? K. Substitute K for y and get $\lambda$z.z because there is no y in the right side.

Now give argument A to that. Substitute A for z to get A.

We started with arbitrary A and got A, so this must be the identity combinator.

Did you notice something interesting there? Since there was no y on the right side we could have substituted anything in there! That is to say that we've just proven that

((SK)B)A == A

for any values of A and B and therefore ((SK)B) gives I for any B.

Note the points of my method here.

• I chose a concrete arbitrary value A for the combinator to operate on.
• I worked from inside to outside
• I understood the meaning of Kz rather than treating it formally, and that enabled me to more quickly reason about its action.

Note also that you have a new tool in your toolbox. You started with K as the combinator that takes something and constructs a combinator that always yields that something regardless of input. You learned that SK is the combinator that constructs I regardless of input.

Another way to look at it is K is the combinator that takes two values and gives you the first; SK is the combinator that takes two values and gives you the second. Both these are powerful intuitions that will help you reason about combinators.