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