[m-dev.] Implicit quantification

[Mark Brown]

On 14-Jan-2007, Ben Schmidt <b.schmidt at ugrad.unimelb.edu.au> wrote:
> 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,

It is, according to the definition of "negated context" above.

> at least
> operationally. But I suspect in this case the implicit quantification
> is the whole goal anyway,

The scope of the implicit quantification is over the condition and the
then-branch.  It doesn't fit neatly around any particular goal, which is
why the manual is a bit awkward about it, I think.

> 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?

No, that part of the manual refers to variables that occur in the condition
*and* the then-branch, but not elsewhere.  The point is that variables can
be bound in the condition and then referred to in the then-branch, but not
anywhere else.

> 
> 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?

It's a bug.  The occurrences of A in the then- and else-branches should be
referring to a different variable than those in the condition.

Cheers,
Mark.

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