Re: New proposal for the semantics

Hi Pierre-Antoine,

Thanks very much for fleshing out your proposal. To me it seems reminiscent of the static vs. dynamic scoping discussion<https://lists.w3.org/Archives/Public/public-n3-dev/2021Jun/0033.html> we had before, at least, regarding the consequences of generating rules with blank nodes (but I could be wrong, of course). In your proposal:

    _:x a :Penguin.
    :bob :thinks {_:x a :Bird}.
    {:bob :thinks _:y}=>{{:bob :is :wise}=>_:y}.

|=

    {:bob :is :wise} => {_:x a :Bird}.
Where “_:x” would be considered as a universal variable when the rule is fired (I think?)

Similarly, a consequence of dynamic scope was as follows: "In the dynamic scope, this quantifier scope would be governed by where variable "ends up" during unification at runtime":

    _:y :b :c.
    {?v1 :b ?v2} => {{?v1 :u :v} => {?v2 :b :c}}.
|=
    {_:y :u :v} => {:c :b :c}.

(where _:y would be treated as an existential scoped on the rule premise, as this is where it ended up, and is hence equivalent to a universal)

Of course, I understand it is not wholly the same – in my case, the variable scope of “_:y” would already be changed to the rule premise, whereas in your proposal, it is “assigned” once the latter rule fires (this difference becomes very relevant in your “pathological example”). Still, the overall result is similar in that “_:y” (and “_:x” in your example) will be treated as a universal when the rule gets fired, I believe.

Now, I’m not trying to be flippant, but I believe this was disliked by Doerthe and yourself :-) and, I’m wondering what has changed.

Personally, I had already shot myself in the foot under that particular interpretation: I was generating rules that had widely different meanings depending on whether blank nodes or URIs were being used to structure the data. I believe this will be the result of this new interpretation as well (?) This did have one useful application – I could “compose” rule premises using quoted graphs, where the latter could include resource paths, and thus blank nodes, which would then be interpreted as proper rule variables. (Sorry if this summary is too concise – I can expand on this example if you like.)

You also mention that blank nodes outside of rules are not intrinsically quantified – but their scope does seem to be document-wide (as per Doerthe’s example 2)? I haven’t had the time to read your semantics document, so it may become clearer afterwards :-)


Thanks,

William

From: Pierre-Antoine Champin <pierre-antoine@w3.org>
Date: Tuesday, November 9, 2021 at 5:13 PM
To: public-n3-dev@w3.org <public-n3-dev@w3.org>
Subject: New proposal for the semantics

Hi all,

as discussed during yesterday's call, here is the new proposal for N3's semantics that I have been working on. Rather than delaying the discussion until I find the time to put everything in a proper document, here is a link to my scribbling, hoping that it will be legible enough.

    https://h.champin.net/nextcloud/index.php/s/QR9pxs96daamFoo/download


Below is a high level summary of the proposal, followed by some discussions and examples not present in the PDF. Apologies in advance for a long email.

Executive summary

N3 graphs are now made of IRIs, Literals and Variables. Variables are not intrinsically quantified -- their quantification (and the associated scope) is determined by their use.

* by default, they are considered as existentially quantified, just like blank nodes in RDF (simple interpretations, p2 in the PDF) -- actually, variables occurring only in quoted graphs are more like free variables than existentials.

* log:implies "interprets" the variables in its subject graphs as universally quantified. Variables that occur only in the object graph are considered as local existentials. This is captured by a semantic extension ("rule interpretation", p7 of the PDF)

* other builtins (e.g. e:forAll) may interpret variables in their subject and object in yet other ways, captured by additional semantic extensions (I have not worked on that yet)

This "schizophenia" of variables can have strange effects in a few corner cases (illustrated below), but my intuition is that those are exotic enough to not be a problem in practice.

Variables in concrete syntaxes can be represented by quick vars (?x), blank node labels (_:x) or anons ([...]). I would suggest that _:x and ?x are considered as different variables. This becomes important in the last section of this email.

Variables in facts / variables in rules

Consider the following graph, where the variable _:b1 occurs both at the top level and in a quoted graph.

    :alice :mother _:b1 .
    :alice :says { _:b1 a :NicePerson }.
    :bob  :mother _:b2.
    :bob  :says { _:b3 a :NicePerson }.
    { _:x :mother _:y; :says { _:y a :NicePerson } } => { :answer :is _:x }.

This would give answer :alice → a variable in quoted graphs "corefers" with the same variable outside any quoted graph.
However, variables in rules are treated differently:

    :alice a :Woman; :mother _:x.
    :alice :says { _:x a :NicePerson }.
    { _:x a :Woman } => { _:x a :Person }.

|=

    :alice a :Woman.

When the rule is fired, _:x is no longer considered as referring to Alice's mother, but as a universal variable, which can be bound to anything matching the condition (in that case, :alice).

Note that the same happens with my previous proposal (adopted by Dörthe yesterday, and implemented in EYE) → _:x in a rule is not the same as _:x outside a rule (although there are also subtle differences).

A consequence is that only named resources (i.e. IRIs and Literals) can be directly referred to by rules. One can look at it as if rules operated from "outside" the graph on which they are applied. Similarly, in the example above, another file can refer to :alice, but not to her mother.

Dörthe's example 1
  {_:x a :Penguin}=>{_:x a :Bird}.
  {_:y =>_:z}=>{_:y a :Premise. _:z a :Conclusion }.

|=

   {_:x a :Penguin} a :Premise.
   {_:x a :Bird} a :Conclusion.

Here, when the second rule is fired, _:y and _:z are interpreted as universals (and matched against the two quoted graph), but _:x in this context is just a free variable inside a quoted graph.

Dörthe's example 2

    _:x a :Penguin.
    :bob :thinks {_:x a :Bird}.
    {:bob :thinks _:y}=>{{:bob :is :wise}=>_:y}.

|=

    {:bob :is :wise} => {_:x a :Bird}.

My understanding of this example is that, if we further know that :bob :is :wise, then we would like to conclude that Bob's thought is true, i.e. that the penguin _:x is indeed a :Bird. Unfortunately, this is not what happens in this new proposal. Just as in the example of Alice's mother above, the _:x in the newly generated rule will not be related to the penguin _:x when the rule is fired. Instead, a new blank node would be generated.

Pathological example

    _:x a :Unicorn.
    { _:x a :Cat } => { _:x a :Animal }.
    { { _:s _:p _:o }=>_:c } => { _:s a :RuleSubject }.

|=

    _:x a  :RuleSubject, # derived from the rule above
             :Unicorn. # was alteady present in the graph

Here, it might be surprising that the _:x at the top level (referring to some unicorn) gets mixed with the _;x in the rule body (matching any cat). Didn't we say above that variables in rules are independent from their use outside the rule?

In fact, they are different only when the rule is fired. Here, the 2nd rule is fired, and its premise matches the 2nd triple of the graph, which has predicate log:implies but is not being used as a rule right now. So its subject and object are simple quoted graphs, with their variables "able to corefer" with variables at the top level.

I would argue that this example is pathological because there is not good reason to use the same variable in the rule and in some facts. It is allowed, it "works": the 2nd rule would fire correctly if we added  ":felix a :Cat." in the graph, for example. But it has no added value compared to using a distinct variable.

Encouraging people to use blank node labels only in facts, and quick vars only in rules, should keep them away from this kind of pathological examples. And since currently people do it because they have to, this looks like a reasonable guideline.

    _:x a :Unicorn.
    { ?x a :Cat } => { ?x a :Animal }.
    { { ?s ?p ?o }=> ?c } => { ?s a :RuleSubject }.

|=

    ?x a :RuleSubject.  # is derived
    _:x a :Unicorn.  # _:x the unicorn is a *different* variable



That's all follks. Thanks for reading all this! Hope it makes some sense.

  pa