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.s...@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.and...@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.and...@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.d...@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@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