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 |

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'

## No comments:

Post a Comment