# [mercury-users] Pred defns

Fergus Henderson fjh at cs.mu.OZ.AU
Fri Apr 3 01:37:10 AEST 1998

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

```