[m-dev.] Implicit quantification

[Ben Schmidt]

Hi,

I am finding section 2.15 of the reference manual inaccurate, or at
the very least unclear, and not finding I understand the
quantification rules instinctively as I thought I did, either.
The section of the manual currently reads:

 > The rule for implicit quantification in Mercury is not the same as
 > the usual one in mathematical logic. In Mercury, variables that do
 > not occur in the head of a clause are implicitly existentially
 > quantified around their closest enclosing scope (in a sense to be
 > made precise in the following paragraphs). This allows most
 > existential quantifiers to be omitted, and leads to more concise
 > code.
 >
 > An occurrence of a variable is in a negated context if it is in a
 > negation, in a universal quantification, in the condition of an
 > if-then-else, in an inequality, or in a lambda expression.
 >
 > Two goals are parallel if they are different disjuncts of the same
 > disjunction, or if one is the “else” part of an if-then-else and the
 > other goal is either the “then” part or the condition of the
 > if-then-else, or if they are the goals of disjoint (distinct and
 > non-overlapping) lambda expressions.
 >
 > If a variable occurs in a negated context and does not occur outside
 > of that negated context other than in parallel goals (and in the
 > case of a variable in the condition of an if-then-else, other than
 > in the “then” part of the if-then-else), then that variable is
 > implicitly existentially quantified inside the negation.

Now, following the wording of the manual, in the following example, A
is in a negated context (condition of if-then-else) and does not
appear other than in the then part, but it is not existentially
quantified inside the negation (condition part), but shares the scope
with the then part, and thus fails:

(	A = "cat"
->	A = "dog"
;	B = "mouse"
).

Presumably this is because when the condition succeeds, this is
equivalent to conjunction of the condition and the 'then' part. As
such, the condition isn't truly in a negated context, at least
operationally. But I suspect in this case the implicit quantification
is the whole goal anyway, as my suspicion is that the manual should
read something like

 > If a variable occurs in a negated context and does not occur outside
 > of that negated context other than in parallel goals (and in the
 > case of a variable in the condition of an if-then-else, *ALSO DOES
 > NOT OCCUR* in the “then” part of the if-then-else), then that
 > variable is implicitly existentially quantified inside the negation.

Is this right? Or is there some other subtlety? Can someone clarify?

I'm also surprised that the following goal fails when compiled. I
expected it to succeed.

(	some [A] ( A="Cat" ; A="Dog" )
->	A="Mouse"
;	A="Canary"
)

Shouldn't the condition succeed without binding A outside of the
existential quantification, and then the 'then' part succeed, binding
A? Could someone explain this, or confirm that it's a bug?

Similarly, I would expect that if the condition were to fail, e.g.
had it a conjunction rather than a disjunction, A would
be bound solely by the 'else' part, and still the goal succeed. Is
that correct? (The compiled code does behave this way in this case.)

Back on the issue of the manual, I think the terminology 'parallel
goal' is also slightly confusing, given that concepts such as parallel
conjunction are now being introduced. Luckily this isn't giving me
problems, but I imagine it has potential to be confusing. If we could
change terminology, I think it would be helpful. Any ideas or
thoughts?

Ben.


--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------