the MPTC Dilemma (please solve)
ross at soi.city.ac.uk
Tue Feb 21 19:16:43 EST 2006
On Tue, Feb 21, 2006 at 03:50:52PM +0800, Martin Sulzmann wrote:
> A depth limit is not enough. For confluence we need that *all*
> derivations for a particular goal terminate. Once we have
> confluence we get completeness of the inference checks.
So without a static test for termination (though just for this goal),
we're still in the no-man's land between proof and counterexample.
Reduction might be confluent, but we have no proof.
More information about the Haskell-prime