Equivalence of deterministic top-down tree-To-string transducers is decidable

Helmut Seidl, Sebastian Maneth, Gregor Kemper

Research output: Contribution to journalArticlepeer-review

11 Scopus citations


We prove that equivalence of deterministic top-down tree-To-string transducers is decidable, thus solving a long-standing open problem in formal language theory. We also present efficient algorithms for subclasses: for linear transducers or total transducers with unary output alphabet (over a given top-down regular domain language), as well as for transducers with the single-use restriction. These results are obtained using techniques from multi-linear algebra. For our main result, we introduce polynomial transducers and prove that for these, validity of a polynomial invariant can be certified by means of an inductive invariant of polynomial ideals. This allows us to construct two semi-Algorithms, one searching for a certificate of the invariant and one searching for a witness of its violation. Via a translation into polynomial transducers, we thus obtain that equivalence of general ydt transducers is decidable. In fact, our translation also shows that equivalence is decidable when the output is not in a free monoid but in a free group.

Original languageEnglish
Article number21
JournalJournal of the ACM
Issue number4
StatePublished - Aug 2018


  • Decidability
  • Equivalence problem
  • Macro tree transducer
  • Polynomial ideals
  • Tree-To-string transducer


Dive into the research topics of 'Equivalence of deterministic top-down tree-To-string transducers is decidable'. Together they form a unique fingerprint.

Cite this