# the MPTC Dilemma (please solve)

Martin Sulzmann sulzmann at comp.nus.edu.sg
Tue Feb 21 02:50:52 EST 2006

```Ross Paterson writes:
> On Sat, Feb 18, 2006 at 12:26:36AM +0000, Ross Paterson wrote:
> > Martin Sulzmann <sulzmann at comp.nus.edu.sg> 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
```