Assignment Number 3 ANSWERS

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)

    \(x,y) f g. ((g (f x)),y)

b)      ('b -> 'a) -> 'c -> ('c -> 'b) -> 'a
   
    \f x g. f (g x)

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

    \x:'a y:('a->void). y x

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

     \f:('a->'b) g:('b->void) x:'a. g (f x)

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)

   \f x. [r=(f x)]

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

   \f. (\a. f [l=a], \b. f [r=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.

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

    Y (\f. (if (f (pre x)) -> false | true) (\f x. f f f x) =
    (see this later)


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

     (\x y. x) = (\*x \*y.x) = (\*x.K x) = S (\*x.K)(\*x.x) =
                 (S (K K) I)

     (\x y. y) = (\*x \*y.y) = (\*x.I) = K I

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))

    NO.  Do the usual translation for the recursive definition.

       and W = Y (\f. (equal f 0 -> 1 | 0)) to establish W's validity.

       Consider the proposition W = 0

       Case 1:  W is 0. (i.e. its true)

              then by the first formula W = (equal 0 0 -> 1 | 0)
                      which reduces to  W = 1
              which means W is not 0, a contradiction.

       Case 2:  W is not 0, call it x (i.e. its false)

              then the first forumla is x = (equal x 0 -> 1 | 0)
                      which reduces to  W = 0
              which means W is 0, a contradiction.

So every case leads to contradiction, our assumption must be wrong.
THEREFORE, there can be no such expression!