# [Haskell-cafe] least fixed points above something

Dan Doel dan.doel at gmail.com
Fri Mar 20 04:01:56 EDT 2009

```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
```