Assignment Number 3

Please remember, while you are allowed to discuss the problem
definition and design issues with your peers, your solution to
these task should be your own!

1. Write lambda calculus expressions (using no constants of a 
non-parametric type) with the following types:

a)      ('a,'b) -> ('a -> 'b) -> ('b -> 'c) -> ('c,'b)

b)      ('b -> 'a) -> 'c -> ('c -> 'b) -> ('c -> 'a)


2. Imagine that we define a new type void (the type with no
values), and that we abbreviate a function from 'a -> void,
!'a.  Write expressions with the following types:

a)     'a -> !!'a

b)     ('a -> 'b) -> !'b -> !'a

3.  Now consider another type constructor "+"--disjoint union.
'a + 'b is the type which contains the union of the values in
each type, where each value is tag with the set it came from
(we will use l [left] for the first type, and r [right] for the second).

So, if E is an expresion of type 'a, then [l=E] is of type 'a + 'b,
and if E' is an expression of type 'b then [r=E] is of type 'a + 'b.

(e.g.  type:  'a -> ('a + 'b)    expression:  \x.[l=x]

Write expressions with the following types:

a)  ('a -> 'c) * 'a -> ('b + 'c)

b)  !('a + 'b) -> (!'a * !'b)


4) Consider the following definition:

       odd = \x. (if (odd (pre x)) -> false | true)

Obviously, this definiton is not legal (since it uses itself).
Using the Y combinator, construct a legal definition of odd.

Then expand out (odd 3) and make sure your definition works.


5)  Computer the equivalent combinators for the fst and snd
expressions. 

6) Can there be a lambda expression that meets the following
defintion:
                     / true        if E1=E2
      equal E1 E2 = |
                     \ false       otherwise


(HINT:  consider the formula W = (equal W 0 -> 1 | 0))

This assignment is due in class by 11/26/96 (so I can squeeze
one more in before the end of class...)