[m-dev.] more correctness problems

[Ralph Becket]

Peter Schachte, Friday, 31 March 2006:
> 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.

It was in response to your earlier e-mail about problems with inst any.
Here is what I wrote:

> An idea just occurred to me:
> 
> For a procedure whose headvars are all ground or free on entry and exit:
> - operational failure is definite semantic failure
> - operational success is definite semantic success
> 
> For a procedure whose headvars may have inst any on entry or exit:
> - operational failure is definite semantic failure
> - operational success is *possible* semantic success
> 
> It should be an error for a procedure of the first kind to have local
> inst any vars without enclosing that code in a
> promise_solver_consistent scope.
> 
> For example:
> 
> main(!IO) :-
>         ( if
>                 promise_solver_consistent (
>                         set_up_solver_problem,
>                         search_for_solution,
>                         final_check_to_ensure_consistency
>                 )
>           then
>                 io.print("the answer is...", !IO),
>                 ...
>           else
>                 io.print("no solution", !IO)
>         ).
> 
> I think this is a reasonable solution to the existentially-quantified-
> solver-vars problem.

Just as promise_pure places a burden of proof on the programmer, so does
promise_solver_consistent.  Solvers should provide predicates to check
for complete consistency.  These predicates need not be cheap, since
they are only called by the programmer as a final sanity check at the
end of a promise_solver_consistent scope.

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

main/2 (or whatever predicate that posts and solves the constraints)
would be required by the compiler to have that code in a
promise_solver_consistent scope.  If the programmer uses the scope, but
doesn't check for complete consistency, then that's the programmer's
error.

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

You don't untrail on a commit: a commit doesn't mean execution won't
backtrack past this point.

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

In practice this hasn't been an issue.

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

How would the solver know when to take calls to the consistency check
predicate seriously and when not to?

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

Variable creation invariably involves adding a trail entry.

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

I don't think I properly follow your point.  Can you give an example?

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