Sylvia Friese. On Normalization and Type Checking for Tree Transducers. PhD thesis, Institut für Informatik, Technische Universität München July 2011.
Tree transducers are an expressive formalism for reasoning about tree-structured data. Practical applications range from XSLT-like document transformations to translations of natural languages. We show that for every deterministic bottom-up tree transducer, a unique equivalent minimal transducer can be constructed - in polynomial time if every state of the transducer produces either none or infinitely many outputs. Using forward type inference it is shown that type checking of tree walking transducers can be performed in polynomial time, if the output type is specified by a deterministic tree automaton and the transducer visits every input node only a bounded number of times. Finally, the approach is generalized to transducers with accumulating parameters and to forest walking transducers.