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 <[email protected]> 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 <[email protected]> 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 <[email protected]>: >> > 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 <[email protected]> >> > 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 <[email protected]> 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 >> > [email protected] >> > http://www.haskell.org/mailman/listinfo/haskell-cafe >> > >> > > > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
