W3C home > Mailing lists > Public > w3c-rdfcore-wg@w3.org > September 2003

Fwd: Re: comments on 26 September version of RDF Semantics document

From: pat hayes <phayes@ihmc.us>
Date: Mon, 29 Sep 2003 20:00:25 -0500
Message-Id: <p06001f3abb9e30eda159@[10.0.100.25]>
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 EDT

This archive was generated by hypermail pre-2.1.9 : Monday, 29 September 2003 21:00:35 EDT