1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.