On Normalization and Type Checking for Tree Transducers
Sylvia Friese · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2011
Tree transducers are an expressive formalism for reasoning about data in a tree structure. Practical applications range from XSLT-like document transformations to translations of natural languages. Important problems for transducers are to decide whether two transducers are equivalent, to construct normal forms, give semantic characterizations, and type checking, i.e., to check whether the produced outputs satisfy given structural constraints. This thesis addresses these problems for important classes of tree transducers. We provide constructive solutions and also identify classes of transducers for which these algorithms run in polynomial time. Concerning semantic characterization of deterministic bottom-up tree transducers, we provide a Myhill-Nerode theorem. Concerning normalization and testing for equivalence, we show that for every deterministic bottom-up tree transducer, a unique equivalent transducer can be constructed which is minimal. For a deterministic bottom-up transducer where every state produces either none or infinitely many outputs, the minimal transducer can be constructed in polynomial time. In general, type checking of tree walking transducers is expensive: already for simple top-down tree transducers it is known to be EXPTIME-complete. Using forward type inference it is shown that type checking can be performed in polynomial time, if (1) the output type is specified by a deterministic tree automaton and (2) the tree walking transducer visits every input node only a bounded number of times. If the transducer is additionally equipped with accumulating call-by-value parameters, then the complexity of type checking also depends (exponentially) on the number of such parameters. For this case a fast approximative type checking algorithm is presented, based on context-free tree grammars. Finally, the approach is generalized from trees to forest walking transducers which additionally support concatenation as a built-in output operation.