Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Johannes Waldmann <waldmann <at> imn.htwk-leipzig.de>
Subject: Re: really undecidable instances?
Newsgroups: gmane.comp.lang.haskell.general
Date: Tuesday 18th October 2005 09:58:15 UTC (over 11 years ago)
Simon Peyton-Jones wrote:
> It's all very delicate.  I believe, though I am not certain, that in the
> absence of functional dependencies, removing at least one type
> constructor might be an example of a rule that is sufficient to ensure
> termination.  There are lots of such rules. Alas none known to me
> capture all cases.

Of course they couldn't - because of undecidability of termination
(of term rewriting, or Prolog-like programs).
But then, there are a lot of (nontrivially) decidable subcases,
and consequently there are quite a few automated methods
for termination proofs,
see http://www.lri.fr/%7Emarche/termination-competition/2005/
Would it be interesting to "beef up" the termination analysis in ghc a 
bit, using some of those methods?

But then, the current solution is just use "-fundecidable.."
and the see if the type checker (apparently) loops.
This might still be more efficient than invoking a larger machinery
that would prove (non)termination because after the proof
you'd still have to invest the time into doing the rewrite sequence.

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/
-------
 
CD: 2ms