Re: Strawman Model Theory

Dan Connolly wrote:
> 
> Brian McBride wrote:
> [...]
> 
> Looks good, mostly...
> 
> > Here goes:
> >
> > Let U be the set of URI References (as defined by RDF 2396).
> 
> I don't think you mean that relative URI references
> are in U. I think U is the set of absolute URI references;
> i.e. URIs with optional #fragment thingies.

Yes.

> 
> >                           //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))
> 
> that last P should be little, no? IEXT(I(p))

Yes

> 
> > <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))
> 
> Just 3 major things missing:
> 
> 1. existentials:
> 
>         _:x <p> <o> is true in I iff
>         o is a member of U, p is a member of P,
>         and there is some thingy tx in I's set of thingies
>         so that (tx, IN(O)) is a member of IEXT(I(p))
> 
>         The substitution (tx for _:x) is
>         said to satisfy the triple _:x <p> <o>.
> 
>         In general, a substitution has
>         any number of (thingy for _:name, thingy2 for _:name2, ...)
>         pairs.

There is a followup message to the original with this in - stuff I added
that were not in Pat's original notes

> 
> 2. conjunctions
> 
>         a list of triples is satisfied by
>         some substitution if each of the triples
>         in it is satisfied by that substitution.

ditto

> 
> 3. putting it all together
> 
>         A list of triples is true in I iff there's some
>         substitution that satisfies it.

Better worded than mine, but ditto

> 
> > Pat goes on to demonstrate a use of this base model theory to
> > define the meaning of reification:
> [...]
> > 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.
> 
> Yes, let's leave that for a rainy day...
> 
> Just one of Pat's notes seems essential:
> 
> > (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.)
> 
> I'd say literals map to themselves. i.e. IS is the
> identity function.

Could be.  Pat did talk about the integer 5 being a literal which is
not the same thing as the string "5".  I figured we could stay
agnostic on this till we get to datatyping.

Brian

Received on Monday, 23 July 2001 04:17:11 UTC