Re: S&AS review: Section 5

From: herman.ter.horst@philips.com
Subject: S&AS review: Section 5
Date: Wed, 26 Mar 2003 15:09:37 +0100

> OWL - Semantics and Abstract Syntax
> Version of 20 March 2003
> 
> As in the other message, I go sequentially through the text.
> 
> 
> Section 5.2
> 
> In the introductory sentences and also in the first definition, D
> is called datatype theory.  This is not consistent with
> the RDF Semantics document and also not with your own
> text in Section 3.1: there, a datatype theory is a tuple
> including D.
> Therefore, D should be described as being a set of datatypes,
> in these two places, and also in the beginning of Appendix A.1.

I've changed from D to T.  I can't change to be like the RDF Semantics
until the RDF datatypes are fixed.

I've added

	(The specifics of datatype theories used here differ from those in
	the RDF semantics because there are continuing problems with RDF
	datatyping.  It is hoped that these problems will be resolved
	during last call, at which time this document will be revised to
	correspond directly to RDF datatyping.)


> Replace
> >..., subset of RI.
> by 
> >..., and is a subset of RI.

I don't see a place where this is appropriate.

> The current version of the RDF Semantics document
> clearly defines the domain of ICEXT to be the set IC. 
> This should be incorporated in the document. 
> For your convenience, I completely describe the 
> required changes, also in connection with the appendix.

> Replace the sentence
> >CEXTI is then defined as CEXTI(c) = ...
> by the following two sentences:
> "CI, the set of classes, is defined by
> CI = {x in RI | <x,SI(rdfs:Class)> is in EXTI(SI(rdf:type)>}.
> CEXTI is a mapping from CI to P(RI), defined for each
> c in CI by CEXTI(c) = [exactly what is already in the text].
> "

I disagree with this characterisation of ICEXT, and will not make these
changes.

> Replace 
> >... that are correspond to constructors ...
> by
> "... that correspond to constructors ..."

Done.

> The first table, "Conditions concerning the parts of the OWL
> universe and syntactic categories" needs to be completed
> in connection with CI:  Each of the 11 empty cells in the
> first column (SI(E) is in ...) needs to be filled with the
> set CI.  Otherwise, as discussed before, many invocations
> of CEXTI that occur later are are not clearly legal.

I disagree.

> I believe that five more lines need to be added to this table,
> for the following vocabulary elements
> (the reason is, as before, that otherwise it is not clear
> that various function invocations occurring later are legal):
> 
> If  E is                      .SI(E). .CEXTI(SI(E)).    and
>   owl:Datarange                 CI       ?      ? subsetof CI
>   owl:SymmetricProperty         CI       ?      ? subsetof IOP
>   owl:FunctionalProperty        CI       ?      ? subsetof IOP
>   owl:InverseFunctionalProperty CI       ?      ? subsetof IOP
>   owl:TransitiveProperty        CI       ?      ? subsetof IOP
> Where I put a question mark I leave it open whether you
> want to define specific sets for these; this would seem 
> most natural to me.

I disagree.

> There are only two further additions to be made:
> the entities SI(owl:DeprecatedClass) and SI(owl:DeprecatedClass)
> need to be put in CI as well.
> (This is used in the proofs in Appendix A.1.)

Done.

> It seems that the last line of the first table, on "l"^^d
> can be left out, since it is implied by the RDF Semantics.
> Or, leave it in and change the note to
> "This condition is also in the RDF model theory", as you do
> in the next table also.

This condition is not in the RDF semantics.  It augments RDF datatyping to
make, for example "1.5"^^xsd:integer have no interpretations.

> By the way, I like the notes that you added to the tables.
> These notes, in combination with the new headers of the tables,
> improve the readability of this section.

> In the first two lines of the same first table, CEXTI(SI(rdfs:Class))
> should be replaced by CI, as this is equal and as it is
> the more fundamental entity in the RDF Semantics, and as
> it simplifies this table.

I've already made this change (but only to conserve space).

> In the third part of the table
> "Characteristics of OWL classes, datatypes, and properties",
> "If E is ... then if e is in CEXTI(SI(E)) then"
> e should be replaced by c in this header.

I don't see where this change is indicated.

> In the table "Further conditions on owl:oneOf"
> the last conclusions "and CEXTI(x)={y1,...,yn}"
> can (and in my view should) be omitted, as they
> are already stated in the table before.

Done.

> The last remark on this section returns to a point we discussed
> earlier.  In the semantics of the cardinality restrictions,
> v should be taken from IOT union LV (three times).
> As mentioned before, there is an immediate proof
> that the entity {v in IOT union LV: <u,v> in EXTI(p)}
> is a set, which is required since its cardinality is taken.
> Also, it is done in exactly the same way in the direct semantics.

I view this change as neither necessary nor desirable, but will very
reluctantly make it.

> Section 5.3
> 
> In the table defining OWL Full interpretations, CEXTI(SI(rdfs:Class))
> should be replaced by CI and CEXTI(SI(rdfs:Property)) should be 
> replaced by PI, as these entities are equal and are more fundamental
> in the RDF Semantics, and since these substitutions simplify
> the definition.

Already done, but only to conserve space.

> Question: why is the definition of 'imports closed' given in this
> section?  It is not used in this section.

It has to be somewhere, as it is referred to from Test.  It is not used
elsewhere in the document, so I'm not sure where it should go if it is not
here.

> Delete bracket ) following "OWL vocabulary".

Done.


> Appendix A.1
> 
> This is not a complete review of this appendix.
> However, in connection with what is discussed above about
> CI/CEXTI, I looked far enough to ensure that the appendix
> becomes completely consistent: each invocation of CEXTI
> done there is legal when the above changes are made.
> 
> I noted also that in the proof of Lemma 4, starting with the
> 6th bullet, very many invocations of the function SI need
> to be added, in expressions such as CEXTI(rdf:type).

Yuck.  I think that I've fixed them all.  Also for EXTI(rdf:type).

> In the same, long, bulleted list, note that many invocations
> of CEXTI need to be replaced by EXTI and vice versa.
> I could list these for you, but I assumed that you can find
> them quicker yourself, by just using the following rules:
> - owl/rdf vocabulary element starts with lower case: use EXTI
> - owl/rdf vocabulary element starts with capital: use CEXTI

No.  This is not correct.  OWL/RDF vocabulary elements that start with
lower case need a CEXTI to complete the definition of EXTI(SI(rdf:type).
OWL/RDF vocabulary elements that start with a capital need an EXTI, because
I've defined PI rather expansively to include the denotation of all the
built-in vocabulary.

> Herman

Today's version of the document has been updated to include all these
changes.

peter

Received on Wednesday, 26 March 2003 14:29:48 UTC