Issue with the scope of ?person in EXAMPLE: Applying an N3 patch.

[josd]

In the EYE implementation of N3 the scope of quickvars is the statement (i.e. triple or rule) level so in the EXAMPLE: Applying an N3 patch the quickvar ?person isn't co-referring hence the patch isn't working.
This has been a long standing N3 disagreement https://lists.w3.org/Archives/Public/public-cwm-talk/2015JanMar/0003.html
and in short, the assumption that the scope of quickvars is the parent graph leads to inconsistencies.

An alternative that works with EYE is at N3 patch example.

[josd]

To put it in a wider historical perspective, see https://lists.w3.org/Archives/Public/www-archive/2022Apr/0001.html

[doerthe]

Please note that the problem you describe does not only depend on the scoping of universals but rather to the way scoping of universals is combined with existential scoping.

To illustrate that, I go back to the example. Here and in all other examples, I will omit the following prefix-declarations:

@prefix solid: <http://www.w3.org/ns/solid/terms#>.
@prefix ex: <http://www.example.org/terms#>.

I will now also modify the subject such that we use an IRI instead of a blank node. We get:

ex:rename a solid:InsertDeletePatch;
  solid:where   { ?person ex:familyName "Garcia". };
  solid:inserts { ?person ex:givenName "Alex". };
  solid:deletes { person ex:givenName "Claudia". }.

Here, we do not have the problem we discussed earlier since cwm and EYE would both quantify the universals on top level and we would get twice the interpretation, namely (adding an FOL quantifier):

∀ person:

ex:rename a solid:InsertDeletePatch;
  solid:where   { person ex:familyName "Garcia". };
  solid:inserts { person ex:givenName "Alex". };
  solid:deletes { person ex:givenName "Claudia". }.

In this situation, the clause-based approach of EYE would be correct even if we follow cwm as

∀ p1.  ex:rename  solid:where   { p1 ex:familyName "Garcia". }.
∀ p2.  ex:rename  solid:inserts { p2 ex:givenName "Alex". }.
∀ p3.  ex:rename  solid:deletes { p3 ex:givenName "Claudia". }.

would be a logical consequence of the above. More concrete: we can derive all three triples for all variables p1, p2, p3. This allows us to only take conjuncts. Each of the conjuncts is on its own a consequence of the conjunction. Thus, when used with a IRI, the different instances of ?person do not need to co-refer.

The situation is different, if we use a blank node in the subject position (as we do in the example). Now, it depends on the order of the quantifiers.

We have:

@prefix solid: <http://www.w3.org/ns/solid/terms#>.
@prefix ex: <http://www.example.org/terms#>.

_:rename a solid:InsertDeletePatch;
  solid:where   { ?person ex:familyName "Garcia". };
  solid:inserts { ?person ex:givenName "Alex". };
  solid:deletes { ?person ex:givenName "Claudia". }.

The question is now, does that mean

Option1:

∃ rename
∀ person:

rename a solid:InsertDeletePatch;
  solid:where   { person ex:familyName "Garcia". };
  solid:inserts { person ex:givenName "Alex". };
  solid:deletes { person ex:givenName "Claudia". }.

OR

Option2:

∀ person:
∃ rename

rename a solid:InsertDeletePatch;
  solid:where   { person ex:familyName "Garcia". };
  solid:inserts { person ex:givenName "Alex". };
  solid:deletes { person ex:givenName "Claudia". }.

In other words: does the existential depend on the universal or does the universal depend on the existential.

If we follow the interpretation of Option1, we are in the same situation as with the IRI: the triples hold for ONE individual (marked by the blank node _:rename) and for all persons (?person).

If we follow Option2, then the existential depends on the universal in the sense, that we need to find a new instance of _:rename for each instance of ?person we encounter.

The last interpretation is what we actually need.

This issue was never discussed in the N3 group since it was not important for our use cases where universals always occurred in rules and could therefore not really interplay with blank nodes stated on top level. But I can say that the original team submission is clear in that case:

"If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials"

(see https://www.w3.org/TeamSubmission/n3/#Quantifica))

For the formalisation we do in the N3 group, we changed that order for practical reasons and because we did not carefully think of the consequences. But it is still possible to change it back (and I think that is what we should do). The use case here is the only case where the order matters and that one is broken if we put the existentials first.