Relationship between RDF-star and reification

Dear all,

the current semantics uses "hidden predicates" to describe embedded 
triples, so there is no standard way to convey embedded triples to 
legacy RDF systems. I know that this has been a concern for some people.

One of the good properties (in my opinion) of the newly proposed 
semantics [1] is that its relies on the reification vocabulary (plus 
some new predicates), in a way that is not a hurdle to native RDF-star 
implementations, but can be useful to legacy RDF systems. Let me explain:

The new proposal suggests that

     :bob :says << :alice a :Genius >>.

can be loosely described as

     :bob :says [
         rdf:subject :alice;
         rdf:predicate rdf:type;
         rdf:object :Genius;
         rdf:quotedSubject "<http://example.com/ns#alice>";
         rdf:quotedPredicate 
"<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>";
         rdf:quotedObject "<htttp://example.com/ns#Genius>";
     ].

"loosely", because there is no semantic relationship between the two 
graphs -- neither of them entails the other. However, this 
transformation is valuable, because /under certain conditions/ (detailed 
below), it preserves entailment. Meaning that a legacy RDF system can 
"encode" an RDF-star graph as above, then reason on it, and if the 
result can be "decoded" as RDF-star, then it is a valid result in 
RDF-star semantics as well.

The technical details follow for those of you who are interested. But I 
would like to know if this evolution is deemed interesting by other 
members of the group.

   pa

[1] 
https://pr-preview.s3.amazonaws.com/w3c/rdf-star/pull/127.html#rdf-star-semantics


Under wich conditions does this work?
-------------------------------------

It works for RDF-star graphs that do not contain any of the predicates 
used to otherwise describe embedded triples, namely: rdf:subject, 
rdf:predicate, rdf:object; rdf:quotedSubject, rdf:quotedPredicate, 
rdf:quotedObject. We call these graphs "reification-free".

The corresponding RDF graphs therefore only contain the 6 predicates in 
a very controlled way. We call these graphs "reification-correct".

Any reification-free RDF-star graph can be mapped to a 
reification-correct RDF graph, and conversely.

If G and H are reification-free RDF-star graphs, and G' and H' are their 
corresponding reification-correct RDF-graphs, then

     G |= H  iff  G' |= H'

IMPORTANT: the proposed semantics does *not* forbid the use of 
reification predicates in other, uncontrolled, ways. The semantics is 
defined for any RDF-star graph, and that definition also relies on 
standard RDF semantics. But in the general case, it is slightly more 
complex than above

To sum it up: reasoning on unrestricted RDF-star graphs is always 
possible; reasoning on reification-free RDF-star graphs is simpler.


Proof sketch
------------

The proposed semantics [1] defines a mapping unstar(G) = (G1, G2). In 
the following, we will append 1 and 2 to any graph name to denote the 
images of that graph through unnap(). In addition, we define G3 = G1 U 
G2, and G3' = G3 minus all the arcs involving the hidden IRI.

It can be proven, using the interpolation lemma, that if G and H are 
reification free, then

     * G3 |= H3 → G1 |= H1

     * and so  G |= H  iff  G3 |= H3

     * G3 |= H3  iff  G3' |= H3'

     * and so G |= H  iff  G3' |= H3'