Fri, 9 May 2003 12:38:09 +1000 (EST)
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:
> 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
that seems related to what we're discussing.