On Friday 20 March 2009 2:43:49 am Martijn van Steenbergen wrote:
> Luke Palmer wrote:
> > Well, it's probably not what you're looking for, but to remain true to
> > the domain-theoretical roots of "fix", the "least fixed point above" can
> > be implemented as:
> >
> > fixAbove f x = fix f `lub` x
>
> How can this be right if f is never applied to x? Or maybe you're trying
> to do something other than I think you are, in which case: sorry for the
> confusion. :-)
The "least" in least fixed point is not according to, say, usual numeric
ordering. It's the (partial) ordering of definedness. So, for a typical
numeric type, this ordering looks like:
1) _|_, the undefined element, is less than every other value
2) All other values are not comparable to each other.
So, iterating a function from a defined starting value finds a fixed point
(maybe), but that fixed point is not less or greater than any other number, as
far as the ordering of definedness is concerned. Luke's function, however:
fixAbove f x = fix f `lub` x
finds the least defined upper bound of 'fix f' and 'x' via some threading and
IO magic. With it you can do stuff like:
fixAbove id 5 = fix id `lub` 5
= _|_ `lub` 5
= 5
(Assuming fix id returns _|_ in a way that the library can detect.) And
indeed, id 5 = 5, 5 <= 5, and 5 is the least defined such value.
More interesting cases occur when you can have partially defined values.
Consider lazy naturals:
data Nat = Z | S Nat
_|_ < Z
forall n :: Nat. _|_ < S n
forall m, n :: Nat. m < n -> S m < S n
Which means we now have more structure, like '_|_ < S _|_ < S (S _|_) < ...'.
Of course, all totally defined values are still incomparable to one another.
However, to answer Luke's wonder, I don't think fixAbove always finds fixed
points, even when its preconditions are met. Consider:
f [] = []
f (x:xs) = x:x:xs
twos = 2:twos
Now:
fix f = _|_
2:_|_ < twos
f twos = f (2:twos) = 2 : 2 : twos = twos
So twos is a fixed point of f, and greater than 2:_|_, but:
fixAbove f (2:_|_) = fix f `lub` (2:_|_)
= _|_ `lub` 2:_|_
= 2:_|_
so we have failed to find the least fixed point above our given value. I think
fixAbove is only successful when one of the following conditions is met:
1) fix f = _|_ and x is a fixed point of f (maybe fix f < x works, too)
2) x < fix f
But neither of those cases are particularly novel, unfortunately.
Anyhow, hope that helps a bit.
-- Dan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
