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

[Ralph Becket]

Mark Brown, Monday,  5 June 2006:
> In other words, the analysis gets it exactly right!

I know that: but in this case the analysis is completely useless! :-)

> > The crux of the debate, as I see it, is which of the two following
> > options is best:
> > 
> > (A) supply groundness inference details where possible and perform
> > groundness analysis in the compiler, requiring an explicit promise where
> > the analysis cannot prove solver completeness;
> > 
> > (B) don't bother doing groundness analysis, always require an explicit
> > promise.
> 
> If you're talking about an explicit promise for each existentially
> quantified variable, then that's a lot of promises.  Particularly when
> then compiler introduces lots of variables.

I was thinking of a promise at the boundary between "solver code" and
"non-solver code" in a procedure that has no inst any parameters.

> If you're talking about an explicit promise at the top level of your
> constraint solving code, then this will provide no help whatsoever in
> either verifying completeness or, if the program is incomplete, in
> localising the problem.

I'm saying I expect your analysis will only help sometimes with some
solvers (FD and ...?) and that (B) is as good as you can get the rest
of the time.

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