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

[Ian MacLarty]

On Fri, Jun 02, 2006 at 04:57:33PM +1000, Mark Brown wrote:
> 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.
> 

They say more than that.  The three modes above say that the value of
any one of the arguments is a function of the value of the other two
arguments.

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

Okay I see.  Though I think that extra information you're talking about
is actually in those three mode declarations already.  There may be
other modes with any insts, but those three ground modes give the
"groundness assertions" you're talking of, don't they?

Of course using this information would mean doing something very
different with the modes at compile time (for example you probably
wouldn't want to generate code for those three modes, only the any
mode).  My point is that the extra information can be expressed with the
existing mode system as I see it.  Could you give an example of these
"functional dependencies" that couldn't be expressed with the existing
mode system?

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