Re: Model theory review, thumbs up

BTW, I'm keeping the 'current edit' at 
http://www.coginst.uwf.edu/~phayes/RDF_Semantics_latest.html
this has everything in [1] now de-styled, so anything in red is a 
post-Friday-snapshot edit.

One big change since yesterday:  I have moved the condition

rdf:nil rdf:type rdf:List .

from  RDFS to the RDF interpretation case, since its entirely phrased 
in the RDF vocabulary. Turns out that this makes some other things 
neater as well.


>Reviewing [1]:
>
>[1] 
>http://lists.w3.org/Archives/Public/www-archive/2002Nov/att-0022/01-RDF_20Model_20Theory_Oct_draft.html
>
>My report to the group is that this is fit to publish.
>
>I would prefer (but don't insist) that 2nd para of section 1.3 is 
>not included.

Gone.

>
>Other comments below are non-editorial, in the sense that I felt 
>they might impact how the document was understood.  But none of them 
>are essential.
>
>...
>
>Section 1.2:
>
>Note that "character string" is a sequence of Unicode characters?

Done

>
>[Later: I see this is mentioned in 0.2]
>
>...
>
>Section 1.4:
>
>Para 2:  following the definition of simple interpretation, I think 
>it is the case that there are no practical uses for it (all RDF 
>graphs being subject to at least RDF-entailment)?

Probably, but its the reduction case for all the entailment lemmas.

>
>...
>
>Section 1.4:
>
>5th para states "assume that LV is a subset of IR"
>
>item 2 says:  powerset of IRx(IR union LV)
>
>surely the latter is now redundant, and could read powerset of IRxIR ?

Yes, done. Also that section has been re-worded to make some of the 
issues clearer

>
>...
>
>Similarly, mention of "y in IR or LV".

Gone.

>
>...
>
>Section 3.2.1
>
>Para 2 mentions "I(aaa) is a token of an RDF triple"
>
>Para 4 has "when x is an occurrence of an RDF triple with the form"
>
>The latter suggests to me that the RDF triple has to actually 
>*occur* somewhere, and some might think that means the graph under 
>consideration.  My suggestion is to change the text in para 4 to 
>read:  "when x is a token of an RDF triple with the form"

Done.
Re. the following, I have rewritten some of the prose in these paras 
to try to make the meaning more precise. It is tricky to get this 
right!!

>
>Para 6 also talks about "a triple in a particular RDF document", 
>again suggesting the triple actually exists unreified, which I think 
>it may not.  (e.g. If my document said "Bill rdf:type ex:Clown" then 
>Bill might be upset with me.)  Suggest:  "a occurrence or notional 
>occurrence of a triple in a particular representation of an RDF 
>graph".
>
>...
>
>Section 3.2.1
>
>I'm uneasy about trying to tie the intended interpretation of 
>reification to a concrete syntax.  In the preceding para, you 
>discuss "apply the interpretation mapping again to get the 
>referent...".  Doesn't the interpretation mapping apply to the 
>abstract syntax, not a concrete syntax?

Yes, but I don't want to get too deeply into this issue. Ive tried to 
word the token/graph language carefully enough now to avoid this.

>
>...
>
>Section 3.2.3
>
>Final para, "should always describe a linear sequence", reads as if 
>lists containing lists are not recommended;  I don't think that's 
>intended, and I have used lists in which some of the elements are 
>themselves lists.

That wasn't intended, Ive added a guard sentence.

>
>...
>
>Section 3.4
>
>Para 3 says "datatype aware RDF engine should ... recognize ... and 
>the set of all the XML schema datatypes".  All?  There seems to be a 
>fair bit of stuff there that doesn't really apply (e.g. ENTITIES). 
>I think this could be limited to the primitive datatypes

Good point, changeds to say 'at least.... the primitive...'.

>(http://www.w3.org/TR/xmlschema-2/#built-in-primitive-datatypes), 
>and maybe the derived integer types.
>
>...
>
>Section 3.4
>
>The ^^ notation appears here without, as far as I have noticed, any 
>prior introduction.

Well, I assume it is covered in the reference to Ntriples.

>
>(Section 0.2 introduces typed literals as pairs.)
>
>...
>
>Section 3.4
>
>I observe that the treatment of invalid literals means that one can 
>legitimately construct an interpretation in which invalid typed 
>literals have useful meanings;  e.g. that a property extension for p 
>might be arranged so that whenever:
>
>    s p "10"^^xsd:integer .
>
>is true, then
>
>    s p "ten"^^xsd:integer .
>
>is also true.
>
>(I don't think this is a problem, just observing.)

Right, I hadnt thought of that, good point. I don't think I will go 
into that in the doc, though.

>
>...
>
>Section 4.3
>
>I find myself uneasy about the lack of any form of entailment lemma 
>for datatype closures.

Me too, see below.

>
>Given that the D-interpretation is defined in terms of a given set D 
>of datatypes, it seems to me that it should be possible to define 
>some rules in terms of the L2V of those datatypes (which I take to 
>be equivalent to "consulting the datatype sources").  I don't have 
>time right now to think this through, but it would be interesting to 
>see if there's something more satisfying (sic) that can be said here.

I think it can be said in terms of large/countable sets of equations. 
I will try to make some useful remarks along these lines: check the 
doc in a few hours to see.

No doubt one ought to talk about facets, but I really have trouble 
following the XML docs at that point. Ive been using numbers all my 
life and I never noticed they had facets before.

>
>...
>
>Appendices not checked.

Im working on them. SOme of the proofs are simpler now, one or two 
are distinctly harder.

Pat
-- 
---------------------------------------------------------------------
IHMC					(850)434 8903   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 Saturday, 9 November 2002 15:18:53 UTC