World Scientific
  • Search
  •   
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
×

System Upgrade on Tue, May 28th, 2024 at 2am (EDT)

Existing users will be able to log into the site and access content. However, E-commerce and registration of new users may not be available for up to 12 hours.
For online purchase, please visit us again. Contact us at [email protected] for any enquiries.

Type Checking of Tree Walking Transducers

    https://doi.org/10.1142/9789814271059_0011Cited by:2 (Source: Crossref)
    Abstract:

    Tree walking transducers are an expressive formalism for reasoning about XSLT-like document transformations. One of the useful properties of tree transducers is decidability of type checking: given a transducer and input and output types, it can be checked statically whether the transducer is type correct, i.e., whether each document adhering to the input type is necessarily transformed into documents adhering to the output type. Here, a “type” means a regular set of trees specified by a finite-state tree automaton. Usually, type checking of tree transducers is extremely expensive; already for simple top-down tree transducers it is known to be EXPTIME-complete. Are there expressive classes of tree transducers for which type checking can be performed in polynomial time? Most of the previous approaches are based on inverse type inference. The approach presented here goes the other direction: it uses forward type inference. This means to infer, given a transducer and an input type, the corresponding set of output trees. In general, this set is not a type, i.e., is not regular. However, its intersection emptiness with a given type can be decided. Using this approach 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 transducer visits every input node only a bounded number of times. If the tree walking 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.