[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [Elist Home]
Subject: [relax-ng] Flaw of the RELAX NG specification
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
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [Elist Home]
Powered by eList eXpress LLC