On Saturday 24 January 2009 10:26:48 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.
You may be able to guarantee termination, but that doesn't mean it is expressible as a fold. Folds are equivalent in power to primitive recursion over the given data type, but not all terminating computations are expressible with primitive recursion (for instance, you can guarantee the termination of the Ackermann function given enough memory and time, but it is famous for not being primitive recursive (at least, in the absence of higher-order functions)). So, it's entirely possible that your function is provably terminating, but not primitive recursive on lists (although you might be able to represent the proof in a sufficiently fancy language, and 'fold' over it instead). The way you've heretofore described it makes one lean in this direction, since in all cases you've called f with the result of an arbitrary function on the only noticeable candidate for an argument that shrinks between calls. But, it's also possible if you filled in something real for "g", a fold version would be more forthcoming. -- Dan