[Haskell-cafe] least fixed points above something

[Jens Blanck]

>
>
> On Friday 20 March 2009 5:23:37 am Ryan Ingram wrote:
> > On Fri, Mar 20, 2009 at 1:01 AM, Dan Doel <dan.doel at gmail.com> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090323/03aa7408/attachment-0001.htm