CPSC 430/530
                           Formal Semantics

                            Problem Set 3
                             Solution Set

                        Prepared by Paul Hudak
                           October 9, 2007



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.

B_|_ contains 3 elements.  Therefore there are 3^3 = 27 functions in
B_|_ -> B_|_.  However, only 11 of these are continuous:

-- If _|_ maps to _|_, then True and False can map to anything, which
   yields 3^2 = 9 continuous functions.

-- If _|_ maps to True, then so must True and False, which is one more
   function.  Analogously we get one more function if _|_ maps to
   False.

Let's represent functions in terms of the results they produce for _|_
(B), True (T), and False (F).  For example, the _|_ function would be
BBB, the identity function BTF, the constant True function TTT, etc.
Then we have this ordering:


  TTT       FFF
   |         |
   |         |
  BTT  BTF  BFF  BFT
   ||  ||  / |    |\
   ||  ||_|__ \__ | \
*  | \_|__|_ |   ||  *
 \ |   | /  ||   ||
  BBT  BBF  BTB  BFB
      \  |   |  /
          BBB


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)

We can first rewrite exp this way:

  exp = \x -> \n -> if n==0 then 1 else x * exp x (n-1)

Then we abstract away exp on the RHS, and apply y:

  exp = y (\exp -> \x -> \n -> if n==0 then 1 else x * exp x (n-1))


3. Consider this alternative definition of y:

      y' f = x where x = f x

   Prove that y = y'.

If y = y' then it must be that y f = y' f for all f.  But note the
solution to x = f x is y (\x -> f x), or y f.  So:

  y' f = y f

and we are done.


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?

As mentioned in class, instead of "how many fixed points", the problem
should probably ask "how many solutions".  As mathematical equations,
the first one has three solutions (_|_, True, and False), whereas the
second one has one (_|_).  In both cases, the least fixed point is
_|_, and indeed if we type these equations into Haskell the program
will diverge.
       

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.

The function (+) is strict in both of its arguments; that is, _|_ + x
= x + _|_ = _|_ for any x.  Therefore the function \x -> 1+x is
strict.  Its least fixed point is the solution to the above equation,
but the least fixed point of a strict function is _|_, and therefore
the least solution to that equation is _|_.

In contrast, (:) is not strict in either of its arguments.  _|_ : xs
is not the same as _|_, nor is x : _|_.  The best way to think about
something like _|_ : xs is as a list data structure in which we know
that the list has at least one element, but we don't know what that
first element is.  This is very different from knowing nothing at all.
       

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.

Suppose g is a fixpoint operator.  Then:

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

Furthermore:

g z f = z (g z) f
      = f (g z f)

QED