W3C home > Mailing lists > Public > www-rdf-logic@w3.org > January 2001

RE: Maximum cardinality of an RDF model

From: Miles Sabin <MSabin@interx.com>
Date: Tue, 23 Jan 2001 13:24:05 -0000
Message-ID: <23CF4BF2C499D411907E00508BDC95E116FB88@ntmews_01.interx.com>
To: www-rdf-logic@w3.org
pat hayes wrote,
> However, your question raises another, related, issue: 
> according to several members of the group which developed 
> RDF, the 'graph model' of a set of RDF triplets is intended 
> itself to be *the* model (in the sense from model theory) of 
> those triplets. It follows that all RDF models of any RDF 
> ontology (that could be stored on any web page, at any rate) 
> must be not only countable, but finite.

Hmm ... I don't see that. It doesn't seem to follow from the
(admittedly vague) sketch of the graph model in rdfms: I don't 
see any restrictions on the cardinality of the class of 
vertices, other that implied by the cardinality of the set of
URIs; and I don't see any restrictions on the cardinality of
the set of edges leaving a given vertex, again apart from the
URI constraint.

And, if Brian McBrides response to my earlier question about
the cannonical URIs corresponding to rdf:_1 etc. is correct,
we can easily construct an RDF/XML document which requires a
countably infinite model,

  <rdf:Description
    aboutEachPrefix="http://www.w3.org/1999/02/22-rdf-syntax#_">
    <s:Type>Membership Property</s:Type>
  </rdf:Description>

makes an assertion about each of rdf:_1, rdf:_2 etc.

> Now, since the finite-model restriction is not expressible in 
> first-order (or any complete semi-decideable) logic, this would 
> appear to indicate that RDF must have a semantics which 
> has no semidecision procedure (and hence no proof procedure.)

Hmm ... well, as things stand, core RDF has no _proof_ procedure
for the simple reason that it has no inference rules.

Even so, if there _were_ a finite model restriction we would have 
something approximating to soundness, completeness, and a 
finitary decision procedure: every finite chunk of RDF/XML would
correspond to some finite graph model; every finite graph model 
would correspond to some finite chunk of RDF/XML; and we could 
check for the presence or absence of a given assertion by simple
enumeration (which is the closest we can get to a decision
procedure in a language without inference rules).

To be sure the finite model condition wouldn't be expressible in
RDF/XML, but it would be expressible in the metalanguage used
to construct the model, assuming that were strong enough. 

In any case, given the example I gave above of an RDF/XML doc 
which requires a countably infinite model, there'd better _not_
be a finite-model restriction.

Cheers,


Miles

-- 
Miles Sabin                               InterX
Internet Systems Architect                5/6 Glenthorne Mews
+44 (0)20 8817 4030                       London, W6 0LJ, England
msabin@interx.com                         http://www.interx.com/
Received on Tuesday, 23 January 2001 08:24:43 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:38 GMT