Re: New proposal for the semantics

Dear Pierre-Antoine,

Thank you for your proposal. For a draft it is very well readable.  I was very much looking forward for our virtual „semantics-ping-pong“, so let’s get started :) (and hopefully get a nice theory out)

Some basic questions to better understand:



  *   Definition of the Interpretation (page 2): I guess there is a typo in the definition of \Delta_I since you somehow claim that the set is its own power-set (which can’t be). So, do you mean that any tuple of elements of IRI \cup Literal \cup Variable is in \Delta_I, or what do you actually mean?

  *   Application of I (page 3): I guess it should be x\in img(Q_I) instead of x\in img(Q^{-1}_{I})?

  *   How is Q^{-1}_I(\Gamma_T(x)) is x is a graph defined? I guess we simply replace all occurrences of variables by their \Gamma_T(x)?

  *   Do you separate log:implies from „normal“ predicates? Otherwise we could get problems with the variables in the rules

Example: Let us assume that the following fact holds:

:tweety :can :fly.

That means that also the rule: {:tweety a :penguin.}=>{:tweety :can :fly.}. (simply because tweety can fly anyway)

So, if we had a rule {?x a :penguin.}=>{?x :can :fly.}. we could make that true with

\Gamma(?x)=(D_I(:tweety), :tweety), (D_I(:tweety), D_I(:can), D_I(:fly))\in EXT_I and
(Q^{-1}_I(\Gamma_T({ ?x a :penguin })), D_I(log:implies), Q^{-1}_I(\Gamma_T({ ?x :can :fly })))=(Q^{-1}_I({:tweety a :penguin })), D_I(log:implies), Q^{-1}_I(({ :tweety :can :fly })))\in EXT_I In that case the rule should not fire on :midas a :penguin. and not derive that :midas :can :fly. But in my understanding we still have a valid interpretation here, so what am I missing?



I did not enough time to look into your proposal yet, so I apologize if my questions are too simple. You will get more elaborate questions later (most likely after me biking home since I need to think it through ;) ).

Ah, one additional remark: did you consider how we align with RDF? Because that RDF alignment with my reason to not go for a semantics with explicit quantification in the first place. I am still wondering whether we should do that instead since it would simplify things a lot (we might even go towards FOL if we are already on that track).

Kind regards and expect my follow-up mail :)
Dörthe

Am 09.11.2021 um 23:05 schrieb Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>>:

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<https://josd.github.io/>


On Tue, Nov 9, 2021 at 10:13 PM Pierre-Antoine Champin <pierre-antoine@w3.org<mailto: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