[Haskell-cafe] least fixed points above something
holgersiegel74 at yahoo.de
Mon Mar 23 11:27:56 EDT 2009
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
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
More information about the Haskell-Cafe