[relax-ng] Flaw of the RELAX NG specification

[MURATA Makoto <EB2M-MRT@asahi-net.or.jp>]

1. Problem statement

not(..) is used in (anyName 2), (nsName 2), (data 2), and 
(element).  However, not(...) is not formally defined. 

What is provable in a proof system?  A formular is provable if and
only if it is an axiom or it is a consequent of an inference rule
whose antecedents are provable.  However, we do not have any inference 
rules to prove not(....).  I think that this is a flaw of the specification 
(although it has no impacts on implementations).

I can think of two solutions.  One is to introduce extra predicates 
such as "notin" and provide inference rules for them.  These predicates 
and inference rules are uninteresting for implementors.  The other is 
to take the (naive) set theory for granted, and define the set of 
names represented by a nameclass as well as the set of strings permitted 
by <data> or <value>.  


2. Introduction of extra predicates

To give an idea of the second approach, here is a rough sketch 
for a rewrite of 6.1 by introducing "notin".

n notin nc
	asserts that name n is not a member of name class nc 

(anyName 2)

n notin nc
-------------------------------------------------------------------
n in <anyName> <except> nc </except> </anyName> 

(nsName 2)

name( u, ln ) notin nc 
------------------------------------------------------------------ 
name( u, ln ) in <nsName ns="u"> <except> nc </except> </nsName> 
 

(name 1)

------------------------------------------------------------------ 
name( u, ln ) in <name ns="u"> ln </name> 

(name 2)

ln1 != ln
------------------------------------------------------------------ 
name( u1, ln1 ) notin <name ns="u"> ln </name> 

(name 3)

u1 != u
------------------------------------------------------------------ 
name( u1, ln1 ) notin <name ns="u"> ln </name> 

 
(name choice 3)

n notin nc1    n notin nc2 
------------------------------------------------------------------
n notin <choice> nc1 nc2 </choice> 


Although this approach works for name classes, I do not think that it 
is a right solution.  I have tried this for <data> and <value> and 
the result is very complicated.


3. Set-theortic

In this approach, we take the naive set theory for granted.  
I think that this approach is natural and easy to understand.

3.1 Name classes (6.1)

Let U be the set of URIs, and LN be the set of local names.

The extension of a nameclass (denoted L(n), where n is a nameclass) is
inductively defined below:

	L(<anyName/>) = U \times LN

	L(<anyName> <except> nc </except> </anyName>) = 
		(U \times LN) \setminus L(nc)

	L(<nsName ns="u"/>) = {u} \times LN

	L(<nsName ns="u">  <except> nc </except> </nsName>) = 
		({u} \times LN) \setminus L(nc)

	L(<name ns="u"> ln </name>) = {u} \times {ln}

	L(<choice> nc1 nc2 </choice>) = L(nc1) \cup L(nc2)
 
In inference rules such as (attribute) or (element)
we write "n \in L(nc)" rather than "n in nc".

3.2 <data> and <value> (6.2.8)

In the para before 6.2.1, I would write "the sequence m of elements
and strings" rather than "the sequence of elements and strings m".

1) Notations

L(u,ln,params,cx) 

	The set of strings allowed by u,ln,params, and cx.

=[u,ln]

	An equivalence relation of string-context pairs that is defined 
	by a datatype (u, ln)

2) Axioms and inference rules

(value)

(s1, cx1) =[u,ln] (s2, context(u2, cx2))        s2 \in L(u1, ln, (), cx2) 
--------------------------------------------------------------------------
cx1 |- { }; s1 =~ <value datatypeLibrary="u1" type="ln"
                       ns="u2" [cx2]> s2 </value> 


(data 1)

L(<data datatypeLibrary="u" type="ln"> params </data>) = L(u,ln,params,cx) 

(data 2)

L(<data datatypeLibrary="u" type="ln"> params
                       <except> p </except> </data>)

 = L(u,ln,params,cx) \setminus L(p)


(data 3)

s \in L(<data datatypeLibrary="u" type="ln"> params </data>)
--------------------------------------------------------------
cx |- { }; s =~ <data datatypeLibrary="u" type="ln"> params </data> 
 
(data 4)

s \in 
 L(<data datatypeLibrary="u" type="ln"> params <except> p </except> </data> )
--------------------------------------------------------------
cx |- { }; s =~ <data datatypeLibrary="u" type="ln"> params <except> p </except> </data> 


3.3 String sequences (7.2)

Remove incorrectSchema()

For any <element> nc p </element> in a grammar, pattern 
p must have some content-type ct, i.e., p :c ct.

Cheers,

Makoto