Using Combinators in Lambda Calculus 
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.
 A: 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.
A: 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.
