Check if the interpolation lemma is still true given the new semantics

[franconi]

Check if the interpolation lemma is still true given the new semantics: we believe it is true, but it is better to double check.

[franconi]

We can adapt the detailed proof of the interpolation lemma as found in:
Jean-François Baget. RDF Entailment as a Graph Homomorphism. Proc. 4th international semantic
web conference (ISWC), Nov 2005, Galway, Ireland. pp.82-96
https://inria.hal.science/hal-00922476/document

[pfps]

This should be resolved before CR.

Depends on w3c/rdf-concepts#220, w3c/rdf-star-wg#169, w3c/rdf-star-wg#128, and #144.

[franconi]

This is my first attempt at adapting Pat's proof to RDF 1.2.
I used the compact formalisation of RDF 1.2 Semantics from RDF-star-liberal-baseline.

Subgraph Lemma.
A graph S entails each of its its subgraphs E.

Proof: from the semantic condition
[I+A](g) = TRUE if and only if ∀ t ∈ g . I+A = TRUE

Instance Lemma.
Each instance S of a graph E entails E.

Proof: from the semantic condition
A simple interpretation I is a model of a graph g
if and only if ∃ A . I+A = TRUE.

Herbrand Lemma.
The Herbrand interpretation of a graph G is a model of G.

Proof:
Given a nonempty graph G, the (simple) Herbrand interpretation of G, written Herb(G), is the interpretation defined as follows.

• IRHerb(G) = the set of all names and blank nodes which appear in a subject or object position in a triple in G;

• IPHerb(G) = the set of URI references which appear in the property position of a triple in G;

• IEXTHerb(G)(p) = {<s,o>: G contains a triple s p o . }

• ITHerb(G)(s,p,o) = {concat(s,p,o) : G contains a triple term s p o}

• ISHerb(G) and ILHerb(G) are both identity mappings on the appropriate parts of the vocabulary of G.

Clearly Herb(G)+B, where B is the identity map on blank nodes in G, satisfies every triple in G, by construction, so Herb(G) satisfies G.

Interpolation Lemma.
S entails E if and only if a subgraph of S is an instance of E.

Proof:
'if' follows from the subgraph and instance lemmas.
'only if' uses the Herbrand construction.
Suppose S simply entails E.
Herb(S) satisfies S, so Herb(S) satisfies E, i.e. for some mapping A from the blank nodes of E to IRHerb(S), [Herb(S)+A] satisfies every triple s p o . in E, so S must contain the triple Herb(E)+A p Herb(E)+A . which is the instance of the previous triple under the instance mapping A. So the set of all such triples is a subgraph of S which is an instance of E.

[doerthe]

I did not spend much time with the proofs (yet), but they look good. Some remarks below:

This is my first attempt at adapting Pat's proof to RDF 1.2. I used the compact formalisation of RDF 1.2 Semantics from RDF-star-liberal-baseline.

Subgraph Lemma. A graph S entails each of its its subgraphs E.

Proof: from the semantic condition I+A = TRUE if and only if ∀ t ∈ g . I+A = TRUE

Instance Lemma. Each instance S of a graph E entails E.

Proof: from the semantic condition A simple interpretation I is a model of a graph g if and only if ∃ A . I+A = TRUE.

Herbrand Lemma. The Herbrand interpretation of a graph G is a model of G.

Proof: Given a nonempty graph G, the (simple) Herbrand interpretation of G, written Herb(G), is the interpretation defined as follows.

• IRHerb(G) = the set of all names and blank nodes which appear in a subject or object position in a triple in G;
• IPHerb(G) = the set of URI references which appear in the property position of a triple in G;
• IEXTHerb(G)(p) = {<s,o>: G contains a triple s p o . }
• ITHerb(G)(s,p,o) = {concat(s,p,o) : G contains a triple term s p o}
• ISHerb(G) and ILHerb(G) are both identity mappings on the appropriate parts of the vocabulary of G.

Clearly Herb(G)+B, where B is the identity map on blank nodes in G, satisfies every triple in G, by construction, so Herb(G) satisfies G.

IRHerb needs to also include the codomain of ITHerb:

• IRHerb(G) = the set of all names, blank nodes and graph terms which appear in a subject or object position in a triple in G;

I would then not use the concatenation because in some weird cases that could produce something already present in the graph, so what about just using the identity as well?

• ITHerb(G)(s,p,o) = { <s, p, o> : G contains a triple term <s, p, o>}
  (or we simply say that ITHerb(G) is the identity)

Another (minor) comment: blank node do not necessarily have names

[doerthe]

I just thought about it:
IRHerb(G) needs to contain ALL names and blank nodes (or names of blank nodes) which appear in subject and object position of a triple in G AND all concatenations (if we keep concatenations) we can (recursively) form from the elements of IPHerb(G) and IRHern(G). Our Herbrand universe needs to be infinite because of the injectivity of IT.

[franconi]

Our Herbrand universe needs to be infinite because of the injectivity of IT.

Unless we change the semantics with IT partial.

[doerthe]

Thinking about it: Making IT partial or giving up its injectivity are the only options to make the interpolation lemma hold, right?