[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.
More information about the users
mailing list