The extensible markup language XML is the current standard format for exchanging structured data. Its widespread use has initiated lots of work to support processing of XML on many different levels: customized query languages for XML, such as XQuery, transformation languages like XSLT, and programming language support either in the form of special purpose languages like XDuce, or of binding facilities for mainstream programming languages like JAXB.
A central problem in XML processing is the (static) type checking problem: given an input and output type and a transformation f, can we statically check whether all outputs generated by f on valid inputs conform to the output type? Since XML types are intrinsically more complex than the types found in conventional programming languages, the type checking problem for XML poses new challenges on the design of type checking algorithms.
In its most general setting, the type checking problem for XML transformations is undecidable. Hence, general solutions are bound to be approximative, but seem to work well for practical XSLT transformations. Another approach is to restrict the types and transformations in such a way that type checking becomes decidable; we then refer to the problem as exact XML type checking. For the exact setting, types can be considered as regular or recognizable tree languages — thus, capturing the expressive strength of virtually all known type formalisms for XML.
Even though the class of transformations for which exact type checking is possible is surprisingly large, the price to be paid for exactness is also extremely high. The design space for exact type checking comes as a huge “exponential wasteland”: even for simple top-down transformations, exact type checking is exponential-time complete, and for more complex transformations such as k-pebble transducers the problem is non-elementary. For practical considerations, however, one is interested in useful subclasses of transformations for which exact type checking is provably tractable.