Re: RDF Semantics: subinterpretations

>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 spam

Received on Wednesday, 26 February 2003 18:42:09 UTC