Re: variable scope: the "metawriter" example

Thanks Dörthe for both your answers (short and long) ;-)

I must confess I didn't realize that my suggestion about changing the 
scope of bnodes had been already deployed... So my intention was not to 
compare EYE and CWM based on their different scoping rules...

And anyway, even with an explicit quantifierfor the existentials, EYE 
and CWM still fire the rules the same way:

   http://ppr.cs.dal.ca:3002/n3/editor/s/NCDP7v5S


On 15/10/2021 16:01, Dörthe Arndt wrote:
> Dear Pierre-Antoine,
>
> Sorry for my late answer (it is the first week of the semester, you can imagine that I am busy :) ).
>
>
> I wrote a very long answer below, which I will keep for those who are interested (sometimes you want long explanations).
>
> That cwm and EYE behave differently is just a consequence of the different blank node scoping they apply (you suggested a new scoping, that has been implemented in EYE but not in cwm, that is explained in the long answer). What is still interesting for me is of course the question how I would expect Cwm to behave with the local scoping.
>
>
>    :charlie :wrote { :bob :wrote [] }.
>
> means:
>
>   :charlie :wrote {\exists x. :bob :wrote x} .
>
> But does that mean that I can choose some kind of witness :w for x such that
>
>   :charlie :wrote { :bob :wrote :w } .
>
> Only if I can do that, the first rule (writer1) can fire.

Agreed. And initially, I was reluctant to allow this kind of witness, 
because we don't necessarily "trust" a quoted graph claiming that "there 
exists X such that...". However, I am gradually changing my mind about 
that, and here is the rationale.

In RDF, anybody can mint an IRI for anything, including things whose 
existence is not consensual. Therefore, we should probably not handle 
differently the two statements below:

   :alice :wrote { :bob :wrote 
<http://example.org/alice_s_namespace/a_book> }.
   :charlie :wrote { :bob :wrote [] }.

Why should we trust Alice with the existence of that Bob's writing, and 
deny that to Charlie? Just because Alice went into the trouble of 
minting an IRI? I don't think that really makes sense.

So yes, I now believe that it is sensible to create a witness for 
Charlie's blank node.

But then, how is it different from considering that all bnodes are 
existentially quantified at the top of the document?

>
> But if I can do that, can I also derive from
>
> :alice :wrote { :bob :wrote :abook }.
>
> that
>
> :alice :wrote { :bob :wrote [] }.
>
> That should cause the second rule to fire (writer2).
>
> I would normally agree with cwm and say, that my derivation here is not correct (think of a nice example with a negative predicate)
I am with you on this.
> and that cwm should therefore not apply the second rule for :alice, but the question is how to then defend the first derivation. Why should the first rule fire on :charlie?

I could very well live with allowing the first derivation and not the 
second.

In the first derivation, I see the witness as a syntactic trick to 
circumvent a scoping problem, but you didn't change the original quoted 
graph.

In the second derivation, you are replacing a quoted graph by another 
quoted graph that is entailed by the first one. Since quoted graphs are 
suppoed to be opaque, I don't think we should allow that.

>
> My current feeling is that I would still like the first rule to fire on Charlie, but I would need some explanation why it does so. But as said: our answer depends on our take on blank node scoping in general (we just need to answer this, if we stay local).
>
> Kind regards,
> Dörthe
>
>
>
>
>
>
>
>
>
>
> —— Here my old and long answer starts----------------
>
> Your example basically shows the two different options of blank node scoping we discussed before (you might know that, but I want to clarify to keep everyone in the discussion :) ).
>
> Cwm has the „classical“ scoping here, which was also implemented in EYE till you suggested to change it: all blank node scopes are local, i.e. the blank node is always quantified in the graph it occurs in.
>
>    :charlie :wrote { :bob :wrote [] }.
>
> means:
>
>   :charlie :wrote {\exists x. :bob :wrote x}
>
> In Eye, the blank node scoping is more complicated: the blank node scope is on document level (what I would have called global earlier) unless the blank node occurs in a rule, then the rule head or body is the scope.
>
>    :charlie :wrote { :bob :wrote [] }.
>
> means:
>
> \exists x.  :charlie :wrote {:bob :wrote x}.
>
> The interesting part is now, that these things also count for the rule head and body:
>
>>    @forAll :X, :Y, :Z.
>>
>>   { :X :wrote { :Y :wrote [] } } => { :X a :MetaWriter2 }.
> Means for EYE:
> \forall :X, :Y, :Z.  { \exists A. :X :wrote { :Y :wrote A } } => { :X a :MetaWriter2 }.
>
> That is logically equivalent to:
> \forall :X, :Y, :Z, A.  { :X :wrote { :Y :wrote A } } => { :X a :MetaWriter2 }.
>
> That is why the rule fires for :alice.
>
> For Cwm the formula means:
> \forall :X, :Y, :Z.  {:X :wrote { \exists A.  :Y :wrote A } } => { :X a :MetaWriter2 }.
>
> This is why the formula does not fire for :alice.
>
> But, if we have this view, the question is, should the first rule fire for :charlie here?
> Can we derive from
>
>>   :charlie :wrote { :bob :wrote [] }.
> Which means
>
>   :charlie :wrote {\exists x. :bob :wrote x} .
>
> and from
>>    @forAll :X, :Y, :Z.
>>
>>    { :X :wrote { :Y :wrote :Z } } => { :X a :MetaWriter1 }.
>>
>
> that :charlie is a :MetaWriter1?  I would say yes, but I think it is not as obvious as it seems.
>
>
> But to concretely answer your question:
>
>
>
>>
>> What is your take on this? I personally have not made up my mind on this...
> I still don’t like the dynamic scoping. But if we decide that blank nodes are quantified on document level unless they occur in a rule head or body, then I would follow EYE.
>
>
> The interesting part is the local scoping as it is present in cwm.
>
>>    pa
>>
>> <OpenPGP_0x9D1EDAEEEF98D438.asc>