Re: [Haskell-cafe] Fold that quits early?

24 Jan 2009

      My point is that without further knowledge of this function, it's not
possible to simplify into a fold.  For f to be a fold, the result
would have to terminate for *every* total function g; given that there
are some total functions for which f does not terminate, f cannot be a
fold.

It's possible that the particular combination of f and g that you have
in mind *does* simplify to a fold, but the current function cannot,
unless I've made a mistake.

  -- ryan

On Sat, Jan 24, 2009 at 7:26 PM, Andrew Wagner  wrote:
...
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  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 :
...
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 
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  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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe