[Haskell-cafe] Fold that quits early?

[Andrew Wagner]

There's at least one thing; I won't call it a flaw in your logic, but it's
not true of my usage. Your definition always produces a non-null list. The
particular g in my mind will eventually produce a null list, somewhere down
the line. I think if that's true, we can guarantee termination.

On Sat, Jan 24, 2009 at 10:16 PM, Ryan Ingram <ryani.spam at gmail.com> wrote:

> 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 [1]?
>
> f 0 [1]
>        = foldr f [0,1] [0,1]
>        = let t1 = foldr f [0,1] [1] in f 0 $ t1
>        = let t1 = foldr f [0,1] [1] in foldr f (0 : t1) (0 : t1)
>        = let t1 = foldr f [0,1] [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?
>
>  -- ryan
>
> 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>
> > wrote:
> >>
> >> 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
> >>> of
> >>> foldr, and it works fine on infinite lists, quitting as soon as it
> finds
> >>> a
> >>> True. As long as you don't use the result of the recursive call (which
> is
> >>> the
> >>> second argument in the function you pass to foldr), it will exit early.
> >>>
> >>> The problem is that your function doesn't look structurally recursive,
> >>> and
> >>> that's what folds (the usual ones, anyway) are: a combinator for
> >>> structural
> >>> recursion. The problem is in your inductive case, where you don't just
> >>> recurse
> >>> on "ys", you instead recurse on "ys' ++ ys", where ys' is the result of
> >>> an
> >>> arbitrary function. folds simply don't work that way, and only give you
> >>> access
> >>> 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,
> >>> for
> >>> 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
> >>> non-
> >>> structurally recursive functions.
> >>>
> >>> -- Dan
> >>
> >
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090124/015748d6/attachment.htm