Re: [Haskell-cafe] least fixed points above something

On Friday 20 March 2009 5:23:37 am Ryan Ingram wrote:

On Fri, Mar 20, 2009 at 1:01 AM, Dan Doel wrote:

...

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

How about

...

fixAbove f x = x `lub` fixAbove f (f x)

Probably doesn't work (or give good performance) with the current implementation of "lub" :)

But if "lub" did work properly, it should give the correct answer for fixAbove f (2:undefined).

This looked good to me at first, too (assuming it works), and it handles my first example. But alas, we can defeat it, too: f (x:y:zs) = x:y:x:y:zs f zs = zs Now: f (2:_|_) = _|_ f _|_ = _|_ fix f = _|_ fixAbove f (2:_|_) = 2:_|_ `lub` _|_ `lub` _|_ ... = 2:_|_ Which is not a fixed point of f. But there are actually multiple choices of fixed points above 2:_|_ f (2:[]) = 2:[] forall n. f (cycle [2,n]) = cycle [2,n] I suppose the important distinction here is that we can't arrive at the fixed point simply by iterating our function on our initial value (possibly infinitely many times). I suspect this example won't be doable without an oracle of some kind. Ah well. -- Dan