1.

(a)
	(\x y -> x y) (\v -> v u) (\x -> x)
-->	(\v -> v u) (\x -> x)
-->	(\x -> x) u
-->	u

(b)
	(\x y -> x y)((\v -> v u)(\x -> x))
-->	(\x y -> x y) ((\x -> x) u)
-->	(\x y -> x y) u
-->	(\y -> u y)

(c)
	(\x -> x (x (y z))x) (\u --> uv)
--> (\u --> uv) ((\u --> uv) (y z)) (\u --> uv)
--> (\u --> uv) (yzv) (\u --> uv)
-->	y z v v (\u --> uv)

(d)
	(\x -> x x y)(\u -> u z)
--> (\u -> u z) (\u -> u z) y
-->	(\u -> u z) z y
--> z z y

(e)
	(\v w -> v w w) (\u -> u y x)
-->	(\w -> ((\u -> u y x) w w))
-->	(\w -> w y x w)

------------------------------------------------------------------------------------

2.
Define F := (\p -> <pair> (<succ> (<fst> p)) (<plus> (<succ> (<fst> p)) (<snd> p))).
Then define <S> := (\x -> (<snd> (x F (<pair> <0> <0>)))).
We prove the correctness using induction. 
Claim is F^{n} (<pair> <0> <0>) --> <pair> <n> <0 + 1 + 2 + ... + n> for all n >= 0.

Base case: n=0. 
Then (F^{0} (<pair> <0> <0>)) --> (<pair> <0> <0>) which is as required.

Inductive step: Suppose the claim is true for n = k. That is, F^{k} (<pair> <0> <0>) --> <pair> <k> <0 + 1 + ... + k>.
Then 
F^{k+1} (<pair> <0> <0>) = F (F^{k} (<pair> <0> <0>)) 
-->_{IH} F (<pair> <k> (<0 + 1 + 2 + ... + k>)) 
--> <pair> (<succ> <k>) (<plus> (<succ> <k>) <0 + 1 + 2 + ... + k>)
--> <pair> <k+1> (<plus> <k+1> <0 + 1 + 2 + ... + k>)
--> <pair> <k+1> <0 + 1 + 2 + ... + k + (k+1)>

And so we have 
<S> <n> --> (<snd> (<n> F (<pair> <0> <0>))) --> (<snd> (F^{n} (<pair> <0> <0>))) -->_{proved} (<snd> (<pair> <n> <0 + 1 + ... + n>)) = <0 + 1 + ... + n>.


------------------------------------------------------------------------------------

3.

(a) null := (\f -> f (\u v -> <false>) <true>)
Then null [] --> (\x y -> y) (\u v -> <false>) <true> --> true.
And null H:T --> (\x y -> x H T) (\u v -> <false>) <true> --> (\u v -> <false>) H T --> <false>.

(b) head := (\x -> x (\u v -> u) (\y -> y))
Then head H:T = (\x y -> x H T) (\u v -> u) (\t -> t) --> (\u v -> u) H T--> H.

(c) tail := (\x -> x (\u v -> v) (\y -> y))
Then tail H:T = (\x y -> x H T) (\u v -> v) (\t -> t) --> (\u v -> v) H T --> T.

------------------------------------------------------------------------------------

4.

(a) \x y -> y x
x : a 
y : (a -> b)
Then y applied to x (i.e. yx) has type b.

(b) \x y z -> x z (y z)
x : (a -> b -> c)
y : (a -> b)
z : a
Then xz : (b->c) and yz : b. So xz(yz) = (xz)(yz) : c. 

(c) \x y z -> x z y
x : (a -> b -> c)
y : b
z : a
Then (xz) : (b->c). So xzy = (xz)y : c.

(d) \x y z -> y (x y z)
x : ((b -> c) -> a -> b)
y : (b -> c)
z : a
Then xy : (a->b) whence xyz : b. So y(xyz) : c.

(e) \x y -> y (\z -> x)
x : a
y : ((b -> a) -> c)
Then (\z->x) : b->a. So y(\z->x) : c.


------------------------------------------------------------------------------------

5. Name the lines in thread A as A1, A2, A3 and in thread B as B1, B2, B3.

(a) A1, B1, A2, B2, A3, B3
(b) A1, B1, A2, B2, B3, A3
(c) A1, A2, A3, B1, B2, B3
(d) B1, A1, B2, A2, B3, A3



Argument that x+y is always even (finally):

Assume that B3 is executed after A3. We can assume this without loss of generality because even though A and B are not symmetric (look at A2 vs B2), we will just use the fact that B2 (respectively A3) makes y (respectively x) even. So B3 (resp A3) is the last step.

So B2 was executed sometime before. Just after B2 executes, y becomes even, say 2k, and finally (after non-negative number of steps) on execution of B3, the final value of y is 2k-m (where m is the final value of x; there are no changes made to x just when B3 is starting). After all steps are executed, we have y+x = 2k-m+m = 2k which is even.