1 A)

not (false) -> true
----------------------------------------------------------------------
and(not(false),and(true,not(true))) -> and (true, and(true,not(true))) 


----------------------------------------------------------
and (true, and(true,not(true))) -> and (true, not (true) ) 

--------------------------------------
and (true, not (true) ) -> not (true))  

---------------------
not (true))  -> false


2 B)

They are not ambiguous.

We have an overlap of the rules for 

if the expression is not(false), two rules could be applied,

not(false) -> ... and not(b)....,
however, since there is no b' such that false -> b', the premise 
of the second rule can't be resolved, so only the first rule can
be applied successfully. 

The same argument applies for the overlapping rules
not(true).. and not (b)... and
and(true,b)... and      and (b1,b2) and
and(false,b) ... and    and (b1, b2)

3 C) 
(We use 'V' to replace the down arrow)
         
   b V true
----------------
not (b)  V false

  b V false
-------------
not (b) V true


b1 V true   b2 V v2
-------------------
and (b1, b2)  V v2


   b1 V false  
--------------------
and (b1, b2)  V false




2 A-i)    see assignment 1
2 A-ii)  
         let f = (fun g x is fun h y is x + y) 10
         in  f 100


3 B) see lecture notes

3 A-i)   unifier exists: [{int/c} {int/a} {int/b}]
3 A-ii)  no unifier exists
3 A-iii) no unifier exists
  
3 B-i)    forall a. forall b. (a + (bool + b))
3 B-ii)   forall a. forall b. forall c. (((a,b) , c) -> b)
3 B-iii)  forall a. (a + a) -> a


3 C)  forall .... takes a pair of values, where both values
have the same, arbitrary type a, and returns a value of this type. 
exists .... takes a pair of values of a fixed (but unknown) type a. 
For any function g of the type, g (true, false) would, for example, be
type correct. The only value we can apply f to (without any further 
knowledge) is error (or other non terminating computations), but no 
'real' value.


4 A-i) see notes
  A-ii) runtime error handling, see notes

  B) co:      product, sum type 
     contra:  function type in first

  C) see discussion in Featherweight Java notes (what is checked
statically, what is checked dynamically?)