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 dan.d...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
Am Montag, den 23.03.2009, 12:55 + 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 are ready. 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 Regards, Holger ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
Luke Palmer wrote: 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 How can this be right if f is never applied to x? Or maybe you're trying to do something other than I think you are, in which case: sorry for the confusion. :-) Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
On Friday 20 March 2009 2:43:49 am Martijn van Steenbergen wrote: Luke Palmer wrote: 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 How can this be right if f is never applied to x? Or maybe you're trying to do something other than I think you are, in which case: sorry for the confusion. :-) The least in least fixed point is not according to, say, usual numeric ordering. It's the (partial) ordering of definedness. So, for a typical numeric type, this ordering looks like: 1) _|_, the undefined element, is less than every other value 2) All other values are not comparable to each other. So, iterating a function from a defined starting value finds a fixed point (maybe), but that fixed point is not less or greater than any other number, as far as the ordering of definedness is concerned. Luke's function, however: fixAbove f x = fix f `lub` x finds the least defined upper bound of 'fix f' and 'x' via some threading and IO magic. With it you can do stuff like: fixAbove id 5 = fix id `lub` 5 = _|_ `lub` 5 = 5 (Assuming fix id returns _|_ in a way that the library can detect.) And indeed, id 5 = 5, 5 = 5, and 5 is the least defined such value. More interesting cases occur when you can have partially defined values. Consider lazy naturals: data Nat = Z | S Nat _|_ Z forall n :: Nat. _|_ S n forall m, n :: Nat. m n - S m S n Which means we now have more structure, like '_|_ S _|_ S (S _|_) ...'. Of course, all totally defined values are still incomparable to one another. 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 Now: fix f = _|_ 2:_|_ twos f twos = f (2:twos) = 2 : 2 : twos = twos So twos is a fixed point of f, and greater than 2:_|_, but: fixAbove f (2:_|_) = fix f `lub` (2:_|_) = _|_ `lub` 2:_|_ = 2:_|_ so we have failed to find the least fixed point above our given value. I think fixAbove is only successful when one of the following conditions is met: 1) fix f = _|_ and x is a fixed point of f (maybe fix f x works, too) 2) x fix f But neither of those cases are particularly novel, unfortunately. Anyhow, hope that helps a bit. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
On Fri, Mar 20, 2009 at 1:01 AM, Dan Doel dan.d...@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). -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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 dan.d...@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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] least fixed points above something
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? Jens ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
I've used a similar function myself, but why write it in such a complicated way? How about lfp :: Eq a = (a - a) - a - a lfp f x | f x == x = x | otherwise = lfp f (f x) Edsko On 19 Mar 2009, at 09:49, Jens Blanck wrote: 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? Jens ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
I've used a similar function myself, but why write it in such a complicated way? How about lfp :: Eq a = (a - a) - a - a lfp f x | f x == x = x | otherwise = lfp f (f x) I've used a similar function too, but your version computes f x twice per iteration, I wrote mine as: fix :: Eq a = (a - a) - a - a fix f x = if x == x2 then x else fix f x2 where x2 = f x I find this fix much more useful than the standard fix. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
I always feel that the compiler should do such optimizations for me :) On 19 Mar 2009, at 16:21, Neil Mitchell wrote: I've used a similar function myself, but why write it in such a complicated way? How about lfp :: Eq a = (a - a) - a - a lfp f x | f x == x = x | otherwise = lfp f (f x) I've used a similar function too, but your version computes f x twice per iteration, I wrote mine as: fix :: Eq a = (a - a) - a - a fix f x = if x == x2 then x else fix f x2 where x2 = f x I find this fix much more useful than the standard fix. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
CSE is tricky and a potential space leak in general. I'd love it if the compiler could pick the best option, but I'm afraid its unlikely to know. On Thu, Mar 19, 2009 at 4:25 PM, Edsko de Vries devri...@cs.tcd.ie wrote: I always feel that the compiler should do such optimizations for me :) On 19 Mar 2009, at 16:21, Neil Mitchell wrote: I've used a similar function myself, but why write it in such a complicated way? How about lfp :: Eq a = (a - a) - a - a lfp f x | f x == x = x | otherwise = lfp f (f x) I've used a similar function too, but your version computes f x twice per iteration, I wrote mine as: fix :: Eq a = (a - a) - a - a fix f x = if x == x2 then x else fix f x2 where x2 = f x I find this fix much more useful than the standard fix. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
Can you give an example of when CSE would not be the way to go? Thanks, Martijn. Neil Mitchell wrote: CSE is tricky and a potential space leak in general. I'd love it if the compiler could pick the best option, but I'm afraid its unlikely to know. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
A JIT compiler can easily know. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Mar 19, 2009, at 10:29 AM, Neil Mitchell wrote: CSE is tricky and a potential space leak in general. I'd love it if the compiler could pick the best option, but I'm afraid its unlikely to know. On Thu, Mar 19, 2009 at 4:25 PM, Edsko de Vries devri...@cs.tcd.ie wrote: I always feel that the compiler should do such optimizations for me :) On 19 Mar 2009, at 16:21, Neil Mitchell wrote: I've used a similar function myself, but why write it in such a complicated way? How about lfp :: Eq a = (a - a) - a - a lfp f x | f x == x = x | otherwise = lfp f (f x) I've used a similar function too, but your version computes f x twice per iteration, I wrote mine as: fix :: Eq a = (a - a) - a - a fix f x = if x == x2 then x else fix f x2 where x2 = f x I find this fix much more useful than the standard fix. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
Can you give an example of when CSE would not be the way to go? if length (replicate 'a' 1) == 1 then [] else head (replicate 'a' 1) This program will use O(1) memory. If we perform CSE: if length x == 1 then [] else head x where x = replicate 'a' 1 Now we use 1 cells of memory. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
Neil Mitchell wrote: if length (replicate 'a' 1) == 1 then [] else head (replicate 'a' 1) This program will use O(1) memory. Doesn't length force evaluation of the 1 cells? Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
On 19 Mar 2009, at 16:37, Martijn van Steenbergen wrote: Neil Mitchell wrote: if length (replicate 'a' 1) == 1 then [] else head (replicate 'a' 1) This program will use O(1) memory. Doesn't length force evaluation of the 1 cells? Yes, but without CSE every cell can immediately be garbage collected; hence, CSE can lead to space leaks - a fair point. Edsko ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
Anyway, these functions do not get the least fixed point ot r, but a fixed point of f starting from the seed x. it is'n? http://en.wikipedia.org/wiki/Fixed_point_(mathematics) 2009/3/19 Neil Mitchell ndmitch...@gmail.com I've used a similar function myself, but why write it in such a complicated way? How about lfp :: Eq a = (a - a) - a - a lfp f x | f x == x = x | otherwise = lfp f (f x) I've used a similar function too, but your version computes f x twice per iteration, I wrote mine as: 't fix :: Eq a = (a - a) - a - a fix f x = if x == x2 then x else fix f x2 where x2 = f x I find this fix much more useful than the standard fix. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] least fixed points above something
2009/3/19 Jens Blanck jens.bla...@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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
