Allen Brown (Microsoft) [Editor], David Ezell (Verifone), Matthew Fuchs (Stele), Dave Hollander (Contivo), Ashok Malhotra (Microsoft), Michael Sperberg-McQueen (W3C), Henry Thompson (U. Edinburgh)
For some time we have thought that basing the XML Schema (XS) type system on an underlying lattice would both help clarify a number of outstanding questions, e.g.
and help provide a framework for future possible developments in the XS type system (e.g. multiple inheritance, union types, etc.). The current formal descriptionfrml (FD) effort and its antecedents are suggestive of how such a lattice might be constructed. Indeed, lurking in FD's serialization of trees and forests are the essentials of such a lattice. Thus we have proposed that the near term efforts for FD development be focused on elucidating that lattice and evolving the proof rules to exploit it.
Heretofore FD has been narrowly cast as formalizing the validation of XML instances. Of course, that is only one reason for formalizing the XS type system. Because XS types (currently) have no denotationinfoset, it is very difficult to discuss how we might
These are all desirable things to characterize (and beyond validation), and
all need of an underlying formal model in order to characterize them. We have
created a lattice of (denotations of) types in order to undertake such
characterizations.
We have defined an algebraic lattice in which we believe such characterizations can be
given. The points in this lattice are sets of trees. Each XS type corresponds to
a point in the lattice. The partial order relation in the lattice allows us
to give an exact denotational characterization of the relationship between types
derived from one another by the existing extension and restriction XS type
constructions. This lattice is specifically intended to accommodate type models
inclusive of but not limited to that of XS. For example, this lattice, can easily accommodate the very general notions
of extension and restriction introduced by Andrew Layman in his XML Schema NG
GuideNG of 3
years ago. The meet and join operations in the lattice allow the discussion of
multiple inheritance, union types, list types and type inference. These topics
are of interest bot just within XS, but also to relate XS types to the type
models of programming languages and to the types in query languages.
We first define finite trees made up of partially orderedorder e-, a-, m-, and v-nodes. Trees (if non-empty) are rooted at e- or a-nodes. e- and a-nodes have names. m- and v-nodes have values An a-node has a (possibly empty) sequence of v-children. An e-node has a (possibly empty) set of distinctly named child a-nodes and either a (possibly empty) sequence of e and m children or a (possibly empty) sequence of v children. An e-node with only v children is said to be of simple content. Notionally, an e-node corresponds to an element, an a-node corresponds to an attribute, an m-nodeother corresponds to a mixed content item, and a v-node corresponds to a value from the set of all values over which XML Schema simple types range. A pre-extension is a set of such trees.
A tree t1 is an immediate thinning of a tree t2 if t1 is obtained from t2 by deleting an exterior (i.e. having no children) node from t2. A tree t1 is a thinning of a tree t2 if t1 can be obtained from t2 by a sequence of (0 or more) immediate thinnings. Note that a tree is a thinning of itself. A thinning t1 of t2 is proper unless t1 = t2. Finally, thinnings can ultimately result in the empty tree.
If P is a set of trees, P' is the thinning closure of P just in case P' is the smallest superset of P such that for every t in P', if t' is a thinning of t, then t' is in P'
Let P1 and P2 be pre-extensions. P1 is pre-extensionally less than P2 (P1 << P2) if either
Let ≤≤ be the reflexive closure of <<.
Let P3 be a minimal pre-extension (in the partial order ≤≤) such that P1 ≤≤ P3 and P2 ≤≤ P3. Let P4 be a maximal (in the partial order ≤≤) pre-extension such that P4 ≤≤ P1 and P4 ≤≤ P2. It can be demonstrated that P3 and P4 exist and are unique. P3 constitutes the join of P1 and P2. P4 constitutes the meet of P1 and P2. Note that the meet or join of a pre-extension with itself yields itself. If we take the set of all trees as the top of the lattice and the empty set as the bottom, these sets (which are pre-extensions) have the correct lattice-like behavior with respect to <<, meet and join.
Pre-extensions are not quite the right thing as we can distinguish two pre-extensions by the names of the root e- or a-nodes of their contained trees. We wish to smear out this distinction, looking only at the forests of children beneath root elements or attributes. We do so by saying that two pre-extensions are extensionally equivalent if for every tree in one pre-extension there is a tree in the other pre-extension that differs only by the name on its root e- or a-node. An extensionext, then is an equivalence class of pre-extensions. Taking meet, join and << modulo this equivalence relation yields new meet and join operators (٨ and ٧) and partial order (<). Note that the empty set continues to be the bottom of this new lattice. The top of the lattice corresponds to anyType. The equivalence class of maximal (in the lattice of pre-extensions) pre-extensions containing only a-rooted trees (or e-rooted trees with only v children) corresponds to anySimpleType.
Semantic extensions as defined actually permit more kinds of trees than permitted by XML Schema (or XML itself, for that matter). That need not worry us as there are extensions in the lattice corresponding exactly to sets of XML trees, in general, and those expressible by XML schemas, in particular. (That the lattice is vastly more expressive of sets of trees follows from the fact that the cardinality of the lattice is certainly not countable. Strictly speaking, the lattice as presented is not even a set.) Another observation to be made is that subtyping by derivation extension will correspond to ascending the lattice we have defined while subtyping by restriction will correspond to descending. Note however, that the extensions corresponding to lists and unions of simple types are above (greater in the partial order) the extensions corresponding to the types on which those lists and unions are based. Thus enlistments and unions of types on this account will be derivation extensions and not derivation restrictions. Furthermore, the lattice of semantic extensions has correspondents not only for the enlistment and union of simple types, but for any types whatsoever!
XML Schema defines a structure called a complex type definition schema component. For our purposes here it suffices to augment this structure with at least one more "property"–its semantic extension. Call this augmented structure a complex type description component (or just complex type description). We also change the constraints on the other properties of a complex type description from those currently prevailing in a complex type definition. The current constraints on the interrelation among properties has to do with the fact that XML Schema types largely define their semantic extensions constructively by derivation. (The principal exceptions are anyType and anySimpleType.) By virtue of the a priori lattice of extensions introduced above, we need not require that an XS type have a constructive relationshipcons to any other type, but only that the type definition extension property of its type definition schema component be well defined. Hence, properties like {base type definition}, {derivation method}, {name}, {final}, {abstract}, etc. are optional. Indeed, as a consequence of our experience with FD, we might insist that every constructive type have a name (whether it is locally defined or not) and simply make locally defined types be final, rendering them unmentionable in the construction of other types. Finally, the type description component constitutes the intensional semantics of the XS complex type which it names.
Now we are in a position to say what the relationship is between the named types of XML Schema and the purely extensional types discussed at various times in XML Query. The named types are the types that we termed constructive above. The extensional types correspond to the complex type descriptions which omit all the constructive properties. That is, the only description of such a type is its extension. In fact, we could posit a type description corresponding to every point of the lattice of extensions. Once we have that in place we can impose a lattice structure on the set of XS complex type descriptions. There are many ways that this can be carried out. However, in none of the ways that come immediately to mind does the "sub type of" relationship have a simple correspondence to the partial order on the lattice. (Indeed, this is as it should be since subtyping and subsetting have no compelling relationship to one another.) In fact, depending on exactly how we constructed the lattice of types the named types anyType and anySimpleType may or may not be ordered with respect to one another (in the lattice) and may or may not be constructively related to one another.
One last observation. We made the empty set the bottom of the lattice of extensions. There is actually another candidate for bottom, namely the set consisting only of the empty tree (which to the best of my knowledge has no correspondent in the XML infoset). Apart from being an alternative basis for the bottom of the lattice, the empty tree is also an interesting candidate for the role of the null value.
How do the partial order, meet and join in the lattice of pre-extensions work?
If we write an e-node with its name as <e n="...">...</e> and an a-node with its name as <a n="...">...</a> and m- and v -nodes with their values as <m v="..."/>, <v v="..."/>, then the set of trees we are talking about maps one to one with the set of XML documents valid according to the DTD
<!DOCTYPE d [
<!ELEMENT t (e|a|EMPTY)>
<!ATTLIST e n NMTOKEN #REQUIRED>
<!ATTLIST a n NMTOKEN #REQUIRED>
<!ATTLIST m v CDATA #REQUIRED>
<!ATTLIST v v CDATA #REQUIRED>
<!ELEMENT e (a*, (v* | (m | e)*))>
<!ELEMENT a (v*)>
<!ELEMENT m EMPTY >
<!ELEMENT v EMPTY >
]>
This DTD offers a very good approximation to the mathematical trees introduced above. (We will omit the t, thinking of e and a as in the substitution group of t.)
Let there be four trees named A, B, C, and D, such that B and C each have at least two edge nodes. For example:
A = <e n="A"/>
B = <e n="B"><a n="Ba"/><a n="Bb"/></e>
B' = <e n="B"><a n="Ba"/></e>
B'' = <e n="B"><a n="Bb"/></e>
B''' = <e n="B"/>
C = <e n="C"><a n="Ca"/><a n="Cb"/></e>
C' = <e n="C"><a n="Ca"/></e>
C'' = <e n="C"><a n="Cb"/></e>
C''' = <e n="C"/>
D = <e n="D"/>
€ = "the empty tree"
Let P1 = {A,B,C}, P2 = {B,C,D}. What is P1 meet P2? By the definition given above, if P = {B,C}, P << P1 and P << P2. So the meet in question is at least P. Is there a P' such that P << P' << P1 and P << P' << P2? Let P' = {B,B',B'',B''',C,C',C'',C''',€}, the flattening closure of P. So the answer is affirmative. Is there a P'' such that P << P'' << P1 and P << P'' << P2? For such a P'' to exist it would have to include either a thinning of A and a thinning of B. But the only tree that can be both a thinning of A and a thinning of B is € . Therefore P'' = P1 meet P2.
Similarly, {A,B,C} << {A,B,C,D} and {B,C,D} << {A,B,C,D}. To satisfy P1 << P << {A,B,C,D} and P2 << P << {A,B,C,D}, P would have to contain thinnings (distinct from €) of both A and D. But this forces P to be incomparable both to P1 and P2. So P must be P1 join P2.
What do simple types look like?
Let's first consider the trees generated by.
<e n="nam"><v v="int"/></e>
<a n="nam"><v v="int"/></a>
In the trees above nam ranges over the domain of all names and int ranges over all the integers in the domain of values. The set of trees generated by varying nam and int constitute a pre-extension for integers. When passing from pre-extensions to extensions the e-and a-nodes are conflated as are the names on such nodes. Were we to construct the thinning closure of the integers (as a pre-extension), we would add to the above
<e n="nam"></e>
<a n="nam"></a>
€
On this account of the integers (and of scalar simple types more generally), the integers are never mentioned alone but only in the context of a reference from another node. Following the Lisp tradition, programming languages with references would term this kind of representation of the integers as "boxed". With some additional complexity we could represent un-boxed simple values and sequences thereof and may eventually choose to do so.
Consider the following schema fragments:
<xsd:simpleType name="onetwothree">
<xsd:annotation>
<xsd:documentation>A type for counting to three.</xsd:documentation>
</xsd:annotation>
<xsd:restriction base="xsd:integer">
<xsd:minInclusive value="1"/>
<xsd:maxInclusive value="3"/>
</xsd:restriction>
</xsd:simpleType>
<xsd:simpleType name="three-to-five">
<xsd:annotation>
<xsd:documentation>A very small integer-based type.</xsd:documentation>
</xsd:annotation>
<xsd:restriction base="xsd:integer">
<xsd:minInclusive value="3"/>
<xsd:maxInclusive value="5"/>
</xsd:restriction>
</xsd:simpleType>
In the notation of the DTD above the following constitutes a pre-extension of the XS type onetwothree:
<e n="A"><v v="1"/></e>
<e n="A"><v v="2"/></e>
<e n="A"><v v="3"/></e>
<e n="B"><v v="1"/></e>
<e n="B"><v v="2"/></e>
<e n="B"><v v="3"/></e>
<e n="C"><v v="1"/></e>
<e n="C"><v v="2"/></e>
<e n="C"><v v="3"/></e>
and so on: three trees for each possible generic identifier, as well as a similarly generated set of trees rooted in a-nodes:
<a n="A"><v v="1"/></a>
<a n="A"><v v="2"/></a>
<a n="A"><v v="3"/></a>
<a n="B"><v v="1"/></a>
<a n="B"><v v="2"/></a>
<a n="B"><v v="3"/></a>
<a n="C"><v v="1"/></a>
<a n="C"><v v="2"/></a>
<a n="C"><v v="3"/></a>
and so on. Type 'three-to-five' would have a similar set of trees in any of its pre-extensions.
Using the notional "substitution group" of t we mentioned above, we can succinctly denote the extensions. We anonymize and conflate e- and a-nodes by replacing e- and a-elements with t-elements. The extensions of onetwothree and three-to-five are thus represented as:
<t><v v="1"/></t>
<t><v v="2"/></t>
<t><v v="3"/></t>
and
<t><v v="3"/></t>
<t><v v="4"/></t>
<t><v v="5"/></t>
Finally, in the lattice of extensions the thinning closure of the extension of the type onetwothree is
{<t><v v="1"/></t>,<t><v v="2"/></t>,<t><v v="3"/></t>,<t></t>,€}.
How does union work?
From the earlier discussion of the meet of two sets of trees, it should be apparent that the lattice join is just a set union. Thus it is entirely natural to consider the extension of the union of two XS types to be just the join of their respective extensions. In the case of taking the union of onetwothree and three-to-five, the join is
<t><v v="1"/></t>
<t><v v="2"/></t>
<t><v v="3"/></t>
<t><v v="4"/></t>
<t><v v="5"/></t>
Note that by design the extension (unlike the PSVI) does not distinguish the 3 that came from onetwothree from that coming from three-to-five.
While we have presented the concrete example unioning simple types, joins exist, of course, for any pairs of sets of trees whatsoever. Indeed, they exist for any finite set of sets of trees. From the extensional perspective we can therefore define the extension for the union of any XS types (simple, complex, or combinations thereof). Extensionally we may explain the extension of anySimpleType to be the join of the extensions of the built-in primitive datatypes. Similarly, if we wanted a generic numerical type, its extension would obviously be the join over the extensions of the existing numerical types.
How does list work?
Were we to define a simple type consisting of lists (possibly empty) of lists of items of type onetwothree, its extension would be the obvious completion of the following:
<t></t> (which is not the same as €)
<t><v v="1"/></t>
<t><v v="2"/></t>
<t><v v="3"/></t><t><v v="1"/><v v="1"/></t>
<t><v v="1"/><v v="2"/></t>
<t><v v="1"/><v v="3"/></t>
<t><v v="2"/><v v="1"/></t>
<t><v v="2"/><v v="2"/></t>
<t><v v="2"/><v v="3"/></t>
<t><v v="3"/><v v="1"/></t>
<t><v v="3"/><v v="2"/></t>
<t><v v="3"/><v v="3"/></t>
...
Properly speaking what we have here are really sequences rather than
lists since they cannot be nested. Also, the lists in question are sequences
of boxed values. Again, since our goal here is to model mathematical
accessibility rather than storage accessibility, this observation is of no
essential consequence.
How does facet restriction work?
From the extensional perspective (derivation by) restriction for the simple types, just as is the case for the complex types, corresponds to descending the lattice of semantical extensions. As we note elsewhere, list and union constructors on simple type should, from the point of view of extensional semantics, be considered a form of derivation by extension. What's interesting about the XS simple types is that the relationship between the extensional and intensional aspects of the (currrent) XS simple types is much simpler than that for the XS complex types.
In the preliminaries above we considered the complex type description component as the carrier for both the extensional and intensional aspects of XS complex types. We posit an analogous simple type description component for XS simple types augmented (from the simple type definition component), once again with an extension property. We should also add back a lexical facet, where this facet is now a set of functions from a set of lexical spaces into the extension of the simple type. We can reconstruct facets such that every facet is a set. Moreover, derivation by restriction will always result in a simple type each of whose facets is a (possibly improper) subset of the analogous facet of its supertype.
What do complex types look like?
Consider a simple subset of HTML, with elements UL, OL, LI, I, B, EM, and complex types LISTTYPE and PHRASETYPE, with UL and OL declared as having LISTTYPE and the other element types having PHRASETYPE. LISTTYPE is declared as being made up of a list of PHRASETYPES. We now consider the thinning closure of the semantical extension of LISTTYPE. This set includes the trees.
<t><e n="li"/></t>
<t><e n="li"/><e n="li"/></t>
<t><e n="li"/><e n="li"/><e n="li"/></t>
as well as the trees
<t>
<e n="li"><m v="this is a list item"/></e>
<e n="li"><m v="this is a second list item"/></e>
<e n="li"><m v="this item has a "/>
<e n="ul">
<e n="li"><m v="Lorem ipsum dolor sit amet"/></e>
<e n="li"><m v="consetetur sadipscing elitr"/></e>
<e n="li">
<m v="sed diam nonumy eirmod tempor invidunt ut labore
et dolore magna aliquyam erat"/>
</e>
</e>
<m v="nested list "/>
</e>
</t>
as well as trees with nested list items ...
The trees in the semantical extension of LISTTYPE do not just include the LI children, but the entirety of the LI-rooted subtrees. Thus the extensions of XS types should be apprehended as "deep" rather than the "shallow" trees that a content model might suggest. Put another way, the extension explicitly represents all of the valid document sub-trees sanctioned by a particular XS type. In that regard the types are not actually sets of trees at all but forests. This is visible in the fact that in our notation for the trees in a semantic extension, every member of the extension is embraced by a t-element.
While the semantical extensions of XS types reflect only the valid trees, most extensions correspond to no XS type whatsoever and per force represent invalid trees. In fact, since we have been very open minded about the permissible sets of trees, we have not even required that they be recursively enumerable. Hence there are extensions which cannot correspond to any validation process. Note that wildcards are dealt with gratis as there are always extensions in which there are subtrees corresponding to every possible combination of wild card namespaces and processing. That said, extensions of XS types are reflective of the validation process only insofar as such extensions contain the trees corresponding to every valid document fragment rooted in that type. There is no reflection of lax or strict processing. Nor is there any representation of invalidity. As all of these notions are intensional, there is no reason for them to surface in the lattice of extensions.
How does complex type (derivation by) extension work?
Let T1 and T2 be XS complex types whose semantic extensions we denote as [T1] and [T2] respectively. Suppose T2 is a derivation extension of T1. It is therefore the case that [T1] < [T2]. (Recall that < is the lifting of the << relation from the lattice of pre-extensions to the lattice of extensions.) Often, trees in [T1] will be thinnings (of a highly stylized sort) of trees in [T2]. There are, of course, many semantical extensions having no corresponding XS type whatsoever. Moreover, there are pairs of semantical extensions, ordered by <, each corresponding to (many) XS types, and yet having no corresponding pair of XS types one of which is a derivation extension with respect to the other. This means that the lattice of extensions is strictly more powerful in its ideas of derivation extension (and dually, derivation restriction) than is XS. Finally, since derivation extension (restriction) takes one up (down) the lattice of semantical extensions, the simple types (semantically speaking) are no less extensible than are the complex ones. In fact, in that lattice the semantical extensions of the types created by the union and list derivations above are up the lattice from the semantical extensions of their underlying simple types.one
How does complex type (derivation by) restriction work?
We emphasize that from the lattice point of view derivation restriction and derivation extension are duals. That this is not so in XS is an intensional feature of the particular type constructors that have been defined. That constructor, in effect, allows one to delete alternatives from what amounts to a union type. One can imagine a constructor which allowed one to introduce alternatives, thereby creating the inverse of the current restriction constructor. Dual to the extension constructor one could imagine a "retraction" constructor that removed the right-most element child or any of the attribute children. Any of these notions is readily mapped onto the lattice.
What goes at the bottom of the lattice?
Among the pre-extensions, every set of trees P is either equal to the empty set, Ø, or Ø << P. Also among the non-empty pre-extensions, P, every P is either equal to {€} or {€} << P. Moreover, both Ø and {€} are identity elements with respect to join. So both Ø and {€} would seem like plausible candidates for the bottom of a lattice. The main strike against {€} in this regard is that XS types include ones whose natural semantic extension would be the empty set. Moreover, there is no empty tree in XML. So there seems to be no compelling reason to perform unnatural acts. However, since € has such nice properties in the greater scheme of things, some consideration should be given to incorporating it in the infoset if not XML itself.
Minutes of face-to-face meeting 25-26 February 2002
David Ezell and C.
M. Sperberg-McQueen
XML Schema NG Guide
Andrew Layman