use/mention and reification: rdf:predicate/subject/object [was: RDF Abstract Syntax...]

Jonathan Borden wrote:
> 
> Dan Connolly wrote:
> >
> >
> > Jonathan Borden wrote:
> > >
> > > > RDF. (http://www.openhealth.org/RDF/RDFAbstractSyntax.html#RDF-MS)
> >
> > I applied the idea of abstract syntax to RDF
> > and found that it matched quite straightforwardly;
> > triples stayed triples:
> >
> >   http://www.w3.org/XML/9711theory/RDFAbSyn.lsl
> >   $Id: RDFAbSyn.lsl,v 1.5 2001/03/30 18:42:44 connolly Exp $
[...]

> First, in order to represent the simple expression:
> 
> (not (color sky blue))
> 
> we need to agree that the presence of a triple in the model _cannot_ be
> equated with _assertion_ of the triple, otherwise expressions such as this
> cannot be represented.

Er... do you mean "we need to agree that the presence
of a triple in the () syntax _cannot_
be equated..."? I'm not sure what you mean by model...

> Rather we can create a container which contains
> _every_ asserted triple.

This business of expressing negation using reification
can sort of work, but not the way you're doing it here...
(i.e. not the way rdf:predicate/subject/object
is typically understood and implemented.)

> [rdf:type #ASSERTED rdf:Bag]
> [rdf:_1 #ASSERTED #S1]
> [:not #S1 ""]
> [rdf:type #S1 rdf:Statement]
> [rdf:predicate #S1 :not]

What do you mean by :not?
Is that a use of the not symbol or a mention of it?

A mention of it (ala 'not) works, but that
doesn't seem to be the way folks use rdf:predicate.

> [rdf:subject #S1 #S2]
> [rdf:object #S1 ""]
> [rdf:type #S2 rdf:Statement]
> [rdf:predicate #S2 :color]
> [rdf:subject #S2 :sky]
> [rdf:object #S2 :blue]

again, do mean color or 'color?

In KIF, there's an axiom schema...
    (<=> (wtr 'p) p)
(provided wtr doesn't occur in p
cf http://logic.stanford.edu/kif/dpans.html#10.3).

so we can trade (not color sky blue) for
	(wtr '(not (color sky blue))

let's suppose rdf_type is defined ala
	(forall (?C ?x) (<=> (rdf_type ?x ?C) (holds ?C ?x))
and let's define a class Falsehood:
	(forall (?formula)
	  (<=> (rdf_type ?formula Falsehood) (wtr '(not ^?formula))) )

and let's let ?s2 = '(color sky blue)
and ?s1 = '(rdf_type ?s2 Falsehood)

and rdf_Statement = KIF triple (i.e. list of length 3)
and rdf_predicate = KIF first
and rdf_subject = KIF second
and rdf_object = KIF third

then we have
	(rdf_type ?s2 rdf_Statement)
	(rdf_subject ?s2 'sky)		; note: 'sky, not sky
	(rdf_predicate ?s2 'color)
	(rdf_object ?s2 'blue)

and
	(rdf_type ?s1 rdf_Statement)
	(rdf_subject ?s1 '?s2)
	(rdf_predicate ?s1 'rdf_type)
	(rdf_object ?s1 'Falsehood)


then it all works out: if we decide ?s1 is true, i.e.
	(wtr ?s1)
then we can use the axioms of
triple/first/second/third to get
	(= ?s1 '(rdf_type ?s2 Falsehood))
so then substituting, we get
	(wtr '(rdf_type ?s2 Falsehood))
and using the wtr axiom schema, we get
	(rdf_type ?s2 Falsehood)
and using triple/first/second/third again, we have
	(= ?s2 '(color sky blue))
and substituting, we have
	(rdf_type '(color sky blue) Falsehood)
then using our definition of Falsehood, we have
	(wtr '(not (color sky blue)))
and using wtr once more,
	(not color sky blue)
QED.

But if you take the quotes (') out,
I can't see how it works. I discovered this problem
back in August when I was writing
  http://www.w3.org/2000/07/hs78/KIF
and I have been trying to make sense of

	(rdf_subject ?s1 color)

without the ' ever since, and I can't make it work.

But translating 'rdf_type back to RDF/xml, it isn't spelled
	http://www.w3.org/1999/02/22-rdf-syntax-ns#type
but rather it needs quoting... something like
	data:,http://www.w3.org/1999/02/22-rdf-syntax-ns#type


So given this bit of RDF based at http://example/stuff,
which asserts that the sky is blue and gives a
name (S2) to the reification of that statement...

	<rdf:Description rdf:about="#sky">
	  <ex:color rdf:ID="S2" rdf:resource="#blue"
		xmlns:ex="http://example/vocab#"/>
	</rdf:Description>

in order to spell out S2, we must write:

  <rdf:Description rdf:about="#S2">
    <rdf:type 
    
rdf:resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#Statement/>
    <rdf:subject
     rdf:resource="data:,http://example/stuff#sky"/>
    <rdf:predicate
     rdf:resource="data:,http://example/vocab#color"/>
    <rdf:object>
     rdf:resource="data:,http://example/stuff#blue"/>
  </rdf:Description>

or perhaps:

  <rdf:Description rdf:about="#S2">
    <rdf:type 
    
rdf:resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#Statement/>
    <rdf:subject>http://example/stuff#sky</rdf:subject>
    <rdf:predicate>http://example/vocab#color"</rdf:predicate>
    <rdf:object>http://example/stuff#blue</rdf:object>
  </rdf:Description>

but perhaps that's so different from the way
rdf:predicate/subject/object are specified, understood,
and used that we need to give them new names.


> so, the expression that is represented by the 7-tuple construct in 2
> statements requires _11_ as triples. Every asserted triples requires _6_
> triples for representation. 1 for the triple, 1 for the container arc and 4
> for the reification quad.
> 
> not very efficient.

The cwm code does some interesting stuff with quads
to represent formulas (i.e. sets of triples-or-formulas).
The substitution routine is remarkably simple; it's
not even recursive:

///////
def _substitute(bindings, list):
    for i in range(len(list)):
        q = list[i]
        list[i] = _lookupQuad(bindings, q)
                            
def _lookupQuad(bindings, q):
        context, pred, subj, obj = q
        return (
            _lookup(bindings, context),
            _lookup(bindings, pred),
            _lookup(bindings, subj),
            _lookup(bindings, obj) )

def _lookup(bindings, value):
    for left, right in bindings:
        if left == value: return right
    return value

  -- http://www.w3.org/2000/10/swap/cwm.py
\\\\\\\

But I'm not sure cwm doesn't have use/mention bugs
too.


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Saturday, 26 May 2001 14:01:29 UTC