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
signature.asc
Description: This is a digitally signed message part.
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
