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

[Ralph Becket]

Peter Schachte, Thursday,  1 June 2006:
> > 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 far we don't have any notion of solver id.

The key point is that a conjunction in a CLP program may succeed
operationally, but be false denotationally.

> So how about, eg,
> 
> 	:- mode any < any is semidet + incomplete(cint).
> 
> 	:- mode cint.ensure_complete is semidet + completes(cint).

I'd really rather not get into syntax too early.  In particular, here
you're positing a static naming scheme for solvers, but I'm not sure
that's a good idea in light of PJS' statement that at some point in 
the future we may want multiple instances of particular solvers in the
same program.

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

I don't think you can solve this problem.

My position in a nutshell is that there are enough situations where
program analysis either can't help or is unlikely to help that we
probably shouldn't bother.  Instead we should
- expect solvers to provide a "check everything" predicate,
- leave it up to the user to call these appropriately,
- require a promise scope of some kind in the program stating that the
  operational semantics of the enclosed goal match its denotational
  semantics (i.e., that success corresponds to definite truth, not
  possible truth); this promise scope should appear at the junction
  in the code between "non-solver space" and "solver space".

[I don't think of interval "solvers" as solvers, because they never tell
you anything positive.]

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

Indeed, so we don't have to worry about them 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.

I was thinking just

:- constraint cint < cint.

(i.e., a constraint is a special kind of pred).

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

Groundness information disappears very quickly in CLP programs.
Therefore virtually all CLP goals will be inferred as solver incomplete
(what a terrible name...)
I doubt there's much value in adding incomplete(cint) annotations to 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).
> 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.

Many, many solvers are solver incomplete.  But Mark's point in a
different reply addresses this issue nicely, IMO.

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

Yep!  But it can't be that hard to remember either every constraint or
every variable.  The cost will be very small.

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

Constraints etc. are garbage collected on backtracking, which should be
okay.

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