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

Ian MacLarty maclarty at cs.mu.OZ.AU
Fri Jun 9 10:22:46 AEST 2006

```On Wed, Jun 07, 2006 at 09:12:13PM +1000, Peter Schachte wrote:
> 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.
>

Groovy.

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

That one went over my head.  If => means there may be multiple
solutions, then shouldn't you have (X, Y -> Z), (Z => X, Y) instead of
(X, Y <-> Z)?

Ian.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au