on termination

[Peter Gammie]

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