Subject: Re: really undecidable instances?
Date: Tuesday 18th October 2005 09:58:15 UTC (over 12 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/ -------