[m-rev.] diff: avoid runtime aborts from the decl debug oracle

[Mark Brown]

On 11-Oct-2002, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> On 11-Oct-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > 	1) The user is asked a missing answer question for p, for which the
> > 	solutions are A, B and C.  The user asserts that this set is complete
> > 	(but it may contain wrong answers).
> > 
> > 	2) The user goes on to diagnose a bug, then saves the oracle
> > 	state, fixes the bug, and fires up another debugging session to
> > 	diagnose some other symptom.
> > 
> > 	3) The user is again asked about that call to p, but this time the
> > 	solutions are A, B and D.  The user asserts that this set is also
> > 	complete.
> > 
> > 	4) At this point, the oracle deduces that {A, B} must be a complete
> > 	set of solutions for that call to p, since it is the intersection
> > 	of the two previous complete sets.
> 
> I figure that getting A, B and D at step 3 would a pretty rare event.
> Most predicates don't have higher order outputs,

Granted.

> and the ones that do
> tend not to be modified in ways that return syntactically different
> but semantically equivalent higher order terms.

This can happen if you change the way a function name is spelt, which is
reasonably likely to happen.

> Another solution would be to modify the process of updating the solution sets.
> If the intersection reduces the cardinality of the set, we can check whether
> the deleted elements include higher order components. If not, do everything
> as before. If yes, then compute the differences between the sets being
> intersected, which in this case yields {C} and {D}, and ask the user
> whether they contain the same functions semantically. If yes, add their union
> to the intersection. In this case, that means storing {A, B, C, D} as the
> complete set of solutions.

That seems like a reasonable approach.  Also, the question about the
semantic equivalence of two higher order terms is an excellent one in
the case that a function's name has changed: it would be an easy question
to answer and it would make it possible for the oracle to transfer all of
its knowledge about the old function to the new function.

> Of course, we can even avoid asking the user, and always add the union of the
> residues to the intersection. This may lead to more questions than if the set
> was precise, but it may lead to fewer questions than a scheme that doesn't
> keep the answer sets at all.

It would also be okay to just keep the residues from one of the sets.
Any set that is known to be a superset of the solutions would be
acceptable.

We should leave further discussion of this until after the freeze.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------