[m-dev.] Implicit quantification

[Mark Brown]

On 15-Jan-2007, Zoltan Somogyi <zs at csse.unimelb.edu.au> wrote:
> On 14-Jan-2007, Ben Schmidt <b.schmidt at ugrad.unimelb.edu.au> wrote:
> > 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"
> > ).
> 
> (A - > B ; C) is equivalent to (A, B) ; (~A, C), so A is in a negated context
> only if A fails (has no solutions). In your example, if these are all the
> occurrences of A, then A *is* in fact quantified, implicitly, over (A, B).
> 
> > 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?
> 
> That is not a bug. A "some" in the condition of an if-then-else extends
> to the then-part of the if-then-else as well.
> 
> The syntax may be a bit misleading,

That's why I consider it a bug.  In particular, if you expand the goal
out to the `(A, B) ; (~A, C)' form, leaving the explicit quantification in A,
then it no longer means the same thing.

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