[m-dev.] Solvers, negation, existential quantification, and so forth

[Peter Schachte]

This thread has been rather long, and included wide ranging
discussion.  I think I understand how the pieces fit together, and in
the spirit of active listening, it seems like a good idea to restate
them all together, to see if I've got them right.

The goal of this whole exercise is to ensure that Mercury programs
don't produce output based on a constraint store not known to be
satisfiable, at least not without the programmer being aware of it or
falsely promising things.  At the moment there is no such guarantee;
it's left up to an informal arrangement between the solver writer and
the solver user.  The problem that arises is that we need to ensure
that there does exist a binding for every existentially quantified
solver variable in the program, but we cannot count on all solvers
doing this automatically, and we certainly don't want to burden them
with the obligation to label every variable when it is existentially
quantified.

It does seem reasonable to expect of solvers to completely decide the
validity of ground primitive constraints, but they also need to do
this for constraints that become ground after they have been executed,
and we don't want to require the solver to notice the moment enough
other constraints are imposed to make the constraint ground.  We want
to check this at the end of the computation, having the solver check
the existence of bindings for any existentially quantified variables
as necessary.  I think we need to ask solver writers to define a
niladic semidet method that performs this check.  It should succeed if
the store is satisfiable, fail if not, and throw an exception if it
cannot decide.  Mercury should require pure code to invoke this method
for any solver types that appear in the body but not the head of a
clause.

As Mark has argued, in a reasonable number of cases, the compiler
should be able to work out that when all the head variables of a
clause become ground, so will the existentially quantified variables
in that clause.  This means that the solver does not need to
specifically check whether there are satisfying bindings for those
variables, because the goal cannot succeed without (eventually)
generating a ground binding, and the solver is expected to fail in its
final test (or sooner) if a ground variable does not satisfy some
constraints.  In other cases, the programmer can determine either that
such a groundness dependency exists, or that there is always a
satisfying substitution for the quantified variables, but Mercury is
unable to prove it.  And in still other cases, the property will not
exist, and the solver must remember some existentially quantified
variables, so it can verify that satisfying bindings exist during the
final completeness check.

To implement the second of these three possibilities, Mercury should
support a special existential quantifier that promises either that
grounding all the other variables in the clause will ground the
quantified variables, or that a satisfying substitution always exists.
For the third possibility, Mark proposes a solver method
delayed_labelling/1 that instructs the solver to remember these
variables so that they can be checked for satisfiability in the final
check.  I would argue that it would be better syntactically to make
this another special quantifier, similar to the one above.  But let's
argue syntax later.

The first possibility, that groundness of head variables ensures
groundness of existentially quantified variables, requires a new
groundness dependency analysis in the Mercury compiler.  This would
probably be a fairly significant project on its own.  However, it may
be possible to piggy-back on the current mode analyser, if modes for
solver predicates used ground and free, instead of any.  Eg, you might
write

	:- mode in + in = out.
	:- mode in + out = in.
	:- mode out + in = in.

and that would give the dependency information necessary for the
analysis, and Mercury can check them with no problem.  It would just
mean changing the interpretation of modes for solver types altogether
so, eg, the first mode above would mean *whenever* the two arguments
of + are ground, so is the result.  Just a teeny little change. :-)
The declaration would also have to indicate which arguments could be
any insts at call time, too, perhaps using any(in) and any(out)
instead of in and out in my example.

So, Mark, Ralph, and others, is this a fair summary of the evolving
plan?  What have I missed?

One problems we shouldn't forget:  negation.  Somehow we still need to
either statically or dynamically ensure that constraints aren't added
inside a negation.  Also, we need to be sure that this scheme makes it
impossible to do pure IO until the final consistency check is
performed for all solvers.  In fact, this might have practical
problems for programs that want to do incremental constraint solving
interleaved with IO, such as interactive constraint-based graphical
layout.

One suggestion I'll repeat is that in addition to a method to finally
check for consistency of a solver, it would sometimes be useful to
have one to initialise a solver.  This would act as an "open bracket"
while the final check method would be a "close bracket."  When the
initialiser is called, it would save away the state of that solver and
initialise a fresh solver (since no old variable can be related in any
way to a new one).  The close bracket would check satisfiability and
then restore the state.  This would allow the solver to avoid ever
rechecking consistency of constraints, and would also allow it to
garbage collect the entire solver state after the final check.  So a
solver could be used for small unrelated tasks without polluting the
solver state with garbage.  The initialisation method for a solver
need not do anything, as long as the final check doesn't garbage
collect the solver state, so this would not burden solver writers.
And it's trivial to detect where the initialisation is necessary when
you're already detecting where the final check is needed, so it's not
much burden on Mercury.

My second suggestion is that Mercury should have an
--infer-completeness switch (or pick a better name) that tells Mercury
to automatically insert the initialisation and final check calls where
they are needed, and to automatically insert the delayed_labelling
goals where needed.  Neither of these would be difficult to do (as
long as we're doing the analysis anyway), so it shouldn't be too much
effort.  And it would make Mercury with constraints *much* easier for
newbies and for people who want to just write their constraint code
before they start worrying too much about search performance.

-- 
Peter Schachte              The use of COBOL cripples the mind; its teaching
schachte at cs.mu.OZ.AU        should, therefore, be regarded as a criminal
www.cs.mu.oz.au/~schachte/  offence.
Phone: +61 3 8344 1338          -- E. W. Dijkstra 
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------