Exact XML Type Checking in Polynomial Time

Macro tree transducers (mtts) are an expressive formalism for reasoning about \\XSLT-like document transformations. \\Here we are interested in the exact type\\ checking problem for mtts. While the problem is decidable, the involved\\ technique of inverse type inference is, however, known to have exponential\\ worst-case complexity (already for top-down transformations without parameters).\\ We present new type checking algorithms based on forward type inference through\\ exact characterizations of output languages. The algorithms show that exact\\ type checking for call-by-value mtts with few parameters can be done in\\ polynomial time, given that the output type is specified by a deterministic\\ automaton and that the mtt visits every input node only constantly often. \\For general mtts, a fast approximative type checking algorithm is presented. \\The algorithms in this paper are based on results about context-free tree and graph grammars.\\ Finally, the new approach is generalized from mtts to macro forest\\ transducers which additionally support concatenation as built-in output operation.     «

Macro tree transducers (mtts) are an expressive formalism for reasoning about \\XSLT-like document transformations. \\Here we are interested in the exact type\\ checking problem for mtts. While the problem is decidable, the involved\\ technique of inverse type inference is, however, known to have exponential\\ worst-case complexity (already for top-down transformations without parameters).\\ We present new type checking algorithms based on forward type inference through\\ exact characterizations...     »