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

Thanks for all comments on my question, especially those bashing my poor code. 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 simply by iterating f, although not necessarily in finite time. Taking the lub of x and the fixed point of f (over bottom) need not give a fixed point even if one exists. Think of reachability in a graph from a starting set. Let S be some fixed set, and let f return all points reachable in 0 or 1 step from the union of S and the argument to f. Then fix f is the set of points reachable from S, which is a fixed point. But adding some point x outside fix f will in general not give me a fixed point, even though a unique fixed point exists (the set reachable from the union of {x} and fix f). Jens