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.


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

  • a leaf nodet = L(l, x:d) where x:d is a typed data value
    an ordered nodet = O(l, xs)where xs is a list of trees
    an unordered nodet = 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">
      <institutes unordered="unordered">
        <ICCS /> <CISA /> <LFCS />
        <child>paula< /child>
        <child>maximillian< /child>
        <child>robin< /child>

    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)



    • 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'

    No comments: