Re: Example [Was: Two things to strengthen the spec]

[Murata Makoto <mura034@attglobal.net>]

I revised my example and sketched subsections of Sections 2, 3, 4, 6, 
and 7.  Before XMLizing these subsections, please let me know if 
they deserve the length.

<section>
<title>Example</title>

<para>Throughout this specification, we use the following XML document 
as an example.</para>

<programlisting>
<?xml version="1.0"?>
<foo xmlns=""
   ><pre1:bar1 xmlns:pre1="http://n1"
  /><pre2:bar2 xmlns:pre2="http://n2"
  /></foo>

Note that the root element has two child elements but has no child
strings.

This document is represented by an element foo containing two child
elements.

We use the following notation:

(...)
  represents a set

{...}
  rrepresents a sequence

prefix ->  uri
  represents a prefix-namespace pair, or the default 
  namespace when the prefix is the empty string.

element(n,cx, a, m)
  an element with name n, context cx, attributes a and mixed 
  sequence m as children

context(b, pair1, pair2, ....)
  a context with base uri b and a mapping given by 
  pair1, pair2, ....

Let cx0 be the context for the root element.  We assume that uri1 is
the base URI of this document.  Then, 

	cx0 = context(uri1, ""->"")

The root element e0 is represented by

	element(name("", foo), cx0, {}, {e1, e2}) 

where e1 and e2 represent the first and second child element,
respectively.

Let cx1 and cx2 be contexts of e1 and e2.  Then, 

	cx1 = context(uri1, "" -> "", pre1 -> "http://n1")

and

	cx2 = context(uri1, "" -> "", pre2 -> "http://n2").


e1 is represented by by

	element(name("http://n1", bar1), cx1, {}, {})

and e2 is represented by by

	element(name("http://n2", bar2), cx2, {}, {})


3.2 Example

Here is an example schema.

ex10.rng

4.20 Example

We consider how a schema in 3.2 is normalized, but we use the XML
instance syntax for convenience.  We assume that unprefixed 
tags are in the namespace "http://relaxng.org/ns/structure/0.9".

4.20.1 Result of 4.1

ex11.rng

4.20.2 Result of 4.2

<element name="foo" ns=""
   ><element ns="http://n1" name="bar1"
      ><empty
  /></element
   ><element ns="http://n2" name="bar2"
      ><empty
  /></element
></element>


4.20.3 Result of 4.3, 4.4, 4.5, and 4.6

These steps do not apply to this example.

4.20.4 Result of 4.7

<element ns=""
  ><name>foo</name
   ><element ns="http://n1"
      ><name>bar1</name
      ><empty
  /></element
   ><element ns="http://n2"
      ><name>bar2</name
      ><empty
  /></element
></element>


4.20.5 Result of 4.8

<element
  ><name ns="">foo</name
   ><element
      ><name ns="http://n1">bar1</name
      ><empty
  /></element
   ><element
      ><name ns="http://n2">bar2</name
      ><empty
  /></element
></element>


4.20.6 Result of 4.9 and 4.10

These steps do not apply to this example.

4.20.7 Result of 4.11

<element
  ><name ns="">foo</name
  ><group
    ><element
      ><name ns="http://n1">bar1</name
      ><empty
   /></element
    ><element
      ><name ns="http://n2">bar2</name
      ><empty
   /></element
  ></group
></element>


4.20.8 Result of 4.12, 4.13, 4.14, and 4.15

These steps do not apply to this example.

4.20.9 Result of 4.16

<grammar
  ><start
    ><element
      ><name ns="">foo</name
      ><group
        ><element
          ><name ns="http://n1">bar1</name
          ><empty
       /></element
        ><element
          ><name ns="http://n2">bar2</name
          ><empty
       /></element
      ></group
    ></element
  ></start
></grammar>


4.20.10 Result of 4.17

<grammar
  ><start
    ><element
      ><name ns="">foo</name
      ><group
        ><ref name="bar1"
       /><ref name="bar2"
      /></group
    ></element
  ></start

  ><define name="bar1"
    ><element
      ><name ns="http://n1">bar1</name
      ><empty
   /></element
  ></define

  ><define name="bar2"
    ><element
      ><name ns="http://n2">bar2</name
      ><empty
   /></element
  ></define
></grammar>

4.20.11 Result of 4.18 and 4.19

These steps do not apply to this example.

6.5 Example

Let nameclass nc1 = <name ns="http://n1">bar1</name> and 
nameclass nc2 = <name ns="http://n2">bar2</name>.

Then, by the inference rule (name) in 6.1, we have

	name("http://n1", "bar1") in nc1

and 
	name("http://n2", "bar2") in nc2 .

By the inference rule (empty) in 6.2.3, we have

	cx1 |= {};() = <empty/> => {};{}

and 

	cx2 |= {};() = <empty/> => {};{}

Since 

	deref(bar1) = 
	  <element>
	    <name ns="http://n1">bar1</name>
	    <empty/>
	  </element>

we have

	cx0 |-   {}; e1 =~ <ref name="bar1"/> => {}; {}

by applying the inference rule (element) in 6.2.8.   Note that 
we have chosen cx0, since any context is allowed.

Likewise, we have 

	cx0 |-   {}; e2 =~ <ref name="bar2"/>  => {}; {}

By the inference rule (group) in 6.2.1, we have 

	cx0 |-   {}; (e1, e2)
	           =~ <group><ref name="bar1"/><ref name="bar2"/></group>
			=> {}; {}

Since

deref(foo) = <element><name>foo</name>
              <group>
                <ref name="bar1"/>
                <ref name="bar2"/>
              </group>
             </element>
,

we have 

	cx3 |- {}; element(name("", foo), cx0, {}, {e1, e2}) =~ 
                     <ref name="foo"/> => {}; {}

by the the inference rule (element) in 6.2.8 again.  Here
cx3 is an arbitrary context.

Finally, since start() = <ref name="foo"/>, we can apply the 
inference rule (valid) in 6.4 and obtain

	valid(e0)


7.5 Example

Observe that the normalized schema in 4.20 satisfies all 
restrictions in 7.1 thorough 7.4.


----
Murata Makoto  mura034@attglobal.net