Re: variable scope: the "metawriter" example

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.

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

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>

Received on Friday, 15 October 2021 14:01:50 UTC