RELAX NG Formal Semantics

Notation

Notation Meaning
s ranges over strings; a string is a sequence of zero or more Unicode scalar values
"" represents an empty string
split( s ) returns a sequence of strings one for each whitespace delimited token of s
ln ranges over local names (NCNames, names without prefixes)
u ranges over URIs
name( u, ln ) constructs an (expanded) name with URI u and local name ln
n ranges over expanded names
nc ranges over name classes
n in nc asserts that name n is a member of name class nc
attribute( n, s ) constructs an attribute with name n and value s
a ranges over bags (unordered collections) of attributes; a bag with a single member is considered the same as that member
{ } represents an empty bag
a1 + a2 represents the bag union of a1 and a2 (the number of occurrences of any member of a1 + a2 is the sum of the number of its occurrences in a1 and a2)
ns ranges over namespace maps; a namespace map is a mapping from namespace prefixes to URIs
ns() represents an empty namespace map
params ranges over sequences of parameters
datatypeAllows(u, ln, params, s, ns) asserts that in the datatype library identified by URI u, the string s interpreted in the context of the namespace map ns is a legal value of datatype ln with parameters params
datatypeEqual(u, ln, s1, ns1, s2, ns2) asserts that in the datatype library identified by URI u, string s1 interpreted in the context of the namespace map ns1 represents the same value of the datatype ln as the string s2 interpreted in the context of ns2
m ranges over sequences of elements and strings; a sequence with a single member is considered the same as that member
normalized(m) asserts that the mixed sequence m is normalized: it does not contain any member that is an empty string, nor does it contain two consecutive members that are both strings
element( n, ns, a, m ) constructs an element with name n, namespace map ns, attributes a and mixed sequence m as children
element ranges over elements
m1, m2 represents the concatenation of the sequences m1 and m2
( ) represents an empty sequence
v ranges over strings and the empty sequence; this is a subset of the range of m
toString( v ) returns an empty string if v is the empty sequence and otherwise returns v
stripSpace( m ) returns the sequence m after removing any member that is a string consisting entirely of whitespace
m1 interleaves m2; m3 asserts that m1 is an interleaving of m2 and m3
key( ln1, u, ln2, s, ns ) constructs a key in symbol space ln1 with datatype ln2 in the datatype library u with lexical value s interpreted with respect to namespace map ns
k ranges over bags of keys
keyConflict(k) asserts that there are conflicting keys in the unordered collection of keys k
k1 subset k2 asserts that k1 is a subset of k2
keyref( ln1, u, ln2, s, ns ) constructs a key reference in symbol space ln1 with datatype ln2 in the datatype library u with lexical value s interpreted with respect to namespace map ns
kr ranges over bags of key references
keyComplete(k, kr) asserts that the collection of keys k has a key that satisfies every key reference in the collection of key references kr
p ranges over patterns
{ns} within the start-tag of a pattern refers to the namespace map of the pattern element
valid(element, p) asserts that the element element is valid with respect to the pattern p
env() constructs an empty environment
defs ranges over sequences of definitions
env( defs, E ) constructs an environment with definitions defs and parent environment E
E ranges over environments
E.ln = p asserts that in environment E, local name ln is bound to pattern p
E; ns |- a; m =~ p => k; kr asserts that in the context of the environment E and namespace map ns, the attributes a and the sequence of elements and strings m matches the pattern p generating the collection of keys k and key references kr

Inference Rules

(valid)
env(); ns() |- { }; element =~ p => k; kr ����keyComplete(k, kr) ����not(keyConflict(k))

valid(element, p)
(group)
E; ns |- a1; m1 =~ p1 => k1; kr1 ����E; ns |- a2; m2 =~ p2 => k2; kr2

E; ns |- a1 + a2; m1, m2 =~ <group> p1 p2 </group> => k1 + k2; kr1 + kr2
(oneOrMore 1)
E; ns |- a; m =~ p => k; kr

E; ns |- a; m =~ <oneOrMore> p </oneOrMore> => k; kr
(oneOrMore 2)
E; ns |- a1; m1 =~ p => k1; kr1 ����E; ns |- a2; m2 =~ <oneOrMore> p </oneOrMore> => k2; kr2

E; ns |- a1 + a2; m1, m2 =~ <oneOrMore> p </oneOrMore> => k1 + k2; kr1 + kr2
(interleave 1)
E; ns |- a1; m1 =~ p1 => k1; kr1 ����E; ns |- a2; m2 =~ p2 => k2; kr2 ����m3 interleaves m1; m2

E; ns |- a1 + a2; m3 =~ <interleave> p1 p2 </interleave> => k1 + k2; kr1 + kr2
(interleave 2)
( ) interleaves ( ); ( )
(interleave 3)
m1 interleaves m2; m3

m4, m1 interleaves m4, m2; m3
(interleave 4)
m1 interleaves m2; m3

m4, m1 interleaves m2; m4, m3
(choice 1)
E; ns |- a; m =~ p1 => k; kr

E; ns |- a; m =~ <choice> p1 p2 </choice> => k; kr
(choice 2)
E; ns |- a; m =~ p2 => k; kr

E; ns |- a; m =~ <choice> p1 p2 </choice> => k; kr
(element)
E; ns1 |- a; stripSpace( m ) =~ p => k; kr ����n in nc ����normalized(m)

E; ns2 |- { }; element( n, ns1, a, m ) =~ <element> nc p </element> => k; kr
(attribute)
E; ns |- { }; v =~ p => k; kr ����n in nc

E; ns |- attribute( n, toString( v ) ); ( ) =~ <attribute> nc p </attribute> => k; kr
(empty)
E; ns |- { }; ( ) =~ <empty/> => { }; { }
(text 1)
E; ns |- { }; s =~ <text/> => { }; { }
(text 2)
E; ns |- { }; m =~ <text/> => { }; { }

E; ns |- { }; m, s =~ <text/> => { }; { }
(empty string)
E; ns |- { }; "" =~ p => k; kr

E; ns |- { }; ( ) =~ p => k; kr
(value)
datatypeEqual(u, ln, s1, ns1, s2, ns2)

E; ns1 |- { }; s1 =~ <value {ns2} type="ln" ns="u"> s2 </value> => { }; { }
(data 1)
datatypeAllows(u, ln, params, s, ns)

E; ns |- { }; s =~ <data type="ln" datatypeLibrary="u"> params </data> => { }; { }
(data 2)
datatypeAllows(u, ln2, params, s, ns)

E; ns |- { }; s =~ <data key="ln1" type="ln2" datatypeLibrary="u"> params </data> => key( ln1, u, ln2, s, ns ); { }
(data 3)
datatypeAllows(u, ln2, params, s, ns)

E; ns |- { }; s =~ <data keyRef="ln1" type="ln2" datatypeLibrary="u"> params </data> => { }; keyref( ln1, u, ln2, s, ns )
(data 4)
datatypeAllows(u, ln2, params, s, ns)

E; ns |- { }; s =~ <data key="ln1" keyRef="ln2" type="ln3" datatypeLibrary="u"> params </data> => key( ln1, u, ln3, s, ns ); keyref( ln2, u, ln3, s, ns )
(list)
E; ns |- { }; split( s ) =~ p => k; kr

E; ns |- { }; s =~ <list> p </list> => k; kr
(grammar)
env( defs, E ); ns |- a; m =~ p => k; kr

E; ns |- a; m =~ <grammar> <start> p </start> defs </grammar> => k; kr
(define)
env( defs1 <define name="ln"> p </define> defs2, E ).ln = p
(ref)
E; ns |- a; m =~ p => k; kr ����E.ln = p

E; ns |- a; m =~ <ref name="ln"/> => k; kr
(parentRef)
E; ns |- a; m =~ p => k; kr ����E.ln = p

env( defs, E ); ns |- a; m =~ <parentRef name="ln"/> => k; kr
(anyName)
n in <anyName/>
(name)
name( u, ln ) in <name ns="u"> ln </name>
(namespaceName)
name( u, ln ) in <nsName ns="u"/>
(name choice 1)
n in nc1

n in <choice> nc1 nc2 </choice>
(name choice 2)
n in nc2

n in <choice> nc1 nc2 </choice>
(difference)
n in nc1 ����not(n in nc2)

n in <difference> nc1 nc2 </difference>
(key)
datatypeEqual(u, ln2, s1, ns1, s2, ns2) ����key( ln1, u, ln2, s1, ns1 ) + key( ln1, u, ln2, s2, ns2 ) subset k

keyConflict(k)
(keyref 1)
keyComplete(k + key( ln1, u, ln2, s1, ns1 ), kr) ����datatypeEqual(u, ln2, s1, ns1, s2, ns2)

keyComplete(k + key( ln1, u, ln2, s1, ns1 ), kr + keyref( ln1, u, ln2, s2, ns2 ))
(keyref 2)
keyComplete(k, { })