Analyzability of Tree Transducers

Sebastian Maneth
Monday, 26 September, 2011 - 14:00
Room: 2NO9.06

We give an introduction to tree transducers.
Tree transducers were invented in the 70's as a model for syntax-directed
translation in compilers. By now they are a well studied topic in formal
language theory with many powerful properties and results. Most recently,
they have been applied for XML queries and transformations. Three different
models are explained: (1) top-down tree transducers, (2) MSO tree transducers,
and (3) macro tree transducers. We discuss two important static analyzes for
these  transducers. The first one is inverse type inference: given a transducer M
and an output type T (i.e., a regular tree language) it derives a representation of
all input trees that produce, via M, a tree in T. Inverse type inference can be used
to type check a transformation against input and output types.  The second one
is equivalence checking: given two transducer it checks whether their
input-output functions coincide. This is useful for XML query optimization, and
also for verification. The full proof of decidability of equivalence is presented
for the case of MSO tree transducers.