[m-dev.] Implicit quantification

Mon Jan 15 16:03:11 AEDT 2007

```My original example:

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

Yes, I realised that...which is why I wrote 'truly', suspecting the
manual's definition to be not quite true.

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

So does this mean that there is no way to actually do explicitly what is
done implicitly? Because surely this is not valid:

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

Is it?! And if it is valid, surely the ';' isn't still 'else'?!

Now, consider this variation:

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

The implicit quantification should be the same, as the else part is a
parallel goal, so doesn't affect the hypotheses for the implicit
quantification. So do we assume this means, loosely,

(	some [A] ( A = "cat" -> A = "dog" )
;	A = "mouse"
).

Wouldn't this give mode errors, as A is bound in one branch of the
disjunction (if-then-else) but not the other? (I guess it wouldn't if
this were an entire predicate, as A would be existentially quantified
and thus not bound outside the predicate, but were the goal above part
of a conjunction, it would be a mode error, no?)

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

OK, that's fair enough. But can the variable then ever be referred to in
the else branch? Surely not, as that would give a mode error, wouldn't
it (like above)? So the quantification may as well be over the whole
if-then-else goal, mightn't it? And wouldn't that be heaps easier to
explain than a strange combined condition+then context?

> (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).

But (A, B) is surely not a negated context, is it? The manual says
nothing about implicit quantification where there is no negated context.
Isn't it actually implicitly quantified over the whole goal (i.e. whole
predicate): (A, B) ; (~A, C)?

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

Well, surely it's a bug that

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

fails?!

There's no way the programmer could indicate his intentions more clearly.

> This doesn't really matter that much, since it's easy enough for the programmer
> to just rename the variables apart.  But then, by the same token, we don't
> really need some/2 at all.

Since pragmatically the only thing 'some' does is limit the scope of
variables listed within a goal, if it doesn't actually do that...

I'd rather have a compile-time error, or at the very least a warning,
rather than have the code do what, IMHO, it clearly shouldn't.

I hate to think what universal quantification in the condition of an
if-then-else might do, what with double negation elimination and so on...

I heard it was said, "If a program is useful, it will have to be
changed. If a program is useless, it will have to be documented." At any
rate, I think this behaviour needs to be either fixed or documented. I'd
prefer it fixed, at least in the long term. And before it is fixed, or
if it is not to be fixed, it should at least be documented (section 2.9).

In terms of section 2.15, I'm still confused. Can someone provide an
example of where implicit quantification actually makes a difference
(whether by removing errors, or changing interpretation of a variable,
or, well, anything really)? I thought I could think of one/some before,
but am struggling now (it seems to me that implicitly quantifying over
an entire predicate would have the same effect as any implicit
quantification whenever that implicit quantification would actually
occur)! Maybe implicit quantification does nothing apart from confuse us!

Perhaps the biggest error in this section of the manual is the part
where it says

> closest enclosing scope (in a sense to be
> made precise in the following paragraphs)

Grins,

Ben.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au