[m-dev.] more correctness problems

[schachte at csse.unimelb.edu.au]

Hi all,

I've been considering the problem of solvers goals that
(operationally) succeed even when the constraint store is
unsatisfiable.  I've argued before that due to this, problems arise
from existential quantification.  Peter argued that the only problem
is negation (I hope I'm being fair here).  On reflection, I think
both are problems.  Consider this code:

	p(X) :- q(X,Y).

	q(X,Y) :- X>4, Y>4, Y<4.

Suppose operationally, the solver for X promises that (>)/2 fails when
the domain for either of its arguments is empty, while the solver for
Y does not (assume they're different types).  Now the code for p/1 may
actually be wrong, because when Y goes out of scope (is existentially
quantified away), nothing forces the solver to actually test that
there does exist a satisfying Y.  Certainly

	exists Y . Y>4, Y<4

is false, but Mercury implements existential quantification by just
dropping the variable.  If the solver doesn't keep a central store, Y
will just get garbage collected, so the inconsistency will never be
discovered.  Even if it does have a central store, when would it ever
get around to checking that Y has a solution?  Note, though, that if
the arguments in the call to q/2 were exchanged, there would be no
problem there, because the unsolvable variable would still be alive.
So the problem is specific to the variables quantified away.

This suggests solvers should be able to define a semidet method that
gets invoked when a solver variable goes out of scope (is quantified
away), indicating that it's now or never to check that the variable
has solutions.  The Mercury compiler would generate calls to this
method automatically where the variable goes out of scope.  This would
also allow solvers that do keep a central store of constraints to
remove dead variables, knowing they'll never be seen again.  Probably
the method should take a list of variables, so the solver gets all the
variables to be killed off at the same time, allowing it to plan its
actions.

Note that this problem is different from the problem of negations
involving any insts.  There the concern is that a negated goal should
not further constrain a non-ground variable.  I don't imagine there
are many goals involving any inst variables that don't constrain those
variables, so I don't expect there would be many cases where a negated
context mentioning an any inst variable is sound.  They really should
be impure.

-- 
Peter Schachte              The government of the United States does not, in
schachte at cs.mu.OZ.AU        its policies, express the decency of its people.
www.cs.mu.oz.au/~schachte/      -- Jerry Fresia 
Phone: +61 3 8344 1338      
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------