Re: Syntax proof

Jeremy Carroll wrote:

> 
> I have done a first version of a sufficiency proof.

[...]


> 
> Working on the proof resulted in [...]

 >

greater insight into a philosophical difference between



> my text and Peter's which I explore in the next message 


Here's the insight, if it's that.

Most syntax is incremental - you can add, remove and move fairly small bits 
of a syntactic valid document, and it remains syntactically valid.
e.g. in an abstract syntax expression:

Ontology(
   DatatypeProperty( dp, range( xsd:int ) )
   Individual(
     type(
       restriction(
           dp
           minCardinality(1)
           someValuesFrom( xsd:byte ) )
       )
     )
   )
)

we can swap the order of the directives, we
can remove one or both of the constraints in the restriction.
We can remove the type expression or the range expression.
We can remove one or both of the directives.

My version of the mapping rules allows both the abstract syntax and the 
concrete syntax to behave incrementally. The proof relies on that 
incrementality because each step in the proof removes 1, 2 or 3 triples 
from the graph, and leaves it syntactically valid.

Those of Peter's mapping rules that I have most difficulty do not permit 
the removal of just a few triples. The DisjointClasses rule requires 
removing n triples for arbitrarily large n. The rule for mapping 
restrictions with multiple parts (like in the ontology above) makes a 
single structure that is monolithic in OWL Lite. I think that under Peter's 
rules for the above structure there are no syntactically well-formed 
subgraphs of the graph, other than those that completely delete the 
restriction.

This lack of incrementality makes the concrete syntax significantly 
difficult to use and to program with - and will lead to interoperability 
difficulties.

An aspect of my approach that I have not actively advocated yet is the 
meaningless top-level directives - descriptions, restrictions (and now also 
dataranges).

These are there to enhance the incrementality of the concrete syntax.
In a way they correspond to a statement like:
   x+3;
or
   sideEffectFree(x,4,foo);
in C. Both might generate a compiler warning, "statement has no effect"
but they are not *syntactically* ill-formed.
(Indeed in C++ one cannot tell that x+3; has no effect)

As an example of the incrementality with a restriction:

<rdf:RDF>
   <owl:Restriction>
      <owl:onProperty>
        <owl:ObjectProperty rdf:ID="p"/>
        <owl:someValuesFrom>
          <owl:Class rdf:ID="c"/>
        </owl:someValuesFrom>
      </owl:onProperty>
      <owl:equivalentClass>
          <owl:Class rdf:ID="d"/>
      </owl:equivalentClass>
    </owl:Restriction>
</rdf:RDF>

corresponding to

Ontology(
    EquivalentClasses(
         restriction( p, someValuesFrom( c ) )
         d
    )
)

With Peter's rules this element must either be kept or deleted as a whole 
(the class and property declarations can be made separate).
Allowing a meaningless restriction allows removing the equivalentClass 
element to leave:

<rdf:RDF>
   <owl:Restriction>
      <owl:onProperty>
        <owl:ObjectProperty rdf:ID="p"/>
        <owl:someValuesFrom>
          <owl:Class rdf:ID="c"/>
        </owl:someValuesFrom>
      </owl:onProperty>
    </owl:Restriction>
</rdf:RDF>

which is not a very interesting ontology since it does not constrain 
anything very much (p must be an ObjectProperty and c a class).
I do not find that lack of interest sufficient to justify making this 
syntactically ill-formed.
The ability to break the task of understanding an OWL ontology down into 
its little pieces is enhanced when these little pieces are syntactically valid.

I have not suggested toplevel directives corresponding to the rdf:List 
constructs in the concrete syntax. This has the effect that all rdf:List's 
must be the object of exactly one triple.
As a result, the steps in the proof to deal with lists
http://www.w3.org/2001/sw/WebOnt/syntaxTF/prolog/out/dl/proof1.html#lemma-first-list-reduction
and
http://www.w3.org/2001/sw/WebOnt/syntaxTF/prolog/out/dl/proof1.html#lemma-second-list-reduction
are significantly more complicated than they need be.
However, to do otherwise, would work badly with RDF/XML's 
parseType="Collection" - which should probably be the main driver for the 
clarity of the concrete syntax, rather than the abstract syntax of RDF.

Jeremy

Received on Monday, 3 March 2003 15:23:27 UTC