spec#issue-output-formats formal specification in terms of graphs

Splitting the editing work with Murray prompted me to look
more closely at the formal guts of the specification and
take out fluffy stuff like "preserve the meaning..."
and formally define "GRDDL result".

Consequently, I currently lean toward the less constrained
position on issue-output-formats, i.e. yes, a GRDDL
transformation may produce RDF in a format other than RDF/XML.

The current text is:

[[
Stated more formally:

      * An XML document whose root element has an attribute with a local
        name of transformation and a namespace name of
        http://www.w3.org/2003/g/data-view# has a GRDDL transformation
        for each resource identified by a URI reference listed in the
        value of the attribute (c.f. section 4.4.1. URI references in
        [WEBARCH]).
      * If ?D is an XML document with GRDDL transformation ?T, then the
        result of applying ?T1 to ?D is a GRDDL result of ?D. 
      * If ?G1 and ?G2 are GRDDL results of ?D, then the merge of ?G1
        and ?G2 is also a GRDDL result of ?D.
]]
 -- http://www.w3.org/2004/01/rdxh/spec#grddl-xml


Even more formally, I worked out the details of those rules in N3.
http://www.w3.org/2004/01/rdxh/grddl-rules.n3

I'm thinking about how to integrate this into the spec; maybe
as an appendix, along with the sample implementation appendix
that I still hope to get to, eventually.

The last rule is pretty straightforward
(assuming you grok N3 syntax, which is kinda close to SPARQL...
if you don't, you can probably stop reading here...)

{ ?D grddl:result ?G1, ?G2.
  (?G1 ?G2) log:conjunction ?G
} => { ?D grddl:result ?G }.


The middle one is not too bad... we treat tranformations
as RDF properties that relate their input to their output.
hmm... the prose isn't careful to separate ?D from ?TXT...

{ ?D grddl:transformation ?TX; w:representation [ w:bodyText ?TXT ].
  ?TXT ?TX ?G
} => { ?D grddl:result ?G }.

And the first one is fairly hairy; it brings in an infoset ontology
and log:uri and a made-up built-in to parse XSD string lists...

{ ?INFORES log:uri ?BASE; w:representation ?M.
  ?M a w:XMLMessage; w:bodyText ?TXT.
  ?TXT xml:infoset [
    infoset:documentElement [
      infoset:attribute [
       infoset:namespaceName "http://www.w3.org/2003/g/data-view#";
       infoset:localName "transformation";
       infoset:normalizedValue [ xsd:stringListParse [ is list:in
of ?TXref ] ]
      ]
    ]
  ].
  (?TXref ?BASE) w:urijoin [ is log:uri of ?TX ].
} =>  { ?INFORES grddl:transformation ?TX }.

I think that glosses over some xml:base details too.
I hope to flesh those out in due course.


To test this, I worked on
 http://www.w3.org/2004/01/rdxh/grddl-rule-tests.n3

Here's the 1st test case in there; we have an XML document
with grddl:transformation="...grokCC.xsl"...

doc1 w:representation [ a w:XMLMessage; w:bodyText txt1 ].
txt1 xml:infoset [
    infoset:documentElement [
      infoset:attribute [
        infoset:namespaceName "http://www.w3.org/2003/g/data-view#";
	infoset:localName "transformation";
	infoset:normalizedValue
	  "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl";
      ]
    ]
  ].

And let's state as a fact what that transformation does
to txt1... hmm... this glosses over the fact that XSLT
specifies its output at the XML level, and we're looking
at it at the RDF graph level. I may need to work on that
a bit..


txt1
 <http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl>
 { doc1 rights shareAlike }.


If we run cwm on these rules and this test input, we
do in fact get the relevant conclusion:

    :doc1     grddl:result {:doc1     :rights :shareAlike . } .


I even got cwm to spit out a proof and check it, sort of.
The check actually fails due to some bug in the
proof representation of list axiom steps. The trace
below is actually edited to work around a few other
bugs in the cwm proof stuff too. But I think it's
kinda interesting to pore over...


1: ...
 [by parsing <grddl-rule-tests.n3>]

2: [** steps 2, 3, 5, and 6 are the result of a cwm bug; they're really
part of step 4]

4: @forSome :_g7 . g:txt1 w:infoset [infoset:documentElement
[ infoset:attribute [ infoset:normalizedValue
"http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl"]]].
 [by erasure from step 1]

7: "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" :notMatches
" " .
 [by built-in Axiom str:notMatches]

8: @forAll :S . { [ infoset:normalizedValue :S ]. :S str:notMatches "
" . } log:implies {:S w:stringListParse ( :S ) . } .
 [by erasure from step 1]

9: ...
 [by rule from step 8 applied to steps [4, 7]
  with bindings {'_g_L14C3': '[...]', 'S': '"http....xsl"'}]

10:
"http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" :stringListParse ( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" ) .
 [by erasure from step 9]

11: "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" :in
( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" ) .
 [by built-in Axiom list:in] [**I fixed cwm's goof on this step]

12: @forSome :_g6 . :_g6 infoset:localName "transformation";
 infoset:namespaceName "http://www.w3.org/2003/g/data-view#".
 [by erasure from step 1]

13: [**more buggy steps elided]

16: @forSome :_g8 . g:doc1 w:representation [ a w:XMLMessage; w:bodyText
g:txt1].
 [by erasure from step 1]

17: :doc1 log:uri
"file:/home/connolly/w3ccvs/WWW/2004/01/rdxh/grddl-rule-tests#doc1" .
 [by built-in Axiom log:uri]

18: [**buggy/duplicate steps left out]

20: @forAll :BASE, :DOC . { :DOC log:uri :BASE; w:representation [ ] . }
log:implies
{ ( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" :BASE )
w:urijoin
"http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" . } .
 [by erasure from step 1]

21: ... [**next step tells you what this ... is, or at least part of it]
 [by rule from step 20 applied to steps [17, 19]
  with bindings {'_g_L18C25': '[...]', 'BASE': '"file...doc1"', 'DOC':
'<file:/home/connolly/w3ccvs/WWW/2004/01/rdxh/grddl-rule-tests#doc1>'}]

22: ( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl"
"file:/home/connolly/w3ccvs/WWW/2004/01/rdxh/grddl-rule-tests#doc1" ) :urijoin "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" .
 [by erasure from step 21]

23: <http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl> :uri
"http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" .
 [by built-in Axiom log:uri]

24: ...
 [by parsing <grddl-rules.n3>]

25: @forAll :BASE, :INFORES, :M, :TX, :TXT, :TXref . { @forSome
run:_g10, run:_g9 . ( :TXref :BASE ) w:urijoin run:_g10 . :INFORES
log:uri :BASE; w:representation :M . :M a w:XMLMessage;
w:bodyText :TXT . :TX log:uri run:_g10 . :TXT w:infoset
[ infoset:documentElement [ infoset:attribute [ infoset:localName
"transformation"; infoset:namespaceName
"http://www.w3.org/2003/g/data-view#"; infoset:normalizedValue
[ w:stringListParse run:_g9 ] ] ] ] . :TXref list:in run:_g9 . }
log:implies {:INFORES grddl:transformation :TX . } .
 [by erasure from step 24]

26: ...
 [by rule from step 25 applied to steps [4, 10, 11, 12, 16, 17, 22, 23]
  with bindings {'_g_L79C28': '"http....xsl"', '_g_L70C20': '[...]',
'_g_L75C32': '"http....xsl"', 'TX':
'<http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl>',
'_g_L72C25': '[...]', 'M': '[...]', 'BASE': '"file...doc1"', 'INFORES':
'<file:/home/connolly/w3ccvs/WWW/2004/01/rdxh/grddl-rule-tests#doc1>',
'_g_L71C29': '[...]', '_g_L75C54': '?', 'TXT':
'<file:/home/connolly/w3ccvs/WWW/2004/01/rdxh/grddl-rule-tests#txt1>',
'TXref': '"http....xsl"'}]

27: :doc1 grddl:transformation
<http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl> .
 [by erasure from step 26]

28: :txt1 <http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl>
{:doc1 :rights :shareAlike . } .
 [by erasure from step 1]

29: @forSome :_g8 . g:doc1 w:representation [w:bodyText g:txt1] .
 [by erasure from step 1]

30: [**buggy; part of 29]

31: @forAll :D, :G, :TX, :TXT . { :D grddl:transformation :TX;
w:representation [ w:bodyText :TXT ] . :TXT :TX :G . } log:implies {:D
grddl:result :G . } .
 [by erasure from step 24]

32: ...
 [by rule from step 31 applied to steps [27, 28, 29]
  with bindings {'D':
'<file:/home/connolly/w3ccvs/WWW/2004/01/rdxh/grddl-rule-tests#doc1>',
'TXT':
'<file:/home/connolly/w3ccvs/WWW/2004/01/rdxh/grddl-rule-tests#txt1>',
'TX': '<http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl>', 'G':
'{g:doc1 g:rights g:shareAlike}', '_g_L58C49': '[...]'}]

33: :doc1 grddl:result {:doc1 :rights :shareAlike . } .
 [by erasure from step 32]



Anybody who has read this far might want to try it out.
The Makefile has enough details that you should be able
to follow your nose...
  http://www.w3.org/2004/01/rdxh/Makefile


In particular, the relevant stanzas are...

#######
grddl-rule-test-pf.txt: grddl-rule-test-pf.n3
	PYTHONPATH=$(SWAP)/.. $(PYTHON) $(SWAP)/check.py --report
grddl-rule-test-pf.n3 >$@


grddl-rule-test-pf.n3: grddl-rule-tests.n3 grddl-rules.n3
grddl-rule-goal.n3
	$(PYTHON) $(CWM) grddl-rule-tests.n3 grddl-rules.n3  \
		--think  --filter=grddl-rule-goal.n3 --why >$@


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Wednesday, 18 October 2006 05:43:03 UTC