Re: the MPTC Dilemma (please solve)

Ross Paterson writes:

On Sat, Feb 18, 2006 at 12:26:36AM +0000, Ross Paterson wrote:

...

Martin Sulzmann writes:

...

Result2: Assuming we can guarantee termination, then type inference is complete if we can satisfy - the Bound Variable Condition, - the Weak Coverage Condition, - the Consistency Condition, and - and FDs are full. Effectively, the above says that type inference is sound, complete but semi-decidable. That is, we're complete if each each inference goal terminates.

I think that this is a little stronger than Theorem 2 from the paper, which assumes that the CHR derived from the instances is terminating. If termination is obtained via a depth limit (as in hugs -98 and ghc -fallow-undecidable-instances), it is conceivable that for a particular goal, one strategy might run into the limit and fail, while a different strategy might reach success in fewer steps.

Yes, the above is stronger than Theorem 2.

Rereading, I see you mentioned dynamic termination checks, but not depth limits. Can you say a bit more about termination? It seems to be crucial for your proofs of confluence.

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. I think you're asking: If one derivation for a particular goal terminates will all other derivations for that goal terminate as well? (BTW, such a result can be proven for range restriction). It might hold (assuming the usual restrictions, instances terminate, weak coverage holds etc) by I'm not sure (means, I couldn't come up with a counter-example but a formal proof is still missing). Martin