DTTF: comprehension

Given that Pat, Peter and Jonathan all think that my proposal is fatally
flawed because of the difficulty of doing comprehension, I had better
address this issue.

Summary:
- an informal list of comprehension rules
  (excluding restrictions)
- the difference between Pat's proposal and mine
- implementations of Peter's proposal and comprehension

Conclusions:
- given that OWL is fairly small (countable) this is not a big deal
- however we approach it there are in any implementation some comprehension
rules
- making these rules explicit is probably a gain not a loss


1: The Comprehension Rules
==========================

My proposal has rules like:

Given a class xxx then
there is a class |intersectionOf xxx|
there is a class |unionOf xxx|

(the notation is a short hand for lots of triples that I think we know, the
above includes lists with one item)

Given two classes
|intersectionof aaa ... | and |intersectionof bbb ... |
then
there is a class
|intersectionof aaa ... bbb ... |
(the above shows finite lists with one or more items being appended)

Given two classes
|unionof aaa ... | and |unionof bbb ... |
then
there is a class
|unionof aaa ... bbb ... |

Given any resource xxx then
there is a class |oneof xxx|

Given two classes
|oneof aaa ... | and |oneof bbb ... |
then
there is a class
|oneof aaa ... bbb ... |

A sample restriction rule given an integer n and a property ppp
then
there is a class
<owl:Restriction owl:minCardinality="n">
  <owl:onProperty rdf:resource="p"/>
</owl:Restriciton>


All of these syntactic expressions above are to be understood as expressing
semantic constraints, rather like the graph closure rules in the RDF Model
Theory.

I believe these rules are sufficiently simple to avoid all the set theoretic
paradoxes because:
- they are characterised by finiteness
- they do not involve any circularity
- the underlying model is countable

The research problems in set theory are characterised by
- transfiniteness
- circular and self referential definitions

Moreover, even if these rules are mistaken, implementors will assume these
rules unless contradictions are explicitly pointed out to them. Thus any
paradox found in the future contained in these rules is an issue for owl
that will require clarification. This need is independent of whether or not
we endorse these rules.

Peter said:
> This theory is so powerful that
> it will contain inconsistencies, leading to a complete breakdown of the
> model theory for the WebOnt language.  (Even if the WebOnt language could
> be expressively limited to disallow the paradoxical classes, the same
> problem will reoccur at higher expressive levels in the Semantic Web
> tower.)

I disagree with the first bit, and believe we should postpone the part in
brackets.

2: Comprehension in Pat's proposal

Pat follows much the same path as above: e.g.
http://lists.w3.org/Archives/Public/www-webont-wg/2002Apr/0338.html
[[[ [Pat]
In OWL it would come from an OWL semantic
constraint of the form that if JOhn is in A and JOhn is in B then
JOhn is in (A intersect B).
]]]
This differs from my proposal merely in that part of the class expression
(the list) is dark. The necessity of some set of comprehension rules and the
difficulty in choosing them is identical.

Hence when Pat suggests that my proposal has
http://lists.w3.org/Archives/Public/www-webont-wg/2002Apr/0253.html
[[[
A blithe confidence that some way will be
found to hack around them should be treated rather like a patent
application for a perpetual-motion machine: its really not worth
getting into the details of what is wrong with it.
]]]
he is also talking about his own proposal.

(I may have misunderstood why he was talking about, in which case I retract
my slur, if Pat will retract all text like the above, or specify, and
justify, *which* proposal is like a perpetual-motion machine).

3. Comprehension in Peter's proposal

Peter's proposal is something like

> If, however, the triples that are used to encode the syntax of the
> constructs of the WebOnt language are unasserted, then these constructs do
> not need to be part of the domain of discourse.  In this case, there is no
> need for comprehension axioms, and a non-trivial theory can be developed
for
> the WebOnt language.

It is unclear whether "the triples that are used to encode" contains ones
with properties such as rdf:type, rdfs:subPropertyOf ..., I certainly take
it to mean all the owl:... ones.

However, there is still the problem of actually reasoning in OWL. A sound
and complete OWL reasoner would be able to conclude that certain mainly dark
syntactic expressions follow for all OWL interpretations.

e.g.

*empty*

entails

rdfs:subClassOf rdf:type |oneOf rdfs:subClassOf|



Peter has not clarified how given a new version of the Patel-Schneider
paradox we would not have

*empty*

entails

Patel-Schneider-Paradox-Q



My previous understanding of Peter's position rested on there being a
separate component, outside of OWL, that does set theoretic reasoning
according to some well known set theory. This, on reflection, seems
problematic since any such reasoner essentially embodies a set of
comprehension principles and, given the real difficulty of some arcane
aspects of set theory, the reasoner is not both sound and complete.

(I don't particularly mind an incomplete reasoner - but it seems strange to
sweep under the carpet in this fashion).


Conclusions:
============
I think Pat and Peter exaggerate this issue.
Finite set theory is trivial, countable set theory is not much harder.
It's only when things get really big that life gets tough and we don't go
there.

Pat's proposal does involve explicit comprehension, illustrating that it's
no big deal.

Peter's proposal does not have explicit comprehension and does not help the
implementator avoid paradox as a result.

In practice implementators will have comprehension rules, and it is a
helpful clarification for us to specify them.

Received on Friday, 3 May 2002 05:52:17 UTC