RELAX NG Type Lattices, draft 0

[John Cowan <cowan@mercury.ccil.org>]

This is a sketch of a set of annotations which allow one or more RNG
schemas to define a type lattice based on RNG patterns.

First, some definitions.

An instance I of the RNG data model *matches* an RNG pattern P iff I,
suitably embedded in a document, would be valid with respect to P.
We write I ~ P.

A pattern P is a *subpattern* of a pattern P' iff for every instance I
of the data model, if I ~ P then I ~ P'.  We write P <= P'.

Patterns P and P' are *equivalent* iff P <= P' and P' <= P.  We write
P == P'.

The *name* N(P) of a pattern P is an ordered pair consisting of a
namespace name (URI) and a local part (NCName).  Not all patterns
have names.  We write N?(P) if a pattern has a name.

We write S for an RNG schema.  We write SS for a set of RNG schemas.
We write PS(SS) for the set of patterns contained within each member
of SS.  Each pattern-type element constitutes a distinct member of PS(SS).

A *lattice specification* LS is a set consisting of a set of schemas
SS(LS) and a set of assertions AS(LS) of the form "P <= P'", where
for each P and P', both P and P' are members of PS(SS(LS)) and N?(P)
and N?(P').

A lattice specification LS is *coherent* iff each assertion in AS(LS)
is true.

A lattice specification LS is *provably coherent* by a validator V iff
V can prove that each assertion in AS(LS) is true.

A lattice specification is *provably incoherent* by a validator V iff
V can prove that at least one assertion in AS(S) is false.

A validator V *conforms* iff V can prove all assertions (within the'
obvious limits of space and time) that do not involve patterns that
contain references to RNG datatypes other than those in the default
datatype library.

Syntax:

The namespace "http://relaxng.org/ns/lattice", usually designated by
the prefix lat, is used for the annotations in this specification.

The attribute lat:ns is used to specify a namespace.  It may appear on
any RNG element and is inherited, like the RNG ns attribute.

The attribute lat:name is used to specify the name of a pattern.  If its
value is an NCName, then the specified or inherited value of the ns
attribute specifies the namespace name part of the name.  Otherwise,
the value is a QName.

The attribute lat:extends has a NCName or QName value and uses the lat:ns
attribute in the former case to specify a namespace name.  The presence of
a lat:extends attribute on a pattern element indicates that the pattern
whose name is given by the attribute is a subpattern of the pattern with
the lat:extends attribute.

The attribute lat:restricts has a NCName or QName value and uses
the lat:ns attribute in the former case to specify a namespace name.
The presence of a lat:restricts attribute on a pattern element indicates
that the pattern with the lat:restricts attribute is a subpattern of
the pattern whose name is given by the attribute.  pattern with the
lat:extends attribute.

A validator accepts a set of schemas and uses the above attributes
to deduce a lattice specification LS.  It then reports whether LS is
provably coherent, provably incoherent, or neither.

Comments?


-- 
First known example of political correctness:   John Cowan
"After Nurhachi had united all the other        http://www.reutershealth.com
Jurchen tribes under the leadership of the      http://www.ccil.org/~cowan
Manchus, his successor Abahai (1592-1643)       jcowan@reutershealth.com
issued an order that the name Jurchen should       --S. Robert Ramsey,
be banned, and from then on, they were all         _The Languages of China_
to be called Manchus."