Some Problems to Study By (CMSC 631)

1.  Lambda Calculus Simplification

a) add 3 5 = 8
b) snd(e1,e2) = e2
c) (\x y z.y)(\f.(\x.f (x x))(\x.f (x x)))((\x y.x)u v)((\y.y y)(\y.y y))


d) add 0 n = n
e) pre (suc n) = n


2.  Lambda Calculus Definitions

a) implies

b) minus

c) eq (such that eq m n = (iszero m -> n | (iszero n -> false | 
                                                   eq (pre m) (pre n))))

3. Random Lambda

a) Y1 = Y (\y f. f (y f)) 

	show that Y1 E = E (Y1 E) for any E

b) LET uncurry = (\f p.(f (fst p) (snd p)))

	show that if sum = (uncurry add)
                 then sum(m,n) = m+n

4.  Denotation/Operational

a) Work out the whole proof the equivalence of the two semantic
   schemes.  

   (or pick out some important cases, e.g. less-than-or-equal,
                                           multiply,
	                                   if-then-else)

b) Exercise 5.9 (page 68) in the book.

c) Exercise 2.5 (page 19) in the book.


5.  Inductions

	(add x y) = (if (y=0) then x else (suc (add x (pre y))))

	(pre (suc x)) = x

	(mult m n) = (if (n=0) then 0 else (add m (mult m (pre n))))

SHOW:

a) (add 0 x) = x   (this looks trivial.  While its pretty easy, it
		    is _not_ trivial.  You gotta work it out.)

b) (add a b) = (add b a)    (N.B. you may use earlier proofs 
                                  as rules)

c) (add a (add b c)) = (add (add a b) c)   (pick the right variable!)


d) (mult 0 x) = 0

e) (mult 1 x) = x


f) (add (suc r) s) = (add r (suc s))   (you might be able to avoid 
                                       induction here, due to 
                                       earlier rules)


g) (mult (suc k) x) = (add x (mult k x)) 


h) (mult x y) = (mult y x)             (you will have to explicitly 
	                                use rules c,g [at least])