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

[Ian MacLarty]

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
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------