Exact XML Type Checking in Polynomial Time
Stay macro tree transducers (smtts) are an expressive formalism for
reasoning about XSLT-like document transformations. Here, we consider
the exact type checking problem for smtts. While the problem is
decidable, the involved technique of inverse type inference is known
to have exponential worst-case complexity (already for top-down
transformations without parameters). We present a new adaptive
type checking algorithm based on forward type inference through exact
characterizations of output languages. The new algorithm correctly
type-checks all call-by-value smtts. Given that the output type is
specified by a deterministic automaton, the algorithm is
polynomial-time whenever the transducer uses only few parameters
and visits every input node only constantly often. Our new approach can
also be generalized from smtts to stay macro forest transducers which
additionally support concatenation as built-in output operation.
back to publications
back to project page