Due on Friday, October 5, 5pm.

Domains and Least Fixed Points

1. Consider the flat domain of Booleans (B_{_|_}).  How many functions are in the set B_{_|_} -> B_{_|_}?  How many functions are in the domain [ B_{_|_} -> B_{_|_} ] of continuous functions?  Draw the elements of the latter in a graph showing the information ordering.
    
2. Consider this recursive definition of the exponentiation function in Haskell:

   exp x 0 = 1
   exp x n = x * exp x (n-1)

   Rewrite it in a non-recursive way using the function y defined by:

   y f = f (y f)
    

3. Consider this alternative definition of y:

   y' f = x where x = f x

   Prove that y = y'.
    

4. Consider the equations:

   x = if x then True else False
   x = if x then False else True

   How many fixed points does each equation have? What are their least fixed points?
    

5. Note that the least fixed-point (LFP) of any strict function is _|_ (because f _|_ = _|_).  Use this result to explain why the LFP of:

   x = 1 + x

   is _|_, whereas the LFP of:

   x = 1 : x

   is not.
    

6. y is a "fixed point operator", in that it returns the fixed point of its argument.  Prove that every fixed point operator is a fixed point of:

   z = \y-> \f-> f (y f)

   Of course, every fixed point operator is also a fixed point of the identity function (which has an infinite number of fixed points)!  So perhaps z is not so special... But in fact it is: Prove that, if g is any fixed point operator, then g z is also a fixed point operator.

Solution.