From: pat hayes <phayes@ai.uwf.edu>

Date: Wed, 26 Feb 2003 17:42:04 -0600

Message-Id: <p05111b08ba82f882756a@[10.0.100.86]>

To: herman.ter.horst@philips.com

Cc: www-rdf-comments@w3.org

Date: Wed, 26 Feb 2003 17:42:04 -0600

Message-Id: <p05111b08ba82f882756a@[10.0.100.86]>

To: herman.ter.horst@philips.com

Cc: www-rdf-comments@w3.org

>Pat, > >Thank you for your comments. > >>>RDF Semantics document, >>>last call version, 23 january 2003 >>>This comment was mailed earlier to the WebOnt WG [1]. >> >>For the record, the editor accepts this as an editorial comment. >> >>>The definition of subinterpretation I << J in Appendix B >>>is not clear, as >>>it is not clear what a "projection mapping from IR into JR, >>>IS into JS, IL into JL and IEXT into JEXT" is. >>>IR and JR are sets, so the first part is clear: a function >>>from IR into JR. However, IS and JS are functions. >>>(What is meant by a mapping from a function to a function?) >> >>The concept is a familiar one in mathematics: it is often referred to >>as a morphism between functional categories. > >I am familiar with category theory and with how morphisms >between [objects in] functional categories are typically defined. I thought you were. >Because the details of this can vary and were not completely >determined by what you wrote, I made my comment. >For the description of the definition I gave below I was >inspired by examples from category theory. >In fact, this definition can be interpreted as making a category out >of the interpretations of an RDF graph. Right, and I know that many professionals like to use category theory as a framework for such proofs. I guess it seemed a little too abstract and 'heavy' for this expository purpose, however; and in any case I find it rather ugly, myself. > >> >>But the wording of the proofs of lemmas will be clarified and this >>definition made more explicit. >> >>>It seems that the following definition suits the intended >>>use in the Herbrand lemma: >>> >>>I is a subinterpretation of J, I << J, when there is a projection >>>mapping f : IR -> JR such that the following hold: >>>- f(IP) subsetof JP [this is needed for the last condition] >>>- for each v in V, JS(v)=f(IS(v)) >>>- for each typed literal l, JL(l)=f(IL(l)) >>>- for each p in IP, >>>{ <f(x),f(y)> : <x,y> in IEXT((I(p)) } subsetof JEXT(f(p)) >>> >>>Then, automatically, the property that is desired in the text >>>follows: any triple is true in J if it is true in I. >> >>Yes, quite, that is the intent of the current phrasing, stated in a >>lengthier form. An aside, but I know that what I do, when I come across definitions like this, is a kind of global recognition process: Aha, he's defining a standard substructure projection mapping. I then immediately forget about the details and the exact terminology, since they are almost always irrelevant, and just remember what 'subinterpretation' *means*. I know that many students have trouble by getting 'lost' in the details of such definitions, and have to be taught to take a longer-range view of the overall proof in such cases; and good textbooks give this overview as a kind of running commentary. I was trying to imitate this style somewhat here. The exact definition of 'subinterpretation', and being careful about the projection mapping, is really not that important. The document is never going to refer to this projection mapping again: what matters is that one gets the point of what that 'sub' prefix means, ie 'just like, but with some parts missing or incomplete'. Given a proof sketch, a competent professional, like yourself, knows what is meant and can fill in the formal details themselves if they feel inclined (as you did, right?). A newbie, particularly one to whom the techniques are unfamiliar, is more likely to benefit from seeing the general structure of the argument and getting a 'feel' for the proof techniques, it seems to me, rather than by seeing proofs written out with great formal precision and detail. > > >>There is an editorial issue generally in writing such things as this >>appendix. In many people's view, a document like this should not even >>have things like lemmas and proofs in it *anywhere*. To anyone >>trained in formal logic these results and the proof techniques are >>all elementary in any case. On balance, therefore, it seemed > >appropriate to give an expository outline of the basic proof >>techniques as an informative guide for some readers as well as >>providing others (such as yourself, Herman) with the opportunity to >>check the reasoning. However, to write out these proofs too formally >>and in too much detail does not seem appropriate, as this would make >>them unreadable by the novice and boring to the initiated. >> >>I will try to make the wording clearer, however, in the light of your >comments. > >You integrate in one sentence two statements >(too formally / too much detail) about two >kinds of reader here (novice / initiated). >It seems that the novice is helped by detail. Yes and no. I think the reader is most helped by a useful overview and enough details to enable them to fill in the rest. A fully detailed proof of the rdfs closure lemma would run to many pages and I bet almost nobody would ever read it. Even journals of record, outside mathematics, tend to deprecate long, tedious, detailed proofs (eg the AIJ has a published editorial policy to this effect.) >It should not be too formal for the novice. For example, I agree that >mentioning categories, as we just discussed above, in this document would >not be appropriate: in this case more details should be spelled out. >Having this material in the document may help people who are not >formal logicians to become convinced to use RDF in projects. >After all, the normative definition of entailment is highly >theoretical, and this appendix supports a more practical, >triple-based characterization of entailment. Right, that's why I did it. But I bet that not many practical readers will want to read the proofs. The proof itself is no guarantee that the result is correct, by the way: proofs can have bugs in them :-) >As to the initiated, I would like to make the following comment. >In spite of the fact that elementary, well-known techniques are >involved in the proofs, and in spite of the fact that the field of >logic has successfully investigated much more complicated situations, >it seems that the entailment results in this appendix do not all >follow directly from existing results in the field of logic. >Correct me if I'm wrong. Not *directly*, no, because the RDF syntax is rather more forgiving than most standard FO presentations. But the proofs are really very minor adaptations of standard results. All these completeness results work in the same basic way, as I expect you know. If you know the Herbrand technique for FOL you could invent this stuff as you go along. (I did!) BTW, they do follow from standard results if one uses a suitably ugly embedding of RDF into FOL, eg the 'axiomatic semantics' style used in the DAML axiomatization which Richard Fikes and Deb McGuinness wrote. But I think it is actually easier to prove the results directly than to use such a ghastly and unreadable mapping, myself. > Even if all these results would follow >directly from existing results in logic, there is value in >collecting stand-alone proofs such as described in the document. >However, it seems that some new territory is involved, and >there is definitely some degree of complexity, and therefore proofs >have to be provided *somewhere*. Right, which is why I felt an odd compulsion to write the damn things out, even though many people felt that they weren't appropriate in a document of this kind, ie a formal specification document. But then you reap what you sow, or something like that. Sigh. 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@ai.uwf.edu http://www.coginst.uwf.edu/~phayes s.pam@ai.uwf.edu for spamReceived on Wednesday, 26 February 2003 18:42:09 GMT

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