On Fri, 9 May 2003, Andrew J Bromage wrote:
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).
To flog the horse a bit further: this isn't what i'm looking for, as there are predicates that do terminate and fail to be identified as such. (Putting it another way, the termination check is incomplete - as all such checks must be for a Turing-complete language.) I recall Harald reckoning their check is adequate for 80% of the predicates in the compiler, so it is impressive even so. A friend pointed me to David Turner's page on strong functional programming: http://www.cs.ukc.ac.uk/people/staff/dat/esfp.html that seems related to what we're discussing. cheers peter