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

[Mark Brown]

On 01-Jun-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> My take regarding recent discussion on the subject topic.
> 
> -----------------------------------------------------------------------
> 
> PROBLEM: goals that may succeed, but leave the hidden solver state
> inconsistent (i.e., for which success does not correspond to truth).

In the terminology of the CP handbook, the program is not "solver complete"
for these goals.

> 
> 	Some goals post constraints (i.e., change the hidden solver
> 	state).
> 
> 	A constraint posting goal may succeed, but render the solver
> 	state inconsistent: for such goals,
> 	- failure means definite inconsistency.
> 	- success means possible inconsistency.
> 	These goals will be common.
> 	Many, if not most, constraint posting goals will be of this
> 	kind.
> 
> 	Some goals may render the solver state consistent: for such
> 	goals,
> 	- failure means definite inconsistency.
> 	- success means definite consistency.
> 	These goals will be rare.

_Atomic_ goals with this property would be rare, but compound goals with
this property should be more common (e.g., in the FD solver any conjunction
that labels all the variables will have it).

> 
> 	Constraint posting goals must not appear in negated contexts
> 	(regardless of whether they guarantee to leave the solver state
> 	consistent or not).
> 
> 	Goals that merely query the solver state must be impure (because
> 	they have an operational semantics, but not a denotational
> 	semantics).
> 
> 	Impure goals can safely appear in negations because their
> 	impurity places the burden of correct use on the programmer, not
> 	the compiler.
> 
> RECOMMENDATION: we (somehow, perhaps by annotation on mode declarations)
> identify constraint posting predicates that may succeed, but leave the
> solver state inconsistent.

If we were to adopt such a scheme, then I'd suggest putting the explicit
annotation on the goals where success means consistent.  That is, by
default we should assume that a program is not solver complete for calls
to predicates with an `any' inst which do not have this annotation.

However, I don't think that attaching this information to modes is
fine-grained enough.  Consider the goal `X = Y + Z' for FD variables X, Y
and Z.  A program will be solver complete for this goal if at least two of
the variables are ground at the time of the call (assuming a reasonable
implementation of '+'), but may not be if only one of them is ground.

Peter Schachte pointed out to me that we may be able to express the condition
we want by using something like functional dependencies.  E.g.: the signature
for '+' could assert the dependencies

	(X, Y -> Z), (X, Z -> Y), (Y, Z -> X)

which, if we have information about which variables are ground at the start
of the call, will tell us whether the program is solver somplete for that
goal.

> This property is inherited by compound
> goals.

How?  The "obvious" way to do it (propagating incompleteness upwards) would
not be very accurate, since a conjunction containing incomplete conjuncts
may itself be complete if the last conjunct labels all the variables.

This is why I asked earlier for a theory about solver completeness.  The
key questions I want to know about are:

	1)  Given information about the completeness of atomic goals,
	how can we infer completeness information about compound goals
	containing them?

	2)  What form does this information take?

	3)  How much of this theory is valid for solvers in general, and
	how much of it is solver specific?  Is there any useful theory at
	all for solvers in general?

Here's some answers (not in the same order) for the case of the FD solver:

	2)  The information takes the form of the functional dependencies
	mentioned above.

	1)  Something similar to groundness analysis.  We calculate the
	closure of the induced dependencies and ensure that variables are
	ground before they are existentially quantified away.

	3)  This theory is solver specific, in that it only works if all
	propagators are "checking" (which, however, is not an unreasonable
	requirement on propagator implementors).

> Goals with this property cannot appear in negated contexts.
> 
> ------------------------------------------------------------------------
> 
> PROBLEM: a goal in a negated context may fail because it detects 
> inconsistency in the solver state due to a goal posted outside the
> negated context.
> 
> RECOMMENDATION: since such a goal must be impure (it is querying the
> hidden solver state and therefore has no denotational reading) this
> behaviour must be described in the documentation for the predicate
> involved.  Caveat emptor.

I agree that this isn't a problem for the language.

> 
> -----------------------------------------------------------------------
> 
> PROBLEM: pure IO should not be allowed in a context where a solver state
> may be inconsistent (because if the inconsistency had been detected
> earlier, we may not have reached this point in the program).
> 
> RECOMMENDATION: a new annotation or scope should be introduced allowing
> IO (or, indeed, any pure, non-backtrackable operation) in a context
> where there are visible inst `any' variables.  This annotation or scope
> should be a promise of some kind.

I don't think this is a separate problem.  Once we have ensured that the
program is solver complete for the goal main/2, then uniqueness and
determinism analysis will take care of any potential problems with IO.

> 
> -----------------------------------------------------------------------
> 
> PROBLEM: existentially quantified solver variables may be constructed,
> constrained (leaving the solver state inconsistent), then "forgotten"
> outside the quantification.
> 
> RECOMMENDATION: solvers should remember all posted constraints so they
> can be checked for consistency at some point (e.g., where the programmer
> wants to do IO).

In other words, we could detect floundering at run time and take appropriate
action.

Cheers,
Mark.

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