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

[Peter Schachte]

On Thu, Jun 01, 2006 at 07:09:56PM +1000, Mark Brown wrote:
> On 01-Jun-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> > Since you need to indicate which solver(s) they are incomplete
> > relative to, you'll need to list the incomplete ones anyway.
> 
> I don't understand this point.
> 
> Elsewhere in the thread, you explained:
> > 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.
> 
> I'm not entirely sure what you mean by a solver id.

It doesn't mean anything by itself, it's just a way of insulating the
incompleteness caused by some predicates from the incompleteness
caused by others.  Typically, it'll just be a solver type name.  Eg,
suppose fd.alldifferent/1 is incomplete and fd.label_everything/0 is
"completing" (ie, it makes the computation complete), and that
interval.whatever/N is incomplete, and you call fd.alldifferent/1
followed by interval.whatever/N, then fd.label_everything/0 can't make
the computation complete, it can only complete the fd part of it.
You'll need to also call some completing predicate for the interval
solver to make the computation complete.  So the completeness state at
a program point must be the set of solvers for which the computation
is incomplete.

> I agree, but I suspect we're talking about different problems.
> 
> More to the point, the following goal is fine:
> 
> 	some [Y, Z] (
> 		X `neq` Y,
> 		Z = c(0),
> 		X = Y + Z
> 	)
> 
> Failure will occur at the latest when X eventually becomes ground, which
> will have to occur before X is quantified away.

I don't think you can reliably detect when an individual variable is
dead (ie, will not have any further constraints posted).  Take this
example:

	p(Y, Z) :-
		some [X] (
			X < 7,
			r(X,Y,Z)
		).

	r(X, Y, [X|Y]).

Here X is quantified (and therefore scoped) to the body of p/2.  But
in fact it escapes through Z.  You really don't want the solver to
ground X at the foot of p/2; it should be left until later.
Distinguishing this case from your example would require some kind of
possible aliasing analysis, and could never be precise.  So ultimately
we'll have to either sometimes force a variable to be ground even
though it will have more constraints added later, or sometimes allow a
variable to become inaccessible without ensuring that it has a
satisfying value.  For performance reason, I think we have to choose
the latter.

Unfortunately, this means that solvers will always have to track all
their variables.  But it does not mean that we can't, with a possible
aliasing analysis, sometimes let a solver know when one of its
variables is becoming dead.

In fact, there's a simple trick we could use to spot some such cases
without a proper possible aliasing analysis.  In my example above,
r/3's mode must have a final inst of any for Z.  If there are no
atomic goals which pass X and have some other argument with a final
inst of any, then we know X can't escape (because any-ness is
contageous to containing terms).  In fact, even if there are other
any-inst arguments, we can still sometimes guarantee no escape.  If
all other arguments with final inst any have the same type as X, then
we can still guarantee that X doesn't escape, because only the solver
itself could have aliased it (and we're asuming the sovler tracks such
aliasing).

So I suspect with a rather simple test we could catch many cases where
we could promise a solver that certain variables were dead.  Solvers
could use this information to detect contradictions earlier than they
otherwise might, as well as to possibly reclaim some internal data
structures.  Of course, they would also have to be careful of
backtracking forcing the recreation of that variable.

This is a lot more work than simply tracking possible incompleteness.
I think we should do both, but I think possible incompleteness
tracking will be necessary and easier, so we should do it first.


-- 
Peter Schachte              A rock pile ceases to be a rock pile the moment
schachte at cs.mu.OZ.AU        a single man contemplates it, bearing within him
www.cs.mu.oz.au/~schachte/  the image of a cathedral.
Phone: +61 3 8344 1338          -- Antoine de Saint-Exupery 
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------