Answer to the First Test (FA96)

1a)  datatype command = skip |
                        assign string * atype |
                        sequence of command * command |
                        ifexp of bexp * command * command;

 b)  fun cexp skip state = state |
         cexp (assign (x,y)) state = update state x (aexp y state) |
         cexp (sequence (c1,c2)) state = cexp c2 (cexp c1 state) |
         cexp (ifexp (b,c1,c2)) state = if (bexp b state)
                                         then (cexp c1 state)
                                         else (cexp c2 state);

2a)  (\x.x x)(\x.x x) only reduces to itself (technically speaking the
                      problem is impossible)

 b)  (\x y z. x (y x z) y)(\x y.y)(\x y.x)u =
     (\y z.(\x y. y) (y (\x y.y) z) y)(\x y.x)u =
     (\z.(\x y.y) ((\x y.x)(\x y.y) z)(\x y.x))u =
     (\x y.y)((\x y.x)(\x y.y)u)(\x y.x) =
     (\x y.y)((\y.(\x y.y))u)(\x y.x) =
     (\x y.y)(\x y.y)(\x y.x) =
     (\y.y)(\x y.x) =
     (\x y.x)

 c)  (\x y.y)((\x.x x)(\x.x x))(\x y.y) =
     (\y.y)(\x y.y) =
     (\x y.y)

3)  since we're in the middle of an induction, we assume the property
    holds for arbitrary b0,b1 both boolean expressions.

    ==>  assume we have a derivation (operational) for an and expression.
         then, we must have derivations  -> t0 and  -> t1.

	 by the I.H. B [|b0|] = {(s,t0)} and
                     B [|b1|] = {(s,t1)}
     
         by the "and" denotation rule

		B [| b0 ^ b1 |] = {(s,t0 ^ t1) | ((s,t0) mem B[|b0|]) and
                                                 ((s,t1) mem B[|b1|])}

    <==  assume we have a denotation for the "and" expression.
         then we must have  B [|b0|] = {(s,t0)} and
                     	    B [|b1|] = {(s,t1)}
     
	 by the IH we have  -> t0 and
                            -> t1

         and by the "and" derivation rule

	 -> t0    -> t1
        ___________________________      where t= t0 ^ t1
            -> t        


      QED.


4)  let addfn = \f m n.(iszero m -> n | (suc (f (pre m) n)))

5)  prove (add (suc a) b) = (suc (add a b))

    by induction on b

    base:  b=0
           
       (add (suc a) 0) = (suc (add a 0))
       (suc a)         = (suc a)          (apply defn of "add" on
                                             both sides)

    induction:  b=(suc k)

	IH:  (add (suc a) k) = (suc (add a k))

        (add (suc a) (suc k)) = (suc (add a (suc k)))
        (suc (add (suc a) (pre (suc k)))) = (suc (add a (suc k))) 
                                             --defn of add
        (suc (add (suc a) k)) = (suc (add a (suc k))) 
                                             --by pre-suc rule
        (suc (add (suc a) k)) = (suc (suc (add a (pre (suc k))))) 
                                             --defn of add
        (suc (add (suc a) k)) = (suc (suc (add a k)))
	                                     --by pre-suc rule
        (suc (suc (add a k))) = (suc (suc (add a k)))
                                             --by IH

6) "be somebody else"