[Haskell-cafe] least fixed points above something

[Luke Palmer]

2009/3/19 Jens Blanck <jens.blanck at gmail.com>

> Hi,
>
> I found myself writing the following
>
> leastFixedPoint :: (Eq a) => (a -> a) -> a -> a
> leastFixedPoint f x = fst . head . dropWhile (uncurry (/=)) $ zip l (tail
> l)
>     where l = iterate f x
>
> and was a bit surprised that I couldn't get any matches on hoogle for the
> type above. The closest one is fix :: (a -> a) -> a but that sort of assumes
> that we're starting the fixed point search from the bottom element
> (undefined).
>
> Anyway, is there a nicer way of doing the above?


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

Where lub is from the "lub" package on Hackage.  This function has the proof
obligation that there is in fact any least fixed point above x (otherwise
results are non-deterministic).

It still needs to be proven that fixAbove always returns a fixed point
(given the precondition).  I can kinda see how it would, but I can't be sure
that it does.

Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090319/d5825ddc/attachment.htm