RDF Semantics: partial review

Here are review comments of the RDF Semantics document,
versions of 5 September (first part) and 
26 September (appendix).

I reviewed Sections 0, 1, 2, and Appendix A up to
and including the compactness lemma, but without
the text (and table) about simple entailment rules -
this latter text links to Section 7.1 which I also
didn't yet review.

Section 0.3

"An instance is proper just when the instance
mapping is invertible."
This does not seem to be consistent with the definition 
of proper instance.  For example, a mapping that maps
only a blank node to a URI reference defines
a proper instance, while it is also invertible.

==

It seems that the definition of merge of RDF graphs
does not adequately formalize the intended notion.
Consider the following example,
writing ~ for RDF graph equivalence:
Let S = { E1, E2, F} where  E1~E2  and  not(E1~F).
Let E~E1, F~F1' and F~F2' and suppose that E1, F1', F2'
doe not share blank nodes.
Then, according to the definition in Section 0.3,
the simple union of E1, F1', F2' counts as a merge of S:
namely the set S'={E1, F1', F2'} is in 1:1 correspondence
with S, and each element of S' is equivalent to an 
element of S.
This is contrary to what I expect to be the intention
behind this definition.

Here is a suggestion for an alternative definition:
Given a set S of graphs, a merge of S is a graph that
is obtained by replacing the graphs G in S by equivalent
graphs G' that do not share blank nodes, and by taking
the union of these graphs G'.
Note that I do not speak of "the" merge of a graph.
It might be added that, as not difficult to see,
the merge of a set of graphs is uniquely defined up 
to equivalence.
Briefly, a merge of S might be viewed as a "blank node
disjoint union of S".
 
==

"A name is from a vocabulary if ..."
I hope that this can be simplified.
First, this is a forward reference:
the notion of vocabulary is defined (a few lines) later.
Second, a vocabulary is defined as a set of names.
So this smells like a circularity.
I think that it would be in the interest of the clarity of
the document if this redefinition of the word "from"
could be removed from the document.

==

Section 1.4

the table: Semantic conditions for ground graphs

line 3 needs to add [what I add between brackets]:
- if E is a typed literal [in V] then ..
line 4 needs to add: 
- if E is aURI reference [in V] then ..
It would be better if line 5 adds
- if E is a [ground] triple
(just like this is done in line 6 for graphs)

As to lines 1 and 2 of these tables: I believe
that clarification would be helpful.
line 1 says: if E is a plain literal "aaa" then I(E)=aaa.
String quotes are removed from "aaa", but it seems that I(E) is a 
string.  What is the definition here?
Anyway, with the definition of Herbrand interpretation later
in the document it seems that plain literals are mapped
into themselves, just like typed literals.
This suggests that a plain literal *in an RDF graph* is
already viewed as a string or a pair consisting of a
string and a language tag.

==

Section 1.5

the table: Semantic conditions for blank nodes

It seems that line 1 would need to be replaced by
something like the following more complete statement:
-  If A is a mapping defined on the blank node E, then
   I+A(E)=A(E).

Note: for completeness, the line directly following this
table seems to need to add LV as well.

==

Appendix A

I consider the text from the sentence: "In the following proofs
and discussion it is convenient ..." up to and including
the proof of the Subinterpretation lemma to be very complicated
and confusing.
It does not seem necessary to add all these extra layers:
extended vocabulary, interpretation of extended vocabulary, I.k.
Moreover, the discussion does not seem to be complete:
what is IP and LV of the extension J of I?

We discussed subinterpretations earlier in the context
of the last call version of the document.
I have to say that I am not satisfied by the current text.

The subinterpretation lemma forms a crucial step toward
the interpolation lemma.  I became convinced of the truth
of the interpolation lemma by constructing the following
version of subinterpretations and the subinterpretation
lemma proof, which use only the definitions concerning
I and I+A in Sections 1.4 and 1.5:

An interpretation I is a subinterpretation of J, I<<J,
if VI subsetof VJ, LVI subsetof LVJ, and if there is a
mapping k (called a projection mapping) from
IRI union IPI  to  IRJ union IPJ  satisfying the following
conditions:
- k(IRI) subsetof IRI
- k(IPI) subsetof IPJ
- k maps strings and pairs consisting of a string and a 
language tag to themselves
- k x k ( IEI(a) ) subsetof IEJ(k(a)) for each a in IPI
- ISJ(v) = k(ISI(u)) for each v in VI intersect U
- ILJ(v) = k(ILI(v)) for each v in VI intersect Lt
Here U is the set of URI references and Lt is the set 
of typed literals.

Subinterpretation lemma: 
If I << J and I satisfies E then J satisfies E.
Proof:
Choose A : blank(E) -> IRI such that I+A satisfies E.
Let spo in E.  Then <I+A(s),I+A(o)> in IEI(I(p))
so that <k(I+A(s)),k(I+A(o))> in IEJ(k(I(p)).
Define A' : blank(E) -> IRJ to be A' = k o A
(composition).  Then <J+A'(s),J+A'(o)> in IEJ(J(p)),
concluding the proof.

(Note that all bits from this definition of I<<J are
actually used in this proof.)

==

(We mentioned this already in our earlier discussion:
It might be noted, although not in the RDF Semantics 
document, that projection mappings defined in this way 
make a category of the class of all simple interpretations.)
 
==

In connection with the preceding remark, the proof of the
Herbrand lemma could also be adapted to this definition
of I<<J.

==

Definition of Herbrand interpretation:
all these lemmas concerning simple entailment do not
involve XML literals explicitly, as these enter the
semantic definitions only in Section 3.
This text devoted to the proof of the interpolation
lemma should therefore ideally at this point not be 
mixed with complications due to XML literals, in my view.

==

Anonymity lemma: I cannot follow the proof.
More precisely, why is the first of the two sentences
("Since ...") true?

==

Section 0.1

It seems that the reference to "sections 1 and 3.1" needs
to be replaced by a reference to sections 2 and 3.1.

Section 1.1

typo: heirarchy


==

Herman ter Horst
Philips Research

Received on Tuesday, 30 September 2003 11:54:00 UTC