Re: New proposal for the semantics

On 10/11/2021 17:10, Dörthe Arndt wrote:
> 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?
>
No I really meant tuples of element of \Delta_I (because elements of 
lists can be lists themselves). And I don't think that this amounts to 
say that \Delta_I is its own powerset, mostly because I consider that 
tuples (unlike subsets) are always finite (although this might need to 
be more explicit).

>   * Application of I (page 3): I guess it should be x\in img(Q_I)
>     instead of x\in img(Q^{-1}_{I})?
>
Indeed!
>
>   * 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)?
>
It is defined in the last line of p.3, for any function \gamma 
(lowercase): Variable → Term.
>
>   * 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?
>
Let me try to summarize the problem you see here:

   :tweety :can :fly.
|=
   :tweety :can :fly.
   { :tweety a :penguin } => { :tweety :can :fly }.
|=
   ?x :can :fly.
   { ?x a :penguin } => { ?x :can :fly }.

Is that it?

I believe the first entailment does not hold. I can construct a model 
for the 1st graph that is not a model of the 2nd graph:

   \Delta_I = { T, C, F } U { all tuples generated with T, C and F }
   Q_I = empty set
   V_I = empty set
   D_I maps T to :tweety, C to :can and F to :fly
   EXT_I = { (T, C, F) }

This interpretation trivially satisfies the semantic condition of 
rule-interpretations (no triple in EXT_I has D_I(log:implies) in the 2nd 
position).

--

The 2nd entailment, on the other hand, holds, and I agree this is a big 
problem :-(

More precisely, what we have is

   :markus a :penguin.
   :tweety :can :fly.
   { :tweety a :penguin } => { :tweety :can :fly }.
|=
   :markus a :penguin.
   ?x :can :fly.
   { ?x a :penguin } => { ?x :can :fly }.

 From this, it would seem that we must infer that :markus :can :fly. 
That would be a problem (as it is clearly not the intent of the first 
graph), but the problem is actually elsewehere. There exists a model of 
the 2nd graph (e.g. the Herbrand model of the 1st one) in which :markus 
can not fly. So ":markus :can :fly" is not entailed by the first graph 
(which is ok) but not entailed either by the 2nd one either (which is a 
problem). So rule-entailment actually fails to capture the semantics of 
rules :-(

Thanks for pointing that out. This is a bit frustrating, but that's 
progress ;-)

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

I believe that, for the subset of N3 graphs that are also RDF graphs, 
the proposed interpretations are effectively equivalent to Simple 
Interpretations...

   best

>
> Kind regards and expect my follow-up mail :)
> Dörthe
>
>> Am 09.11.2021 um 23:05 schrieb Jos De Roo <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

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