[m-dev.] Implicit quantification

[Zoltan Somogyi]

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, but it isn't our syntax; we inherited it
from NU-Prolog. I don't think anyone has proposed any better syntax.

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