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. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
