Desiderata

Let D be a set of datatypes, with, for each d ∈ D, a set of possible datavalues x:d. Let L be a set of labels. We consider finite labelled trees t:T with labelled, typed values x:d as leaves. Our trees have nodes of two flavours: ordered and unordered, and are subject to the restriction that the labels of the children of an unordered node must be distinct.

Values

Formally, a tree is constructed inductively as one of three cases

a leaf node	t = L(l, x:d)	where x:d is a typed data value
an ordered node	t = O(l, xs)	where xs is a list of trees
an unordered node	t = U(l, a)	where a: L ⇒ T is a finite partial map from labels to trees

In each case, the label l is called the rootlabel of the tree t, denoted l = #t.

Our model for access to the nodes allows selection of a child of an unordered node by label, and traversal of the children of an ordered node in order.

Given a suitable representation of the underlying datavalues, such a labelled tree can be represented by an xml document, with labels as tags, and an optional attribute "unordered".

<profile unordered="unordered">
  <name>
  </name>
  <institutes unordered="unordered">
    <ICCS /> <CISA /> <LFCS />
  </institutes>
  <children>
    <child>paula< /child>
    <child>maximillian< /child>
    <child>robin< /child>
  </children>
</profile>

We describe a system of types s:S for such trees, and corresponding schemata for the corresponding xml documents, together with orderings ≥, the "extension" orderings on trees and schemata, such that:

If t'≥t, t:s and s≥s' then t':s'

First, we define the extension ordering on trees inductively t ≥ t (reflexive) O(l, x::xs) ≥ O(l, y::ys) iff x ≥ y andalso O(l, xs) ≥ O(l, ys) U(l, a) ≥ U(l, b) iff ∀ m:L. a(m) ≥ b(m) (meaning that if b(m) is defined then so is a(m), and the ordering condition holds)

t:T

Typing

• L(l, x:d):L(l, d)
• O(l, []):O(l, d)
• O(l, h::xs):O(l, d) provided h:d andalso O(l, xs):O(l, d)
• U(l, af):U(l, df) provided ∀ m. af(m):df(m) (meaning that if af(m) is defined then so is df(m), and the typing condition holds)
• x:A(af) iff x:af(#x)

First we suppose given a partial order ≥ on D, such that if x:d and d ≥ d' then x:d'