Semantics of cited formulas

[doerthe]

Related to: #1

We need to agree how to interpret cited graphs like for example

:x :says {:s :p :o}.

I think this topic is quite challenging (for TriG, for example, there was no agreement https://www.w3.org/TR/rdf11-datasets/). RDF* [4] reduces such constructs to rdf reification which unfortunately doesn't solve the problem of defining a semantics since reification is excluded in rdf semantics (see: https://www.w3.org/TR/rdf11-mt/#reification). There are many different approaches we could follow like for example KIF [5], Common Logic [6] or also make it more complex like they do in SUMO [7].

[4] O. Hartig, B. Thompson, Foundations of an alternative approach to reification in RDF, CoRR abs/1406.3399. arXiv:1406.3399. URL http://arxiv.org/abs/1406.3399

[5] P. Hayes, C. Menzel, A semantics for the knowledge interchange format, in: IJCAI 2001 Workshop on the IEEE Standard Upper Ontology, Vol. 1, 2001, p. 145.

[6] ISO/IEC 24707:2007 Information technology – Common Logic (CL), standards.iso.org/ittf/PubliclyAvailableStandards/c039175_ISO_IEC_24707_2007%28E%29.zip (2007).

[7] C. Benzmüller, A. Pease, Higher-order aspects and context in sumo, Web Semantics: Science, Services and Agents on the World Wide Web 12 (2012) 104–117.

[william-vw]

Yeah, it looks like the W3C Working Group on RDF dataset semantics discussed for about half a year and never reached a consensus .. One could be pessimistic and say there is a small chance that we'd be able to reach consensus in the year that we took out for N3 standardization.

On the other hand, we're only debating their interpretation for N3 in particular and not RDF in general. Indeed, it seems that a major issue the WG faced was that very different assumptions existed among [RDF] practitioners and choosing one or another of the propositions before would have gone against some deployed [RDF] implementations.

In light of this, it wouldn't be a bad idea to ask people who are acquainted with how existing N3 implementations deal with embedded formulas, and/or how they would prefer the N3 standard to deal with them.

Personally my preference would go towards having each named graph define its own context - but I feel that any solution must take care not to put a huge burden on N3 implementations (e.g. avoiding the possibility for complex nestings of formulas as discussed by Benzmüller).

[doerthe]

Just to add something to the discussion here: The TPLP paper about N3 claims that nested formulas are not “referentially transparent”. This means that even if two terms in a cited formula denote the same object in the domain of discourse two cited formulas which only differ in the use of these two terms should be considered as different.

As a concrete example consider the following:

:LoisLane :believes {:Superman :can :fly.}.

Even if we know that the term :Superman denotes the same object as :ClarkKent, this knowledge combined with the above formula should not imply the following formula:

:LoisLane :believes {:ClarkKent :can :fly.}.

In the concrete example :LoisLane might not know that :ClarkKent denotes the same resource as Superman.

The problem is known as the "superman problem" and was discussed in many contexts.

Direct question: Do we agree on that?

I do, but would like to hear opinions.

[doerthe]

As a result of the discussion we had in our last meeting (1.7.2019) I would like to add that I see some advantages in keeping the above "lack of referential transparency": I think it is a rather weak semantics in the sense that there are not many direct conclusions which can be drawn from simple cited formula. This "weakness" is in my opinion an advantage: If N3 assumes as little as possible, everyone who wants to have some more meaning and implications can have rules to support such stronger semantics.

For the superman-example above, we can for example add:

:LoisLane :believes {:Superman :can :fly.}.

:Superman owl:sameAs :ClarkKent.


{
:LoisLane :believes {?s1 ?p1 ?o1}.
?s1 owl:sameAs ?s2.
}
=>
{
:LoisLane :believes {?s2 ?p1 ?o1}.
}.

and get that:

:LoisLane :believes {:ClarkKent :can :fly}.

Of course this is a very basic example and we would have to look deeper into that matter to know which kinds of derivations are possible,

[doerthe]

In the above context, we also discussed in our last meeting (1.7.2019) how the scope of blank nodes in cited formulas should be. As we already had this discussion in another tread (see #5), I try to keep it short here.

Does:

:LoisLane :believes {_:x :can :fly.}.

Mean:

a) ∃x: believes (LoisLane, can(x,fly))
"There exists someone from which whom LoisLane believes that he or she can fly"

or

b) believes (LoisLane, (∃x: can(x,fly)))
"There LoisLane believes that there exists someone who can fly"

The N3 specification says that b is correct. We discussed the arguments for both sides:

It seems that TriG also follows this approach for named graphs, see here.

But: in the lists of possible semantics there are also counter examples. Without a proper semantics, we cannot really say anything here.

In this context we also discussed that one problem with the global scope of cited formulas is, that if such cited formulas refer to existing graphs in the Web, think for example in something like

<concreteGraphUri> :containsTriples {:a :b :c. _:x :p :o}.

the scope of _:x is local.

As a solution it was proposed to simply not allow such cases and say that we can only use blank nodes to name graphs.

This is in my opinion no solution (not here, but also not for named graphs), because such a blank node can still refer to a concrete graph (remember that blank nodes are simply existentially quantified variables) and I think in many cases this is also what we want.

By assuming the quantifier of the cited formula on top level, we loose the expressivity to even state that a triple containing a blank node is in a formula. More concrete, let's assume that we have a :graph1 which contains the triple

_:x a :Unicorn.
"Unicorns exist."

If we assume all existential variables to be quantified on top level, there is no way to express in N3 that :graph1 stated that unicorns exist. If we write:

:graph1 :states {_:x a :Unicorn.}.

that statement means (assuming quantification on top level):
"There exists something, about which graph 1 states that this is a unicorn."

this is a totally different statement then we wanted to make.

A last argument I would like to add here in favor of interpretation b is that it would be easier for rules. I could be wrong, but I think that users would expect that a rule having a blank node in the antecedence can actually be applied. Consider the following example:

We have a triple:
:bob a :Unicorn.

And a rule:

{_:x a :Unicorn.} => {:world a :MagicPlace}.

Following interpretation a, this rule means

∃x: (type(x, Unicorn) → type (world, MagicPlace)

"There exists something and if this something is a unicorn, then the world is a magic place."

With this rule we can not draw any conclusion from our triple.

But, if we assume local scoping, namely interpretation b, than we have here:

(∃x: type(x, Unicorn) → type (world, MagicPlace)

"If unicorns exist, then the world is a magic place"

With this interpretation, we could derive the triple:

:world a :MagicPlace

and at least I think that is also what the users of N3 will expect (but here I am also asking you).

So, my "short" summary is not short at all, sorry for that. I am still interested in your opinions.

[william-vw]

@doerthe I'm having trouble getting the desired results for your example in Cwm:

@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <#>.

:LoisLane :believes {:Superman :can :fly.}.
:Superman owl:sameAs :ClarkKent.

{ :LoisLane :believes {?s1 :can ?o1}. ?s1 owl:sameAs ?s2. }
=>
{ :LoisLane :believes {?s2 :can ?o1}. }.

In Eye it indeed infers that
:LoisLane :believes {:ClarkKent :can :fly}.

But, note that this is no longer inferred when replacing :can by ?p1.

[william-vw]

Your explanation re scoping of blank nodes makes sense to me, personally.

Just to be sure, how can one refer in N3 to a previously cited formula - I believe @gkellogg mentioned the use of owl:sameAs:

{ :Superman :can :Fly. } owl:sameAs :supflies.
:LoisLane :believes :supflies.

[doerthe]

@doerthe I'm having trouble getting the desired results for your example in Cwm:

@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <#>.

:LoisLane :believes {:Superman :can :fly.}.
:Superman owl:sameAs :ClarkKent.

{ :LoisLane :believes {?s1 :can ?o1}. ?s1 owl:sameAs ?s2. }
=>
{ :LoisLane :believes {?s2 :can ?o1}. }.

In Eye it indeed infers that
:LoisLane :believes {:ClarkKent :can :fly}.

But, note that this is no longer inferred when replacing :can by ?p1.

Yes, for technical reasons you need to add an extra triple for EYE (which I omitted, since that is EYE specific ;) ). So, to make your example run in EYE, try:

:LoisLane :believes {:Superman :can :fly.}.

:Superman owl:sameAs :ClarkKent.


{
:LoisLane :believes ?something.
?something log:equalTo {?s1 ?p1 ?o1}.
?s1 owl:sameAs ?s2.
}
=>
{
:LoisLane :believes {?s2 ?p1 ?o1}.
}.

then you will get your desired result.

[doerthe]

Your explanation re scoping of blank nodes makes sense to me, personally.

Just to be sure, how can one refer in N3 to a previously cited formula - I believe @gkellogg mentioned the use of owl:sameAs:

{ :Superman :can :Fly. } owl:sameAs :supflies.
:LoisLane :believes :supflies.

Why do you want a URI if you could also use the formula itself?

But given that you just want it: you can use owl:sameAs if you want. I, personally don't like that notion too much since I am not sure whether a cited formula is an owl:Thing. OK, the idea is that everything is an owl:Thing, but then owl itself does not support such constructs....

I would like to fix the semantics such that by using owl:sameAs here, you can be really sure that :supflies is a graph consisting of one single triple, namely :Superman :can :fly.. This is how I read the specification of N3 but this differs from some of the definitions for the meanings of named graphs.

By letting the graph itself be part of the logic (can be used in a triple, is a resource) and following this definition, we can also enable the other (have to check whether all) meanings, you can for example simply state:

{:Superman :can :fly.} :isPartOf :supesuperflies.

if you want to say that your cited formula is only one part of a bigger graph.

[william-vw]

@doerthe Thanks, it's working in Eye now (not sure why that extra triple is needed ..) but still not in Cwm.

[william-vw]

@doerthe I think we've landed on a default semantics, which could possibly be overruled by adding some rules (as discussed at the top of this issue page, and in our RuleML paper :-) So would it be acceptable to close this issue? ..

[TallTed]

One thing that's missing from all this (not meant to reopen this issue, but relevant anywhere inference is brought up) is:

Who is allowed to see the data that claims :Superman owl:sameAs :ClarkKent.?

It's a fairly short list. :Superman, :ClarkKent, :KalEl, :JimmyOlsen, :Batman, and :BruceWayne. I think :WonderWoman and :DianaPrince, too.

There are certainly some others, but the point here is that :LoisLane isn't on the list (except in some particular timeframes in some particular universes within the multiverse).

As I've raised in other contexts -- it's important for members of the Rebel Alliance to be able to expose that to other members, but not to members of the Empire Stormtroopers -- and possibly vice versa, presuming that the Empire figures out that plainclothes/undercover detective work is of value.

Just because a triple (statement) is uttered or asserted somewhere, even if there's only one place for such utterances, doesn't mean that the statement should be visible to all.