[m-dev.] Implicit quantification

[Ben Schmidt]

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
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------