Strawman Model Theory

Here is my interpretation of the notes Pat sent me outlining his ideas on
a model theory for RDF.  I've taken one or two hopefully minor liberties
with the original (which I've included at the end for comparison):

  I've introduced the notion of a set P of properties
  I've introduced the notion of a set of Strings
  I've couched it in terms of an interpretation of n-triples

As I said in the telecon - all credits to Pat, all mistakes are mine.

Here goes:


Let U be the set of URI References (as defined by RDF 2396).  
          
                          //ignore lang and namespaces for now
Let S be the set of of UNICODE strings (UNICODE*)

An interpretation I consists of:

A set R of thingies

A subset P of thingies which corresponds to Properties

A mapping IN : U -> R

A mapping IEXT : P -> R x R            // R cross R

A mapping IS : S -> R

<s> <p> <o> .  is true in I if and only if:

   s, o are members of U, p is a member of P
   (IN(s), IN(o)) is a member of IEXT(I(P))

<s> <p> "string" . is true in I if and only if:

   s is a member of U, p is a member of P and string is a member of S
   (IN(s), IS(string)) is a member of IEXT(I(p))

Pat goes on to demonstrate a use of this base model theory to
define the meaning of reification:

I(rdf:subject) = { ((s,p,o), s) : s is a member of U, p is a member of P,
                                  o is a member of U union S }

similarly for rdf:predicate and rdf:object.

Pat points out an issue with reification, and I have another,
but I suggest we get the base model theory sorted out before we get
into that.

And Pat's original notes:

Its very simple, really. An interpretation I (of a namespace) is a 
set R of thingies and a mapping extI (for relational EXTension) from 
R to sets of pairs of thingies, and an interpretation mapping from 
identifiers (in the namespace) into R.  (Literals are required by law 
to map to a certain subset of thingies in a predefined way, but 
otherwise are treated like any other names.)  The triple
s P o is true in I just when 's' 'P' and 'o' are all in the namespace and
<I(s),I(o)> is in extI(I(P)); otherwise it is false in I.

(If someone wants to insist that properties *are* their relational 
extension, that amounts to insisting that extI is the identity on R, 
which is a special case. However the set R might then not be 
well-founded (ie there might be membership loops among its members) 
which many mathematicans are uncomfortable with since its 
inconsistent with ZF set theory; but there are perfectly good modern 
set thoeries that allow it. But this is rather an arcane matter which 
can usefully be ignored by non-mathematicians.)

For reification, we require that there are a special class of 
thingies corresponding to triples and names, and give special 
interpretations for the 'subject'and 'object' and 'predicate' 
properties as follows (I'll just do 'subject')
I('subject')= {< [s P o] , s> : s,P,o in namespace(I) }
where [x y z] indicates the thingie in R that stands for the triple 
with subject x, property y and object z.

A few issues that crop up for reification (1) do we want to say that 
the things in the domain *are* the triples, or are just some category 
of things that are 1:1 with the triples? (2) The way Ive stated it, 
each theory can only reify triples made from its own namespace. Is 
this adequate, or do we want reification to include all possible 
names (even those involving URIs that havnt been invented yet)?

Brian

Received on Monday, 23 July 2001 03:05:20 UTC