- From: pat hayes <phayes@ihmc.us>
- Date: Mon, 29 Sep 2003 20:00:25 -0500
- To: w3c-rdfcore-wg@w3.org
- Cc: Dan Connolly <connolly@w3.org>
There is a version (dated 29 Sept.) with the changes described below at http://www.ihmc.us/users/phayes/RDF_Semantics_LC2.1.html It also has glossary entries for consistent and decideable, with brief comments. I tend to agree with Peter about the rules being normative, particularly as I couldn't find a formal record of that decision either (the best I could do was to link to the IRC log). The only coherent interpretation I can assign to this, on reflection, would be that any other inference engine which worked in some other way would not be conformant, even if it was complete and correct: which is silly. Maybe y'all could just advise me to make section 7 informative rather than normative? I'd suggest that we do that before LC2, in any case. Pat >X-Original-To: www-rdf-comments@frink.w3.org >Delivered-To: www-rdf-comments@frink.w3.org >Delivered-To: www-rdf-comments@w3.org >X-Sender: phayes@mail.coginst.uwf.edu >Date: Mon, 29 Sep 2003 12:17:07 -0500 >To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com> >From: pat hayes <phayes@ihmc.us> >Cc: www-rdf-comments@w3.org >Subject: Re: comments on 26 September version of RDF Semantics document >X-Archived-At: http://www.w3.org/mid/p06001f37bb9e001c903e@%5B10.0.100.25%5D >Resent-From: www-rdf-comments@w3.org >X-Mailing-List: <www-rdf-comments@w3.org> archive/latest/3848 >X-Loop: www-rdf-comments@w3.org >Sender: www-rdf-comments-request@w3.org >Resent-Sender: www-rdf-comments-request@w3.org >List-Id: <www-rdf-comments.w3.org> >List-Help: <http://www.w3.org/Mail/> >List-Unsubscribe: <mailto:www-rdf-comments-request@w3.org?subject=unsubscribe> >Resent-Date: Mon, 29 Sep 2003 13:17:15 -0400 (EDT) > > >> Comments on RDF Semantics (version dated 26 September 2003) >> >> >>I did a quick read of the most of RDF Semantics, along with a careful >>investigation of a couple pieces. > >Thanks. > >> Here are my comments. >> >>1/ The major new issue I have with the document is the unsupported change >>of the entailment rules from informative to normative. > >Just for the record, that change happened a few versions ago; but >your comment is noted. > >> >>2/ The removal of the translation to LBase is a major improvement. I would >>have prefered different wording in Section 0.1 concerning this translation >>but can live with the new situation. >> >>3/ The document is of several minds with respect to just what the semantics >>of RDF (and RDFS) is. There is wording in Section 1.3 to the effect that >>the definition of the semantics of RDF and RDFS excludes the entailment >>rules. How can this coexist with having the entailment rules be normative? > >Well, the rules are not part of the semantics as such. The issue of >their normativeness (normativity? normitude?) seems to be orthogonal >to this point. The Abstract of the document begins > >"This is a specification of a precise semantics, and corresponding >complete systems of inference rules, for...." > >clearly indicating that the semantics is one thing, and the rules >another, a division reflected in the organization of the document. > >(??Maybe I havnt followed your point here??) > >> >>4/ The figures in the copy of the document that I reviewed have naming >>problems, but I am told that these have since been fixed. > >They may not have been fixed to your satisfaction. The changes were >largely graphical (color, font rendering) rather than textual. We >have discussed the issue of the wording in figure 1, and I responded >in an earlier message. > >> >>5/ The Monotonicity and Compactness Lemmas are only stated for simple >>entailment. However, readers could easily be left with the impression that >>the other forms of entailment could also have the desirable properties that >>accrue from these lemmas. > >The text states explicitly: > >"These results apply only to simple entailment, not to the extended >notions of entailment introduced in later sections." > >reiterated after the statement of the anonymity lemma: > >"Note again that this applies only to simple entailment, not to the >vocabulary entailment relationships defined in rest of the >document.". > >Later, when RDF-entailment is introduced (section 3.1, second >paragraph) the document repeats the warning, with a back-link and an >illustrative example.: > >"It is easy to see that the lemmas in <a href>Section 2</a> do not >all apply to rdf-entailment: for example..." > >I think this constitutes an adequate safeguard against this misunderstanding. > >> >>6/ The characterization of simple entailment rules is misleading as they do >>not currently correspond to the instance lemma. The comment on how to make >>this change at the end of Section 7.1 does not adequately serve to correct >>the misimpression. > >Let me suggest a re-wording and expansion of the first line of >section 7.1 as follows. Would this be more acceptable? > >"The interpolation lemma in section 2 characterizes simple >entailment in terms of instances and subgraphs. Being a subgraph >requires no explicit formulation as an inference rule on triples, >but one can give rules which generate generalizations, for example: " > >>7/ The document needs a better description of consistency and >>inconsistency. > >Can you elaborate? Ah, I see that there is no glossary entry for >'consistent'; I will rectify this. > >> >>8/ The change to the RDFS entailment lemma is incorrectly noted in the >>change log as editorial. > >It was considered editorial because it was considered to be a >correction of an error in the text rather than a change to the lemma. > >>9/ I view the development and statement of the entailment lemmas as >>fundamentally flawed. I look for soundness and completeness in any such >>syntactic characterization of entailment. Neither simple entailment, RDF >>entailment, nor RDFS entailment have both these characteristics. > >In the sense of 'complete' you probably mean, that is correct. They >never have been written in that style and I see no useful purpose to >be served by so doing. > >>9a/ Section 7.1 does not provide any statement at all on whether the simple >>entailment rules are complete with respect to simple entailment. > >Section 2 has already noted, however : > >"The interpolation lemma completely characterizes simple RDF >entailment in syntactic terms. To tell whether a set of RDF graphs >entails another, check that there is some instance of the entailed >graph which is a subset of the merge of the original set of graphs. >Of course, there is no need to actually construct the merge. If >working backwards from the consequent E, an efficient technique ..." > >followed by a paragraph of discussion. The amended text (above) at >the beginning of section 7.1 will refer back to this. > >I also note that section 7 begins by saying : > >"The following tables list some inference patterns which capture >some of the various forms of vocabulary entailment." > >and does not refer to simple entailment. As you may recall, the >inference rules in section 7.1 were introduced in order to ensure >that the RDF and RDFS closures included appropriate generalizations >of some of the entailed triples. > >>There is >>a statement that the rules are sound, and that an agumentation of them >>correspond to the instance lemma, but no proof is presented. > >That is true; however, I do not think that a proof is needed, as the >relevant syntactic condition is fully described by the interpolation >lemma. > >To provide a complete set of rules which implement the relevant >search as a forward application of valid entailment rules would be >computationally ridiculous. Since the main purpose of describing >entailment rules in this document is not as an exercise in textbook >formal logic, but rather to provide a useful guide to suggest >relatively easy implementation styles for inference engines, to >adopt the style you are here suggesting in the main body of the >document would in my view serve no useful purpose and would likely >be counterproductive. > >However, I plan to insert the following in the proof appendix (just >after the QED of the interpolation lemma) , with a forward link from >section 7.1 (end), which may go some way towards satisfying your >point. (This change has not yet been discussed by the WG. ) > >--------- >This lemma can be used as the basis for several different mechanical >processes for checking simple entailment. One way to characterize >entailment syntactically is in terms of inference rules which apply >to a set S and can be used to derive E just when S entails E. For >example, a slight modification of the simple entailment rules >described in section 7.1 will suffice, where we allow new blank >nodes to be allocated to existing blank nodes as well as to URI >references and literals: > >extended simple entailment rules. >---------<table>------ >Rule name > >If E contains > >then add > >xse1 > >uuu aaa xxx . > >uuu aaa _:nnn . > >where _:nnn is a blank node identifier allocated to xxx by rule xse1 or xse2. > >xse2 > >uuu aaa xxx . > >_:nnn aaa xxx . > >where _:nnn is a blank node identifier allocated to uuu by rule xse1 or xse2. >----------</table>-------- >These rules allow blank nodes to proliferate, producing highly >non-lean graphs; they sanction entailments such as > >ex:a exp ex:b . >ex:a ex:p _:x . by xse1 with _:x allocated to ex:b >ex:a ex:p _:y . by xse1 with _:y allocated to _:x >_:z ex:p _:y . by xse2 with _:z allocated to ex:a >_:u ex:p _:y . by xse2 with _:u allocated to _:z >_:u ex:p _:v . by xse1 with _:v allocated to _:y > >It is easy to see that if S is an instance of T then one can derive >T from S by applying these rules in a suitable sequence; the rule >applications required can be discovered by examination of the >instance mapping. So, by the interpolation lemma, S entails E iff >one can derive (a graph containing) E from S by the application of >these rules. However, it is also clear that applying these rules >naively would not result in an efficient search process, since the >rules will not terminate and can produce arbitrarily many redundant >derivations of equivalent triples. > >The general problem of determining simple entailment between >arbitrary RDF graphs is decideable but NP-complete. This can be >shown by encoding the problem of detecting a subgraph of an >arbitrary directed graph as an RDF entailment, using blank nodes to >represent the graph (observation due to Jeremy Carroll.) >----------- > >> >>SUGGESTION: I suggest that Section 7.1 be augmented with the following >>Lemma and that its proof be added to Appendix A. >> >> Simple entailment lemma. S simple-entails E iff there is a graph >> that can be derived from S by the application of the simple >> entailment rules that is a supergraph of E. (Proof in Appendix A.) >>This lemma requires that the simple entailment rules be augmented to allow >>vvv in rule se1 and bbb in rule se2 to be a blank node. > >See above. > >> >>9b/ Section 7.2 does not provide an adequate syntactic characterization of >>RDF entailment. >> >>SUGGESTION: I suggest that Section 7.2 be augmented by the following >>change to the RDF entailment lemma and that its proof in Appendix A be >>modified accordingly. >> >> RDF entailment lemma. S rdf-entails E if and only if ... and which >> is a supergraph of E. (Proof in Appendix A.) >> >> >>9c/ Section 7.3 does not provide an adequate syntactic characterization of >>RDF entailment. >> >>SUGGESTION: I suggest that Section 7.3 be augmented by adding the >>following lemma and providing a proof for it in Appendix A. >> >> RDFS consistency lemma. S is rdfs-consistent if and only if it is >> not possible to derive a supergraph of a graph of the following >> form from S plus the RDF and RDFS axiomatic triples by the >> application of the simple, RDF, and RDFS entailment rules >> >> uuu vvv rrr^^rdfs:XMLLiteral . >> vvv rdfs:range www . >> www rdfs:subClassOf rdfs:Literal . >> >> where rrr is a non-well formed XML literal. (Proof in Appendix A.) >> >>I believe that this is a correct characterization of RDFS consistency but >>this would have to be shown in the proof. >> >>SUGGESTION: I suggest that Section 7.3 be augmented by the following >>change to the RDFS entailment lemma and that its proof in Appendix A be >>modified accordingly. >> >> RDFS entailment lemma. If S is rdfs-consistent then S rdfs-entails >> E if and only if ... and which is a supergraph of E. (Proof in >> Appendix A.) > >Thanks for your suggestions. > >Pat -- --------------------------------------------------------------------- IHMC (850)434 8903 or (650)494 3973 home 40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32501 (850)291 0667 cell phayes@ihmc.us http://www.ihmc.us/users/phayes
Received on Monday, 29 September 2003 21:00:30 UTC