Give as simple a set of rules as you can for transforming lambda calculus to a form where there are no bound variables mentioned, but where there are many instances of the three standard combinator constants S, K and I. [6 marks] Describe tree-rewrites suitable for reducing expressions written in terms of combinators. [6 marks] Explain how you might deal with the issue of keeping track of the values of bound variables if you were to interpret lambda calculus directly. [8 marks] For each of the given pairs of terms, give a most general unifier or indicate why none exists. (Here x, y, z are variables while a, b are constant symbols.) h(x, y, z) and h(y, z, u) h(x, y, z) h(x,y,b) and and h(f(y), z,a) h(a,x,y) h(x, y, z) and h(g(y,y), g(z, z), g(u, u)) [4 marks] A standard unification algorithm takes a pair of terms t and t2 and returns a substitution such that t0 = t20. Show how this algorithm can be used to find the unifier of several (n > 2) terms t, t2,..., tn: a substitution such that t0 = t20 == tn0. Indicate how the unifier is constructed from the unifiers of n 1 pairs of terms. (Assume that all required unifiers exist and ignore the question of whether the unifiers are most general.) [6 marks] Prove using resolution the formula (Vx [P(x) (Q(x) AQ(f(x)))])y-P(y) or indicate why this formula is not a theorem. [10 marks]