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

[Ian MacLarty]

On Thu, Jun 01, 2006 at 03:38:31PM +1000, Mark Brown wrote:
> On 01-Jun-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > My take regarding recent discussion on the subject topic.
> > 
> > -----------------------------------------------------------------------
> > 
> > PROBLEM: goals that may succeed, but leave the hidden solver state
> > inconsistent (i.e., for which success does not correspond to truth).
> 
[...]
> > 
> > RECOMMENDATION: we (somehow, perhaps by annotation on mode declarations)
> > identify constraint posting predicates that may succeed, but leave the
> > solver state inconsistent.
> 
> If we were to adopt such a scheme, then I'd suggest putting the explicit
> annotation on the goals where success means consistent.  That is, by
> default we should assume that a program is not solver complete for calls
> to predicates with an `any' inst which do not have this annotation.
> 
> However, I don't think that attaching this information to modes is
> fine-grained enough.  Consider the goal `X = Y + Z' for FD variables X, Y
> and Z.  A program will be solver complete for this goal if at least two of
> the variables are ground at the time of the call (assuming a reasonable
> implementation of '+'), but may not be if only one of them is ground.
> 
> Peter Schachte pointed out to me that we may be able to express the condition
> we want by using something like functional dependencies.  E.g.: the signature
> for '+' could assert the dependencies
> 
> 	(X, Y -> Z), (X, Z -> Y), (Y, Z -> X)
> 

Could you elaborate on exactly what these functional dependencies mean?
What is the difference between the above constraints and having the
following three modes?

:- mode +(in, in, out) is det.
:- mode +(in, out, in) is det.
:- mode +(out, in, in) is det.

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