[Haskell-cafe] least fixed points above something

[Dan Doel]

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