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

[Mark Brown]

On 01-Jun-2006, Mark Brown <mark at cs.mu.OZ.AU> wrote:
> This is why I asked earlier for a theory about solver completeness.  The
> key questions I want to know about are:
> 
> 	1)  Given information about the completeness of atomic goals,
> 	how can we infer completeness information about compound goals
> 	containing them?
> 
> 	2)  What form does this information take?
> 
> 	3)  How much of this theory is valid for solvers in general, and
> 	how much of it is solver specific?  Is there any useful theory at
> 	all for solvers in general?
> 
> Here's some answers (not in the same order) for the case of the FD solver:
> 
> 	2)  The information takes the form of the functional dependencies
> 	mentioned above.
> 
> 	1)  Something similar to groundness analysis.  We calculate the
> 	closure of the induced dependencies and ensure that variables are
> 	ground before they are existentially quantified away.

That should be: we calculate the closure of the set of non-local variables
with respect to the induced dependencies, and ensure that all existentially
quantified variables are in this closure.  In other words, we check that
if all non-local variables are ground then all local variables are ground.

This is sufficient to ensure that all existentially quantified variables
in the program become ground by the time the program terminates (by
induction on the SLDNF tree).  And since main/2 has no solver variables
as arguments this means that all solver variables become ground, and hence
the program is solver complete for main/2.

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