From: <herman.ter.horst@philips.com>

Date: Tue, 30 Sep 2003 17:52:55 +0200

To: pat hayes <phayes@ihmc.us>, www-rdf-comments@w3.org

Message-ID: <OFCE6A893D.31EB5C23-ONC1256DB1.004B8E2E-C1256DB1.005755D2@diamond.philips.com>

Date: Tue, 30 Sep 2003 17:52:55 +0200

To: pat hayes <phayes@ihmc.us>, www-rdf-comments@w3.org

Message-ID: <OFCE6A893D.31EB5C23-ONC1256DB1.004B8E2E-C1256DB1.005755D2@diamond.philips.com>

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 ResearchReceived on Tuesday, 30 September 2003 11:54:00 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Friday, 21 September 2012 14:16:32 GMT
*