[Haskell-cafe] MonadFix

[Marc A. Ziegert]

Am Dienstag, 18. Dezember 2007 schrieb Joost Behrends:
<snip>
>    "fix f is the least fixed point of the function f, i.e. the least defined x
> such that f x = x."
> 
> What does "least" mean here ? There is nothing said about x being a variable of
> an instance of Ord. And why fix has not the type a -> (a -> a) -> a, means: How
> can i provide a starting point of the iteration x ==> f x ==> f (f x) ==> ...?  
> 
<snip>

the starting point is "undefined".
the ordering of functions is is_subset_of.


a more detailed explanation:

a function "A -> B" is a subset of the cartesian product "A x B", where for each element in A there is not more than one element in B.
subsets are partially ordered. the empty set (the function "const undefined" or simply "undefined") is the lowest subset, and AxB is the largest (but in most cases not a function).
the function "f0 (_::a) = (undefined::b)" is the lowest subset.
the function "f1 ('x'::a) = (5+fromEnum 'x'::b)" is larger than f0.
the function "f1' ('y'::a) = (7::b)" is larger than f0, and not equal (neither equal, nor lower, nor larger) to f1.
the function "f2 (c::a) | isUpper c = (5 + fromEnum c::b)" is larger than f1, and not equal (neither equal, nor lower, nor larger) to f1'.
the function "fn (c::a) | True = (5 + fromEnum c::b)" is one maximal defined function: it is defined on every input parameter.

now, the "fix" function takes a function "construct_f::(a->a)->(a->a)" and calculates first "(construct_f undefined) :: (a->a)". "undefined :: (a->a)" equals f0, the lowest function/element, but it is not a fixpoint. "construct_f undefined" is a bit more "defined"....
"construct_f . construct_f . construct_f . construct_f . ... (oo times) $ undefined" is the largest thing you can get this way, it does not need to be defined everywhere, but it is a fixpoint. there may be larger fixpoints, but no lower.

example:

fix construct_f
 where construct_f f = \x -> (if x==0 then 42 else f (x-1))

look at "construct_f undefined": it constructs a function which is defined on the input x==0; otherwise it tries to evaluate "undefined (x-1)", which is completely undefined.
look at "construct_f $ construct_f undefined": it constructs a function which is defined on the input x==0 and x==1.

"fix cf = cf (fix cf)" is the fixpoint function, and with this...
"fix construct_f" constructs a function which is defined on all inputs x>=0, but not on inputs x<0. this function is one fixpoint (the least one) of construct_f.
another function is a fixpoint of construct_f: "\x->42". but this is a larger function than the above fixpoint, so this is not the LEAST FIXPOINT; the above one is.
you can test, whether it is a fixpoint: "construct_f (\x->42) == (\x->if x==0 then 42 else (\x->42)(x-1)) == (\x->if x==0 then 42 else 42) == (\x->42)"
exercise1: "construct_f (\x->if x>=0 then 42 else 23) == ...?"
exercise2: "construct_f (\x->if x>=0 then 42 else undefined) == ...?"

another example: lists.

fix (\fibs->1:1:zipWith (+) fibs (tail fibs))



i hope to have helped.
- marc



-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: This is a digitally signed message part.
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20071218/336c2213/attachment.bin