Equivalence of Deterministic Tree-to-String Transducers is Decidable

Top-down tree-to-string transducers recursively process their structured input data while producing output in an unstructured way, namely as a string. Let yDT denote the class of all deterministic top-down tree-to-string transducers. In the presentation, we show that equivalence of two such transducers is decidable – a problem which has been open for more than 30 years. As non-equivalence can be witnessed by an input on which the two transducers differ, decidability of equivalence follows if only an effective proof system can be provided for certifying equivalence whenever it holds. We indicate how such a proof system can be constructed using powerful techniques from commutative algebra. While in general not much is known about the complexity of the decision problem, we also present special cases where polynomial upper bounds can be obtained.

Authors

• Joint work with Sebastian Maneth (Edinburgh)
• Gregor Kemper (München)

Keywords

No keywords are indexed for this paper.