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

[Mark Brown]

On 02-Jun-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
> On Thu, Jun 01, 2006 at 03:38:31PM +1000, Mark Brown wrote:
> > 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?

They express relationships between the groundness of solver variables.
`X, Y -> Z' means that (X is ground) and (Y is ground) implies (Z is ground).

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

Mode declarations put constraints on the call patterns, so you wouldn't
be allowed to call this '+' unless two of the arguments are already ground.

With the constraint solving version of '+' the variables have inst `any'
at the time of call -- none of the variables need be ground.  Any time after
the call the relationship above will hold, so if X and Y become ground
sometime later on then Z will also.

The "functional dependencies" or "groundness assertions" or whatever we want
to call them provide extra information about the `any' insts which we
otherwise wouldn't have.

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