on termination

[Andrew J Bromage]

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