| |
Due on Friday, October 5, 5pm.
Domains and Least Fixed Points
- 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.
- 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)
- Consider this alternative definition of
y:
y' f = x where x = f
x
Prove that
y = y'.
- 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?
- 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.
- 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.
|