[mercury-users] Pred defns

[Fergus Henderson]

On 31-Mar-1998, David Powers <powers at ist.flinders.edu.au> wrote:
> 
> I agree with Fergus about the operators (leaving aside arguments about which 
> symbols to use) and with Ralph about the capitalization.
> 
> Once we introduce the operator so that the accumulator never occurs
> unadorned, it IS acting as a VARIABLE and the construct is quite pure,

Almost, but not quite. 
The problem is that the quantification of the variable is not right.

For example, if you write say

	p(Z) #:-
		#X = 0,
		#Y = 0,
		##X = #X + 1,
		##Y = #Y + 2,
		Z = #Y - #X.

then logically p(Z) should be true not only for Z = 1, as you would expect,
but also for Z = 0, since X may be equal to Y.

To make it work, you would need to write something like

	p(Z) #:-
		new [X, Y] (
			#X = 0,
			#Y = 0,
			##X = #X + 1,
			##Y = #Y + 2,
			Z = #Y - #X
		).

where `new [X, Y] Goal' is an abbreviation for `new [X] new [Y] Goal',
and where `new [Var] Goal' is a new quantifier which indicates that
`Var' is a fresh name, distinct from any others.  That is,

		      	def
	new [Var] Goal	<=>  some [Var] (
					Goal,
					not some [V] (
						set__member(V, FV(Goal)),
						term_contains(V, Var)
					)
			     ).

		where FV(Goal) is the set of non-local variables of Goal,
		and where term_contains(Term, SubTerm) is true iff
		`Term' contains `SubTerm' as a sub-term
		(with a little fancy footwork for higher-order types,
		which I will leave as an exercise for the reader).

This `new' quantifier is like the `nu' quantifier in Martin Odersky's
lambda-nu calculus.  Using the `new' quantifier would avoid
undesirable aliasing between accumulators that are supposed to be distinct.

However, if using upper-case variable names would mean that you have to use
special quantifiers, then it's probably simpler to just use lower-case
variable names.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.