- From: Graham Klyne <GK@ninebynine.org>
- Date: Sun, 27 May 2001 09:43:43 +0100
- To: Dan Connolly <connolly@w3.org>
- Cc: Jonathan Borden <jborden@mediaone.net>, Drew McDermott <drew.mcdermott@yale.edu>, www-rdf-logic@w3.org
At 01:01 PM 5/26/01 -0500, Dan Connolly wrote:
>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.
Going out on a limb here, I'm going to hazard a guess that you need
quotation to make sense of this using the KIF wtr axiom schema, because wtr
is defined in terms of quotation.
Is it not a different approach to have the subject resource of a statement
reification stand for the *interpretation* of the statement in the domain
of discourse, rather that a quotation of the original statement? (I rather
thought that this was what Pat Hayes was trying to suggest in a previous
message [1].)
#g
--
[1] http://lists.w3.org/Archives/Public/www-rdf-logic/2001May/0071.html
At 01:01 PM 5/26/01 -0500, Dan Connolly wrote:
>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/
------------
Graham Klyne
GK@NineByNine.org
Received on Sunday, 27 May 2001 04:46:58 UTC