The Problem with Having DAML+OIL Syntax Produce RDF Triples


The problem with including meaningful syntax in interpretations is coming
up with a set of semantic rules that actually work, i.e., don't produce
paradoxes.  Embedding RDF and RDF Schema syntax in RDF interpretations only
works because RDF and RDF Schema are so weak that you cannot get into these
paradoxical situations.  However the situation is different in DAML+OIL as
it is more powerful.

Here is a very simple example using complementOf.

Suppose we want to have a language of classes whose only class constructor
is complementOf.  In RDF syntax complementOf most naturally turns out to be
a property between classes, so we can say

	Thing complementOf Nothing .

or

	notPerson complementOf Person .

We can come up with an RDF-style semantics for this very simple language,
something like the following.

There is a collection of names, V
and a collection of blank nodes, B

An extended interpretation consists of 

	R		      	the domain of resources, nonempty
	EXT : R -> 2^(RxR)	the extension of properties
	CEXT : R -> 2^R		the extension of classes
	S : V -> R		the denotation of names
	A : B -> R		the mapping of blank nodes

An interpretation is an extended interpretation without the blank node map.

We define I as I(n) = S(n) for n a name
	       I(b) = A(b) for b a blank node

An extended interpretation satisfies statements as follows:

	A P O .			< I(A), I(O) > in EXT(S(P))
	A complementOf B .	CEXT(I(A)) = R \ CEXT(I(B))
	
where A,B,O are names or blank nodes and P is a name.

An interpretation satisfies a collection of statements if there is some
extended interpretation that satisfies each statement in the collection and
that matches the interpretation in the obvious way.


So far everything is fine.  We are now at the DAML+OIL point, more or
less.  (See the model theory for DAML+OIL (March 2001) at
http://www.daml.org/2001/03/model-theoretic-semantics.html .)

If we state, for example,

	Person complementOf Person.

all we get is no interpretations that satisfy the (singleton) collection of
statements. 


However, suppose we want to have the meaning of complementOf really show up
in interpretations.

We need to add the following conditions *to interpretations*

An interpretation satisfies the following constraints

	if <a,b> in EXT(S(complementOf))  then CEXT(a) = R \ CEXT(b)


So what is wrong with this?

Well consider the following extended interpretation, with only two names,
and no blank nodes

	R = { equiExtension, complementOf, a }
	S(complementOf) = complementOf
	EXT(complementOf) = { < a,a > }
	EXT(a) = { } 
	CEXT(complementOf) = { }

But when we try to finish this interpretation by determining CEXT(a) we are
in trouble.  If something is in CEXT(a) then, by the semantic rules for
complementOf, it has to not be in CEXT(a).  If something is not in CEXT(a)
then, by the semantic rules for complementOf, it has to be in CEXT(a).

There is no way to determine CEXT(a) and thus we have created an
ill-specified model theory.

In particular, we have gone from a perfectly good syntactic construct,
complementOf, that had a perfectly good meaning for reflexive complementOf,
to an ill-specified model theory.  

Why does this happen?  Well when something is in syntax you can just say,
by means of the model theory, that there is no way that a construction can
result in an interpretation.  However, when something is in the semantics
you don't have this liberty because any semantic construction *has* to make
sense.

(The situation is probably even worse than indicated above because, to make
entailment work correctly, interpretations would have to include all
possible class constructions, and thus, maybe, every interpretation would
be semantically ill-formed, not just some of them.)


A similar thing happens, by the way, in axiomatizations.  An axiomatization
with a similar flaw ends up ends up producing a contradiction from the
empty set of statements.  


The conclusion here is that it is not possible to have DAML+OIL class
constructions be in an RDF-like model theory.  (Well, in the interests of
fairness, there might be a way, but it would have to somehow forbid
complementOf loops of odd lengths.  Worse, these loops might not just have
complementOf relationships but could have many other kinds of
class-relating relationships.  It would be a gigantic mess, at best.)