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

[Mark Brown]

On 02-Jun-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> On Thu, Jun 01, 2006 at 07:09:56PM +1000, Mark Brown wrote:
> > 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).

The condition that we want to prove is that all variables eventually become
ground.  This is sufficient (although not necessary) for completeness of the
FD solver.

Trying to prove that a variable is dead (which I take to mean that all
constraints on it are entailed and there won't be any further constraints
put on it) is much harder, and I don't intend to try to do that!

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

This one's easy.  For r(A, B, C), it is straightforward to infer the
dependencies (A, B -> C) and (C -> A, B).  Or, if you like,
A' /\ B' <-> C', where A' is the proposition that A is ground, etc.

Therefore, for the body of p/2 we have that Z' -> X' /\ Y'.  Further, we
have for the goal p(Y, Z) that Z' -> X' /\ Y' (where X is no longer in
scope).

So to make the goal p(Y, Z) solver complete it is sufficient to add
something that makes Z ground -- this will ensure all other variables,
including those no longer in scope, become ground.

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

Agreed -- it could never be as precise as we would like.

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

Yes, we definitely don't want the former.  One way to ensure that the
variable has a satisfying value is to allow yet another promise:

	promise_some [X] (
		... Goal which may not ground X ...
	)

Declaratively and operationally `promise_some' means exactly the same
thing as `some'.  The difference would be in the static semantics: the
compiler wouldn't need to ensure that X becomes ground.

Whether this would wind up being too awkward depends, it seems, on exactly
how imprecise the groundness analysis I'm describing is.  I think I should
leave that question up to your judgement.  ;-)

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