[Haskell-cafe] Fold that quits early?
ryani.spam at gmail.com
Sat Jan 24 22:16:20 EST 2009
foldr f z xs =
x0 `f` (x1 `f` (x2 `f` ... (xN `f` z) ...))
In particular, note that if f is a total function, xs is finite and
totally defined, and z is totally defined, then the result of this
fold is totally defined.
Now consider your "f" (rewritten slightly)
f x xs
| null xs = 
| p x = 
| otherwise = foldr f (x:xs) (g x xs)
with these definitions:
c _ = False
g = (:)
c and g are definitely total functions, so what happens when we
evaluate f 0 ?
f 0 
= foldr f [0,1] [0,1]
= let t1 = foldr f [0,1]  in f 0 $ t1
= let t1 = foldr f [0,1]  in foldr f (0 : t1) (0 : t1)
= let t1 = foldr f [0,1] 
t2 = foldr f (0:t1) t1
in f 0 t2
etc.; this is clearly non-terminating.
Therefore there is no way to make f into a fold.
Any errors in my logic?
2009/1/24 Andrew Wagner <wagner.andrew at gmail.com>:
> Ahem. That's what happens when you don't type-check your brainstorming
> before barfing it out, kids. Sorry about that. Let's try this again:
> f _  = 
> f y x | c y = 
> | otherwise = foldr f (y:x) (g y x)
> I've got a fold on the inside now, but I'm pretty sure the whole thing is
> just a fold. Not quite there yet, though...
> On Sat, Jan 24, 2009 at 1:42 PM, Andrew Wagner <wagner.andrew at gmail.com>
>> Actually, I think I can rewrite it this way:
>> f xs  = False
>> f xs (y:ys) | any c ys' = True
>> | otherwise = f (f (y:xs) ys') ys
>> where ys' = g y ys
>> This should help, I think.
>> On Sat, Jan 24, 2009 at 12:11 PM, Dan Doel <dan.doel at gmail.com> wrote:
>>> On Saturday 24 January 2009 11:39:13 am Andrew Wagner wrote:
>>> > This is almost a fold, but seemingly not quite? I know I've seem some
>>> > talk
>>> > of folds that potentially "quit" early. but not sure where I saw that,
>>> > or
>>> > if it fits.
>>> > f xs  = False
>>> > f xs (y:ys) | any c ys' = True
>>> > | otherwise = f (nub (y:xs)) (ys' ++ ys)
>>> > where ys' = g y xs
>>> Quitting early isn't the problem. For instance, any is defined in terms
>>> foldr, and it works fine on infinite lists, quitting as soon as it finds
>>> True. As long as you don't use the result of the recursive call (which is
>>> second argument in the function you pass to foldr), it will exit early.
>>> The problem is that your function doesn't look structurally recursive,
>>> that's what folds (the usual ones, anyway) are: a combinator for
>>> recursion. The problem is in your inductive case, where you don't just
>>> on "ys", you instead recurse on "ys' ++ ys", where ys' is the result of
>>> arbitrary function. folds simply don't work that way, and only give you
>>> to the recursive call over the tail, but in a language like Agda, the
>>> termination checker would flag even this definition, and you'd have to,
>>> instance, write a proof that this actually does terminate, and do
>>> induction on
>>> the structure of the proof, or use some other such technique for writing
>>> structurally recursive functions.
>>> -- Dan
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe