[mercury-users] Re: Determinism detection (Was Newbie problem.)

[Peter Schachte]

On Wed, Jun 16, 1999 at 11:53:47PM +1000, Fergus Henderson wrote:
> On 16-Jun-1999, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> > Note that in general these things will have multiple
> > arguments, some output, so you need to be careful with quantifiers
> > (the examples given are simplistic in this respect).
> 
> Yes.  Richard O'Keefe's and Peter Schachte's suggestions didn't
> discuss situations with multiple arguments.
>
> In general I'm pretty supportive of their general approach, but I would
> like to see a more detailed and complete proposal.

I won't give a complete proposal now, but I think the multiple
argument problem isn't so difficult.  I think the "variables are
quantified as tightly as possible" view works pretty well here, too.

<digression>
Note on notation: I agree with Richard that we must distinguish
between exclusive and exhaustive groups of predicates, so I'll extend
my proposal to cover both concepts.  I also agree that syntax isn't so
important yet, but in the interest of concreteness, I'll use
`exclusive' and `exhaustive' as :- op(1100, fy, [...]) operators; I
also take writing
	:- exclusive exhaustive ... 
is the same as
	:- exhaustive exclusive ...
is the same as
	:- exclusive ...
	:- exhaustive ....)
</digression>

Take the example

	:- exclusive foo(X, Y), bar(X, Z), baz(W, X, Y).

X and Y would be quantified over all the goals, and W and Z would be
quantified over the single goals they appear in:

	:- all [X,Y] . exclusive
			foo(X, Y),
			(exists [Z] . bar(X, Z)),
			(exists [W] . baz(W, X, Y)).

This means all of these must hold:

	all [X,Y] . (foo(X,Y) => (\+ exists [Z] . bar(X, Z)),
				 (\+ exists [W] . baz(W, X, Y))).

	all [X,Y] . (exists [Z] . bar(X, Z)) => 
			(\+ foo(X, Y)),
			(\+ exists [W] . baz(W, X, Y)).

	all [X,Y] . (exists [W] . baz(W, X, Y)) => 
			(\+ foo(X, Y)),
			(\+ exists [Z] . bar(X, Z)).

And

	:- exhaustive foo(X, Y), bar(X, Z), baz(W, X, Y).

means:

	all [X,Y] . 
		(   foo(X, Y) 
		;   (exists [Z] . bar(X, Z))
		;   (exists [W] . baz(W, X, Y))
		).

-- 
Peter Schachte                     History teaches us that men and nations
mailto:schachte at cs.mu.OZ.AU        behave wisely once they have exhausted
http://www.cs.mu.oz.au/~schachte/  all other alternatives.
PGP: finger schachte at 128.250.37.3      -- Abba Eban 
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------