Re: N3 semantics new-new proposal

On 29/11/2021 18:58, Doerthe Arndt wrote:
> 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))
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.


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.


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

> (...) 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... :-/

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

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!

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.

   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>>: >> >> >> >> ----- Weitergeleitete 
Nachricht ----- *Von:* Jos De Roo >> <josderoo@gmail.com 
<mailto:josderoo@gmail.com>> *An:* >> Pierre-Antoine Champin 
<pierre-antoine.champin@ercim.eu >> 
<mailto:pierre-antoine.champin@ercim.eu>> *CC:* >> public-n3-dev@w3.org 
<mailto:public-n3-dev@w3.org> >> <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/> >> >> >> On Thu, 
Nov 25, 2021 at 12:39 PM Pierre-Antoine Champin >> 
<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> >> >> 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 >> >