Re: [relax-ng] Flaw of the RELAX NG specification

[James Clark <jjc@jclark.com>]

Murata-san and I discussed this offline, and out tentative conclusion is to 
leave the inference rules as they are, but to document the meaning of not() 
and describe how our formalism differs from a true proof system.  The 
reason is that although it would be better from a mathematical perspective 
to avoid the use of not(), using not() does not cause any ambiguity or 
undefinedness in the semantics of RELAX NG (once we explain what it means), 
and the spec will be easier to understand with not().

--On 02 November 2001 21:39 +0900 MURATA Makoto <EB2M-MRT@asahi-net.or.jp> 
wrote:

> 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
>
> ----------------------------------------------------------------
> To subscribe or unsubscribe from this elist use the subscription
> manager: <http://lists.oasis-open.org/ob/adm.pl>
>
>
>