From: Peter F. Patel-Schneider (pfps@research.bell-labs.com)
Date: 12/03/01
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
workd because RDF and RDF Schema are so weak that you cannot get into these
paradoxical situations.
Here is a very simple example using complemenentOf.
Suppose we want to have a language of classes whose only class constructor
is complementOf and whose only class definition mechanism is equiExtension.
In RDF syntax these both most naturally turn out to be properties of
classes, so we can say
Thing complementOf Nothing .
or
Person complementOf _:1 .
_:1 equiExtension notPerson .
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 equiExtension B . CEXT(I(A)) = CEXT(I(B))
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.
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 equiExtension and
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(equiExtension)) then CEXT(a) = CEXT(b)
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(equiExtension) = equiExtension
S(complementOf) = complementOf
EXT(complementOf) = { < a,a > }
EXT(equiExtension) = { }
EXT(a) = { }
CEXT(equiExtension) = { }
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 construct can
make sense. However, when something is in the semantics you don't have
this liberty because any semantic construct *has* to make sense.
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.
NB: I was planning on using equiExtension to show that an example without
having complementOf being reflexive also exhibited the semantic paradox,
but I didn't need to. I'm leaving equiExtension in just in case I have to
show this later.
From: Dan Connolly <connolly@w3.org>
Subject: Re: how to handle DAML+OIL syntax in the RDF model theory
Date: Fri, 30 Nov 2001 17:20:58 -0600
> "Peter F. Patel-Schneider" wrote:
[...]
> > You would need to include all DAML+OIL syntax in every interpretation,
> > i.e., unionOf for every list of classes, ..... I'm uncertain if this
> > approach would work.
>
> Hmm... I assumed it was already working. I suppose
> I was reading more into the DAML+OIL model theory than was there.
[...]
> > However, even if it would, I have severe reservations. I liken it to a
> > mechanism for including disjunction in RDF that would work something like.
[...]
> Er... ok, I'll bite... why does this sort of thing bother you?
>
> I ask mostly because our implementation of logic on top
> of RDF works pretty much exactly this way. At least: I think
> it does, after interviewing TimBL about it... I'm never
> quite sure what theory best explains what the code does,
> but I've been reasonably confident that this theory
> matches Tim's code and writings and such
> since I discovered it in September:
>
> a formal design for RDF/N3 context/scopes
> Dan Connolly (Thu, Sep 06 2001)
> http://lists.w3.org/Archives/Public/www-rdf-logic/2001Sep/0004.html
>
> In N3, log:implies isn't really a logical connective;
> it's a relation constant, ala
>
> (defrelation log:implies (?P ?Q) :=
> (wtr ^(=> ,?P ,?Q))
>
> so that
> { :x :y :z. } log:implies { :p :d :q }.
> pretty much means
> (wtr ^(=> (y x z) (p d q)))
>
> It's really pretty strange... it means that the universal
> quantification in most N3 rules is over *terms*, not
> over objects. I thought this was totally wierd,
> but I've run into folks that don't think so; they
> call it "schematic quantification" or something like that.
>
> Anyway... logical disjunction is introduced similarly...
> there are classes log:Truth and log:Falsehood,
> and rules
>
> this log:forAll :P, :Q, :R.
>
> { :P log:or :Q.
> :P a log:Falsehood } log:implies
> { :Q a log:Truth }.
> { :P log:or :Q.
> :Q a log:Falsehood } log:implies
> { :P a log:Truth }.
>
> { :P log:or :Q.
> :P log:implies :R.
> :Q log:implies :R. }
> log:implies { :R a log:Truth }.
>
> Our rules engine doesn't use any tactics that really
> exploit the last rule -- it only does forward chaining --
> but it seems to do sensible
> things with the first two. Oh... actually, I think
> the rules engine pays special attention to
> :X a log:Truth
> but I haven't really tested it.
>
I haven't looked at the details of this, but I would be very concerned that
there is some paradox lurking here.
> --
> Dan Connolly, W3C http://www.w3.org/People/Connolly/
Peter F. Patel-Schneider
Bell Labs Research
This archive was generated by hypermail 2.1.4 : 04/02/02 EST