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

[Peter Schachte]

On Fri, Jun 02, 2006 at 05:45:06PM +1000, Ian MacLarty wrote:
> Could you give an example of these
> "functional dependencies" that couldn't be expressed with the existing
> mode system?

Yes.  They also imply mode segments.  Eg,

	(X, Y -> Z), (X -> W)

means that we can compute W from X in the absence of Y.  Suppose this
is the mode for a predicate p(X, Y, Z, W), and consider the clause 

	q(X, Z) :- p(X, W+1, Z, W).

Mercury's current mode system can't mode this.  But with functional
dependencies, we have 

	X -> W,
	W -> W+1,		+ is a function, after all
	X, W+1 -> Z
	therefore X -> Z	by modus ponens

so it's well-moded.  The compiler could generate separate code for the
X -> W part of p/4 (call it p_1) from the code for the X, Y -> Z part
(p_2).  So the code for q(in, out) calls p_1 to compute W, calls + to
compute W+1, then calls p_2 to compute Z.

It gets more interesting, too, when the arguments are compound term
types.  Eg, append(X,Y,Z) could have a mode like

	(X, Y <-> Z),
	=> X.backbone, 
	(Y.backbone <-> Z.backbone)

or something like that.  The second line is meant to say that the
backbone of X is always all bound on exit, though there may be
multiple solutions.  The third says that the backbones of Y and Z are
always equally bound (on exit).  So if the backbone of X is bound,
then append/3 will be deterministic.

It obviously needs a better syntax, but something like that should
capture everything that needs to be said about append/3, other than
which modes the compiler should actually generate code for.  I'd
really love the compiler to work that out itself.  Oh, it doesn't
cover uniqueness, though I think it should cover any-ness.

-- 
Peter Schachte              The universe is full of magical things,
schachte at cs.mu.OZ.AU        patiently waiting for our wits to grow sharper.
www.cs.mu.oz.au/~schachte/      -- Eden Phillpotts 
Phone: +61 3 8344 1338      
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------