[m-dev.] more correctness problems

[Ralph Becket]

schachte at csse.unimelb.edu.au, Thursday, 30 March 2006:
> 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.

I believe my promise_consistent scope addresses this problem.

> 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.

Both the solvers and the trail will remember Y, so Y will not be garbage
collected.

> 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.

I think this would shaft search performance in virtually all solver
applications and make solver types highly unattractive.  This is why I
suggested promise_consistent instead.

> This would
> also allow solvers that do keep a central store of constraints to
> remove dead variables, knowing they'll never be seen again.

That's not quite true, as these things will still exist on the trail
(untrailing will cause solvers to "forget" variables).

> 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.

There are many sound cases where you end up with a solver variable in
the condition of an if-then-else.  For example, list.length(Xs) (Xs is a
list of solver vars) or any_map.search(AnyMap, Key, X) (AnyMap contains
solver vars, but Keys are ground).  Currently the compiler *does* require
such situations to be treated as impure.  It has been suggested (and I
think it's a good idea) that such things should instead only be allowed
in a scope that states explicitly the nature of the problem (e.g.,
something like promise_solver_type_in_negation_is_sound, but hopefully
less wordy).

-- Ralph
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------