Seminars

Abstract:
Tree transducers have a wide range of application domains ranging from compiler construction,
program analysis, and computational linguistics, to semi-structured databases and file system
transformations. A common application of these domains is to specify and verify transformations
of data trees, i.e., trees whose nodes are labeled by data values from an infinite domain. Most
existing classes of tree transducers and their formal studies, however, are restricted to trees over
finite signatures without data. In this paper, we lift the most prominent class of top-down tree
transducers to data trees, such that its good properties are preserved. In particular, we show that
top-down transducers for data trees have a decidable equivalence problem, without imposing any
linearity restriction as in previous approaches based on symbolic top-down tree transducers.