Re: New proposal for the semantics

  *
Dear all,

I am writing from a different e-mail-address, so I am not sure whether I can include the whole mailing list. Please do not forget to include the list again when you answer (I promise, I will fix that issue).

I also messed up with the lay-out. I try to mark my own answers as good as possible (with -> and in green). Sorry if there is still confusion


Now, to answer the mail:

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

-> I see what you mean. I need some time to think it through. I still think that we need more restrictions here, but if so, we can find them.


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

ANSWER STARTS HERE

-> No, I wanted to get somewhere else, but I think that both of your observations are interesting. What I wanted was:

  :tweety :can :fly.
:markus a :penguin.

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

Does not entail:

:markus :can :fly.

Assume that we have an interpretation I for all the triples and rules which do not contain variables. Now, let’s consider the rule with the variable. For that ?x in the rule we can find a grounding which assigns :tweety to ?x. Then we have

( I[\Gamma]( { ?x a :penguin }),  I[\Gamma](log:implies),  I[\Gamma]( { ?x :can :fly }))= ( I({ tweety a :penguin }, I(log:implies),  I ({ :tweety :can :fly }))

As I models { :tweety a :penguin } => { :tweety :can :fly }., we know that ( I({ tweety a :penguin }, I(log:implies),  I ({ :tweety :can :fly })) \inEXT_I.

We furthermore have that fo all  ( I({ tweety a :penguin }, I(log:implies),  I ({ :tweety :can :fly })) \in EXT_I the rule conditions hold (I models  { :tweety a :penguin } => { :tweety :can :fly }.).

So, we can find a model for our formulas above where the triple: :markus :can :fly. Does not hold.

So, there must be some special handling for rules? What stops me from grounding them as I would do for any other predicate?

ANSWER ENDS HERE


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

-> That is interesting, so rules now actually also need to be claimed in order to be derivable from the formulas. That is nice because I do not expect that any reasoner will be able to produce all rules which can be derived from the data.

Then

  :tweety :can :fly.
not(|=)
  :tweety :can :fly.
true => { :tweety :can :fly }.

Interesting.



--

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


-> OK, that is actually very similar to the problem I wanted to discuss. The problem comes from the special nature of log:implies and I think we will have to give it a special treatment here. I am not sure whether it can remain being a „normal“ predicate (even though I like the non-entailment caused by that). But indeed, let’s think about it. The progress does not end here :)

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

-> Now I see it. There is now slight difference for the handling of blank nodes since we will have to find „witnesses“  for each blank node (all instances of the universe the blank nodes point to will need to have a name, even though we will never use that name anywhere), but I think we would have to do that in all our solutions because of the referential opacity.


Kind regards,
Dörthe


  best

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







----- Weitergeleitete Nachricht -----
Von: Doerthe Arndt <doerthe_arndt@yahoo.de<mailto:doerthe_arndt@yahoo.de>>
An: doerth.arndt@tu-dresden.de<mailto:doerth.arndt@tu-dresden.de> <doerth.arndt@tu-dresden.de<mailto:doerth.arndt@tu-dresden.de>>
Gesendet: Montag, 15. November 2021, 14:19:31 MEZ
Betreff: Fw: New proposal for the semantics



----- Weitergeleitete Nachricht -----
Von: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu<mailto:pierre-antoine.champin@ercim.eu>>
An: Dörthe Arndt <doerthe.arndt@ugent.be<mailto:doerthe.arndt@ugent.be>>; Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>>
CC: public-n3-dev@w3.org<mailto:public-n3-dev@w3.org> <public-n3-dev@w3.org<mailto:public-n3-dev@w3.org>>
Gesendet: Montag, 15. November 2021, 14:15:57 MEZ
Betreff: Re: New proposal for the semantics

More thoughts

On 15/11/2021 13:32, Pierre-Antoine Champin wrote:
> (...)
>
> 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 ;-)
>
My gut feeling is that this issue is causes by the merging of blank
nodes and quick vars into a single kind of variables... Handling them
differently might help solve this problem. I'll think about it.


  pa