Re: New proposal for the semantics

Hi Pierre-Antoine,

Thank you very much, it makes a lot of sense and I really like it!

I am also happy that we could then drop Skolem IRIs in EYE ;-)

Currently EYE seems to be happy with the examples except for the
pathological one which does not work due to a variable predicate
issue but http://ppr.cs.dal.ca:3002/n3/editor/s/zEiNj22t works :-)

Jos

-- https://josd.github.io


On Tue, Nov 9, 2021 at 10:13 PM Pierre-Antoine Champin <
pierre-antoine@w3.org> wrote:

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