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

[Ralph Becket]

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

	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.

	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.  This property is inherited by compound
goals.  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.

-----------------------------------------------------------------------

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.

-----------------------------------------------------------------------

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

-----------------------------------------------------------------------

Feedback welcome.

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