[Haskell-cafe] least fixed points above something

[Holger Siegel]

Am Montag, den 23.03.2009, 12:55 +0000 schrieb Jens Blanck:

> The above approach does not apply to my case. What I have is a
> monotone function f on a partial order satisfying f x >= x, for all x.
> Given that the partial order is in fact a cpo this is enough to
> guarantee that a least fixed point can be found above any point in the
> partial order

....which implies that every total value is a fixed point.

> > simply by iterating f, although not necessarily in finite time.

Since every total value is a fixed point of f, the infimum of all total
values above x is an upper bound for the least fixed point above x. This
upper bound can be found the following way:

1) Find a position p in x at which the value is bottom::T, such that
   type T has exactly one constructor. If there is no such position, you
   are ready.

2) If T has exactly one constructor, then replace the value at position
   p with that constructor, leaving the constructor arguments undefined
   for now. Go on with step 1.

Let's call this upper bound y and assume a function glb that calculates
the greatest lower bound of two values. Then you can 'frame' a value v
into the interval [x, y] via the expression ((v `glb` y) `lub` x). This
works, because y >= x implies that (v `glb` y) and x have an upper bound
in the CPO.  Also, function

f' v = ((f v `glb` y) `lub` x)

is monotonic and expanding on the interval [x, y]. So we get:

fixAbove f x = fix f'
	where f' v = (f v `glb` y) `lub` x
              y    = ... -- see above

Regards,

Holger