From: Neva Cherniavsky (nchernia@cs.washington.edu)
Date: Wed Apr 14 2004 - 07:48:55 PDT
This paper describes a model for the core features of XML. XML is an
external format for representing data that is neither self-describing nor
round-tripping. The authors fix this through their model, for which they
prove a number of properties culminating in the Validation Theorem and the
Roundtripping corollaries. Essentially, validation matches an element to a
type. It is akin to compilation in other languages.
Validation is important because we want to ensure that our data is of the
right form. There is structure to the elements of XML and validation
ensures we are matching the proper structure for each element.
Subtyping and restriction are very similar. Usually in programming
languages, an element that is subtyped from another shares the same
initial structure and also adds on to that structure. In this model, the
restricted class is not allowed to add on elements; the parent class
contains all the elements allowed by the children. Extension is also
similar to inheritance, particularly multiple inheritance, which is not
implemented in the commonly used programming languages. One big
difference is in XQuery, type checking requires that one knows all the
types that can be derived from a given type, whereas in other programming
languages, one can type check a class without knowing all its subclasses.
The parent class in XQuery is the union of all its children, which leads
to unusual behavior.
The most important practical implication of the Validation Theorem was to
add pure named typing to XQuery. Pure named typing simplifies the formal
semantics of the language.
I liked this paper a lot; the theory was sound, well-written, and easy to
understand, and the authors have helped bring formal semantics back into
the fold with regard to XML.
This archive was generated by hypermail 2.1.6 : Wed Apr 14 2004 - 07:48:57 PDT