Re: N3 semantics new-new proposal

Dear Pierre-Antoine,


> > Thank you for your proposal, I am still thinking about it and have a > few first questions/remarks: > > > 1. Can you explain, why |_:x :says { _:x a :Unicorn }| is equivalent > to |_:x :says { _:y a :Unicorn }?|

call the two graphs G1 and G2 respectively.

G1 |= G2 because for any model I of G1, we have I |= G2
by choosing R(_:y)=_:x (R(_:x) has to be ≠ _:x, but its value does not matter))

My whole remark was about this last point: does the value really not matter?:

We know that  I({ _:y a :Unicorn })≠I({ _:x a :Unicorn }) for all _:x≠_:y because Q_I is injective.

That means no matter how I rename my _:x, the renaming will cause that the cited graph with the new variable has a different meaning than the graph with _:x.

The only reason why the value really does not matter is that Q_I is partial and that therefore there could be a variable _:z for which the original model I has no interpretation for { _:z a :Unicorn } (and for no other cited graph, so, _:z \not\in Var_I). That could be used to define a new I. So we do not have  I |= G2 but we can make a new I’ such that  I' |= G2.

It interesting here that the trick only works if there always exist variables which are not in img(Q_I).


𝑄


and by choosing A(R(_:x)) appropriately such that the (top-level) triple is satisfied by EXT_I.

G2 |= G1 because for any model I of G2, we have I |= G1
by choosing R(_:x)=_:y,
and by choosing A(_:y) such that the (top-level) triple is satisfied by EXT_I.


That direction is indeed easier and we can have the same model.


More generally, a model of a graph G does not need to contain exactly the quoted graphs from G in its mapping Q_I... It only to contain them modulo some renaming.


I see your point, but I still think that it is very tricky.



> According to your interpretation, { _:x a :Unicorn } and { _:y a > :Unicorn } have different interpretations.

You seem to assume that models of G1 and/or G2 would contain both graphs in img(Q_I), but that does not have to be the case.

Here is a minimal model for G1 and G2:

Delta = { Alice, Says, G, ImaginaryUnicorn }
Q_I = { G → `_:z a :Unicorn' }
D_I = { :says → Says, _:z → ImaginaryUnicorn }
EXT_I = { (Alice, Says, G) }

Both are entailed by this interpretation, renaming _:x or _:y to _:z, respectively, and assigning R(_:x) to Alice.


Yes, you are right. I did not think about the fact that not all possible graphs are in the image of Q_I.  But in general we need to be more careful with renaming if the variables can have fixed interpretations.


> (...) I would like if |{ _:x a :Unicorn } and { > _:y a :Unicorn } had the same meaning or at least could have the same > meaning. Why don’t we need that?

I hope I made it clearer why (I think) we don't need that *in the G1 vs. G2 example*.
However, considering G3:

  :alice :says { _:x a :Unicorn }.
  :bob :says { _:y a :Unicorn }.

Here, any model would contain two isomorphic graphs, with different meaning. That might be a problem... :-/

Here, I agree, but I now understand why the other part can at least be solved.


> > > 2. Your entailment |:alice :smurfs { :bob :likes _:x }.| To > > |_:x :smurfs { :bob :likes _:x }.| > > Has as a consequences that > > :alice :smurfs { :bob :likes _:x }. {?x :smurfs {:bob :likes ?x}}={?x > a :auto-smurf}. > > Leads to > > _:x a :auto-smurf. > > I think that could be a problem.

I am not sure that this entailment holds, but there is a problem nonetheless.


Ah, I see (also from the example below). If we have variables which get replaced by variables we still have local quantification. So, my example would entail that there exists an auto-smurf (_:u a :auto-smurf.) but that does not have to be _:x.

Binding rule-variables to other variables is actually tricky, and does not work as expected.

Consider G3:

  _:x a :Cat.
  _:y a :Unicorn.
  { _:z a :Unicorn } => { _:z :can :Fly }.

this does *not* entail G4:

  _:y a :Unicorn ; :can :fly.

Consider the following interpretation

  Delta = { X, A, Cat, Y, Unicorn, Z, Gb, Implies, Gh, Can, Fly, Superman }
  Q and D as one would expect
  EXT = { (X A C), (Y A Unicorn), (Gb Implies Gh), (Superman Can Fly) }

This interpretation clearly does not satisfies G4, and still, it satisfies G3 in a nasty way:
choosing β(_:z) = _:w, we have I |= β(Gb) (e.g. with R=Id and A(_:w) = Y),
so we MUST have I |= β(Gh)... which is true by chosing R=Id and A(_:w) = Superman!


OK, so we keep the local scoping if we replace the variable by another one. We could also make sure that the result is ground and use a grounding function for our „normal“  blank nodes as well, but then we would deviate from RDF.

Jos was right: defining the semantics of log:implies in terms of a renaming was a very bad idea!

In the next iteration, I plan to consider β as a mapping from Variables to Delta, directly.


If you do that, nested graphs remain tricky in my opinion. Consider the example from above (with some additions):

_:x :smurfs { :bob :likes _:x }.
:alice :smurfs { :bob :likes _:x }.
:alice :smurfs { :bob :likes :alice }.
:alice :smurfs { :bob :likes :kate }.

{?x :smurfs {:bob :likes ?x}}=>{?x a :auto-smurf}.

What do we get out?

Some questions:


  *   Does  _:x :smurfs { :bob :likes _:x }.  {?x :smurfs {:bob :likes ?x}}=>{?x a :auto-smurf}. result in _:x a :auto-smurf or at least in _:something a :auto-smurf?
  *   Is {?x :smurfs {:bob :likes ?x}}=>{?x a :auto-smurf}. equivalent to {?x :smurfs {:bob :likes ?y}}=>{?x a :auto-smurf}. To put it differently: does
:alice :smurfs { :bob :likes :kate }.
{?x :smurfs {:bob :likes ?x}}=>{?x a :auto-smurf}.
entail :alice a :auto-smurf.
  *   Is _:x :smurfs { :bob :likes _:x }.
equivalent to _:x :smurfs { :bob :likes _:y }.
  *   Does
:alice :smurfs { :bob :likes :alice }.
{?x :smurfs {:bob :likes ?x}}=>{?x a :auto-smurf}.
entail
:alice a :auto-smurf.

If we only have one type of variable, it is difficult to define whether scoping is local or global. I think _:x :smurfs { :bob :likes _:x }. should have the same meaning in a rule premise as if it occurred in a plain triple. If the scope is local (so the two x in the triple do not need to refer to the same resource or have some similar but weaker connection), then we will loose the power ro reason over graphs (often you want to ground a graph pattern based on its context).

The more I think about it the more I wonder whether it makes sense to distinguish between local and global variables. But I know that it would not stop there and that we would get more problems with „semi-local“ variables.

I am looking forward to your response and the next proposal. If you want some help to brainstorm, please let me know.

Kind regards,
Dörthe


  best

> > > I am still preparing more questions (but I have to think about > log:notIncludes first :) ). > > Kind regards, Dörthe | | > > >> Am 29.11.2021 um 15:33 schrieb Doerthe Arndt >> <doerthe_arndt@yahoo.de<mailto:doerthe_arndt@yahoo.de> <mailto:doerthe_arndt@yahoo.de><mailto:doerthe_arndt@yahoo.de>>: >> >> >> >> ----- Weitergeleitete Nachricht ----- *Von:* Jos De Roo >> <josderoo@gmail.com<mailto:josderoo@gmail.com> <mailto:josderoo@gmail.com><mailto:josderoo@gmail.com>> *An:* >> Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu ><mailto:pierre-antoine.champin@ercim.eu>> <mailto:pierre-antoine.champin@ercim.eu><mailto:pierre-antoine.champin@ercim.eu>> *CC:* >> public-n3-dev@w3.org<mailto:public-n3-dev@w3.org> <mailto:public-n3-dev@w3.org><mailto:public-n3-dev@w3.org> >> <public-n3-dev@w3.org<mailto:public-n3-dev@w3.org> <mailto:public-n3-dev@w3.org><mailto:public-n3-dev@w3.org>> *Gesendet:* >> Donnerstag, 25. November 2021, 23:19:47 MEZ *Betreff:* Re: N3 >> semantics new-new proposal >> >> Hi Pierre-Antoine, >> >> This is just a quick feedback about the very last paragraph ;-) >> >> Looking at log:notIncludes I found a floundering issue in our >> implementation. It is fixed in the latest EYE which now expects the >> object of log:notIncludes to be ground at reasoning time. >> >> So only >> >> :gang :contains :bob, :charlie. :alice :says { :bob :name "bob" }. >> { :alice :says _:g. _:g log:notIncludes { _:s :name "bob" }. :gang >> :contains _:s. } => { :alice :ignores _:s. }. >> >> entails >> >> :alice :ignores :charlie. >> >> -- https://josd.github.io<https://josd.github.io/> <https://josd.github.io/><https://josd.github.io/> >> >> >> On Thu, Nov 25, 2021 at 12:39 PM Pierre-Antoine Champin >> <pierre-antoine.champin@ercim.eu ><mailto:pierre-antoine.champin@ercim.eu>> <mailto:pierre-antoine.champin@ercim.eu><mailto:pierre-antoine.champin@ercim.eu>> wrote: >> >> Hi all, >> >> I have a new proposal (now in a more readable format). >> >> https://pad.lamyne.org/xZF7gcnxTLSNKdueLBYv2A >> <https://pad.lamyne.org/xZF7gcnxTLSNKdueLBYv2A><https://pad.lamyne.org/xZF7gcnxTLSNKdueLBYv2A> >> >> Note that I haven't checked it in depth yet. And that I haven't >> found a satisfying way to model the semantics of log:notIncludes >> yet :-/ >> >> best >> >
<OpenPGP_0x9D1EDAEEEF98D438.asc>