Re: RDF Semantics: partial review

>Here are review comments of the RDF Semantics document,
>versions of 5 September (first part) and
>26 September (appendix).

Hi Herman, thanks for the input.

For a version with the corrections made, as noted below, look at

http://www.ihmc.us/users/phayes/RDF_Semantics_LC2.1.html

dated 30 September.

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

Good point. I have deleted the sentence. (I am not sure what was in 
my mind when I wrote that...)

>
>==
>
>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.

Indeed. I  have rephrased the definition along the lines you suggest below.

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

I am not sure how to make it any simpler than it is.

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

It would be (harmlessly) circular if it were not for the part of the 
definition which mentions typed literals. For example,

"23"^^xsd:integer
is from
{xsd:integer}.

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

I need some word to use. Can you suggest an alternative?

>
>==
>
>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 ..

Actually that should be 'from V'. So added.

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

Done.

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

The tables are all stated using the N-triples conventions. In this, 
literal character strings are enclosed inside double quote marks. So 
aaa here indicates the character string.

>Anyway, with the definition of Herbrand interpretation later
>in the document it seems that plain literals are mapped
>into themselves

Yes, they are.

>, just like typed literals.

?? I do not follow your point here. Typed literals do not denote themselves.
Oh, I see. They do in Herbrand interpretations, of course, but this 
is a special case (which needs special treatment in the proofs).

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

Yes, that is correct.

>==
>
>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).

I don't feel that that is necessary.

>Note: for completeness, the line directly following this
>table seems to need to add LV as well.

Right. So done.

>
>==
>
>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.

I agree that the matter is more complicated than I would like it to 
be, but I cannot avoid the complexities of the existential quantifier.

After a great deal of trying things out I have rewritten this more or 
less along the lines you suggest below,  though expressed in places a 
little less rigorously for non-mathematical readers.

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

I agree that the development could be filled out in more rigorous 
detail. However I do not think it would be appropriate to do so in 
this document.

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

Ah, good catch on IP. Thanks.

>  to  IRJ union IPJ  satisfying the following
>conditions:
>- k(IRI) subsetof IRI

The problem is how to say this without using conventions known only 
to mathematicians. You are here using applying a function to its 
domain to indicate its range: but this convention is not only not 
widely understood, but actually violates the class/member conventions 
on which RDF itself is based. I had intended that the use of the 
explicit composition would be a way to avoid these long 
circumlocutions, but perhaps it is better to just tackle the matter 
directly.

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

Again,I do not think that this would be understandable to many 
readers in this compact form. (You were trained in category theory, 
right?)

>- 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.)

This seems to me to be simply a rephrasing of the proof given, but 
taking longer to state because it does not make use of the notion of 
extended vocabulary.  But I will rephrase the section along these 
lines if you think it is easier to follow.  Now done.

>==
>
>(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.)

Well, there are of course entire textbooks devoted to observations 
like this, but we should refrain from putting all of model theory 
into the document, right? :-)

>==
>
>In connection with the preceding remark, the proof of the
>Herbrand lemma could also be adapted to this definition
>of I<<J.

Indeed; again, it is simply a re-statement of the same proof.  Now 
done as suggested.

>==
>
>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.

I see your point, and agree about the 'ideally'; but to keep the 
matters ideally separate in this way would require the re-statement 
of several results; and the inclusion of the XML conditions in 
Herbrand interpretations is harmless to the results proven here, so I 
prefer the more compact if less elegant development.

>
>==
>
>Anonymity lemma: I cannot follow the proof.
>More precisely, why is the first of the two sentences
>("Since ...") true?

It is hypothesized in the statement of the lemma: if E is lean and E' 
is a proper instance of E then...

(??This seems obvious. Am I missing something here??)

>
>==
>
>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.

Actually the section reference is correct, but the wording should 
read 'for simple and RDF interpretations described.... '

Done.

>
>Section 1.1
>
>typo: heirarchy
>

Fixed. I seem to have a localized dyslexia for that particular word.

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 Tuesday, 30 September 2003 19:51:39 UTC