G'day all. On Thu, May 08, 2003 at 06:07:44PM +1000, Peter Gammie wrote:
Now, a question of my own: is it possible to uniformly define a class of functions that have a non-trivial decidable halting predicate? The notion of "uniform" is up for argument, but i want to rule out examples like Andrew's that involve combining classes in trivial ways.
The Mercury group did some work on this as a static analysis. Have a look for all papers with "termination analysis" in the title: http://www.cs.mu.oz.au/research/mercury/information/papers.html Unfortunately this work is probably no use for Haskell, as they all rely on data structures not being infinite or cyclic (which they are in any logic language which features an occurs check or statically computable equivalent). Cheers, Andrew Bromage