[m-dev.] more correctness problems

[Peter Schachte]

On Thu, Mar 30, 2006 at 04:55:55PM +1000, Ralph Becket wrote:
> schachte at csse.unimelb.edu.au, Thursday, 30 March 2006:
> > 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.

I haven't seen any description of promise_consistent, but it's hard to
see how anything called "promise_consistent" can help to make
inconsistent goals fail.

Peter argues that "success" of a constraint goal carries no
information (it just means the solver isn't sure it's false), and the
result of a succeeding computation is the constraint store.  If that
constraint store is inconsistent, it's up to the user to see that.  So
it's OK for

	X > 4, X < 4

to succeed.  But Mercury doesn't print the constraint store, and
anyway that wouldn't be much help to the guy on the shop floor trying
to use the output of a Mercury program.  Or to the traffic signals
that all go green at once because they don't realize that doing so is
not actually a solution to the input constraints.

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

Why would anything be trailed?  The code between the introduction and
elimination of Y is all "semidet."  And why should all solvers be
required to keep track of all variables?  If I'm implementing a
solver, I *want* unneeded variables to be garbage collected, but only
after I've checked that there is a solution for them.  Currently,
there's no way to know when a variable is eliminated, so no way to
know when to check.

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

It wouldn't make any difference to any solver that didn't declare such
a method.  And it would improve performance for a solver that wants to
be lazy when it can get away with it, but still be complete.

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

You can remove a dead variable if no choicepoints have been pushed
since the variable was created (of course, you sometimes have to
propagate constraints on it to other variables it's related to).  When
you're doing constrain-and-generate, that should be fairly common.
Whether or not this is a win will depend on the details of the solver
implementation, but right now there's no way to do it.

-- 
Peter Schachte              George W. Bush is like pecan pie - a sweetened
schachte at cs.mu.OZ.AU        way to sell a marginally-popular Texas nut.
www.cs.mu.oz.au/~schachte/      -- Bill Lockyer 
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
--------------------------------------------------------------------------