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

[Peter Schachte]

> PROBLEM: goals that may succeed, but leave the hidden solver state
> inconsistent (i.e., for which success does not correspond to truth).

This isn't a problem in itself, only if main finishes with a solver in
an inconsistent state.  Forbidding main/2 from being inconsistent is
enough (for this problem).

> 	A constraint posting goal may succeed, but render the solver
> 	state inconsistent
> 
> 	Some goals may render the solver state consistent

And some goals may post constraints that cannot affect the consistency
of the solver (eg, a complete solver, or a solver that is always
complete for certain primitive constraints).

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

This property needs to be parametric in the solver id involved.  This
is because a primitive may render a *particular* solver complete, but
it can't possibly promise to render *all* solvers complete.

So how about, eg,

	:- mode any < any is semidet + incomplete(cint).

	:- mode cint.ensure_complete is semidet + completes(cint).

But this still has the problem with polymorphism.  Eg, you might want
to write a predicate all_equal(list(T), T) that constrains all
elements of the first argument to equal the second.  And you might
want this to work on lists of any inst terms.  I'm not sure how you
can handle the incompleteness of this pred depending on the
incompleteness of unification for the parametric type.  Suggestions
welcome.


> 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

Any semidet tell constraint queries the hidden solver state, and tell
constraints aren't impure.  Likewise a labelling pred.  But they can't
be used in negations.

So every goal that may impose constraints, whether complete or
incomplete, must be marked.  Zoltan was suggesting a similar syntax to
impurity, eg:

	:- constraint pred cint < cint.

or maybe this:

	:- clp pred cint < cint.

It's a bit cryptic, but so are 'det' and 'multi', and it's easier on
the eye.

This would be required on any predicate that calls a clp pred.  The
one exception would be a complete predicate that does not have any
any-inst parameters.

Wait.  On reflection, it might be better to attach clp-ness to procs,
rather than preds.  So it would instead be, eg:

	:- clp mode any < any is semidet + incomplete(cint).


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

It shouldn't be necessary to promise anything.  If all solvers are
complete (and det or cc_multi), IO should be OK.  It should also be OK
to do IO in an impure context.

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

I guess.  This is actually a problem for my delay solver:  it doesn't
centrally remember all the delayed constraints, so it would need to
be rewritten.

It seems pretty undesirable not to provide any mechanism for garbage
collecting constraints:  after all, they increase monotonically
throughout the computation.  So you'll never be able to write a
long-running Mercury program that uses constraints.  Eventually I
think we'll need to support existential quantification, and I don't
think it'd be hard on the Mercury side.  But for now I think we can
ignore it.

-- 
Peter Schachte              Most people would sooner die than think, in fact
schachte at cs.mu.OZ.AU        they do so.
www.cs.mu.oz.au/~schachte/      -- Bertrand Russell 
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
--------------------------------------------------------------------------