Programming Language Concepts
                          Jan-Apr 2009
                          Assignment 5

		   Due Monday, 20 April, 2009

NOTATION: 
  Use the Haskell notation \ for the greek letter lowercase
  lambda when writing expressions in the lambda calculus.
  Similarly, use /\ for capital lambda, used in the 2nd order
  polymorphic typed lambda calculus.

  Submit your solution by email, typed as plain text using the
  convention above.

In the untyped lambda calculus, let <n> be the Church numeral
encoding of the number n --- that is, 
 
     <n> =\fx. (f^n x).  

Also, let

     <true> = \xy.x
     <false> = \xy.y
     <if b then x else y> = \bxy.bxy

1. Verify that \pq. (pq) encodes the exponentiation function for
   Church numerals.
                                
2. Find an encoding for the predecessor function given by:

          pred(0) = 0
          pred(n) = n-1 for n > 0

3. Write an expression in the 2nd order polymorphic typed lambda
   calculus corresponding to the Haskell function.

          twice f x = f (f x)

   Derive its type using the type inference rules for the 2nd
   order polymorphic typed lambda calculus.

4. Unify the following pairs of formulas, if possible.  Explain
   your answer in terms of the unification algorithm discussed in
   class. 

   (a) p(x,g(f(a)),f(x)) and p(f(y),z,y) 
   (b) p(a,x,f(g(y))) and p(z,h(z,u),f(u))