Equivalence of Deterministic Top-Down Tree-to-String Transducers Is Decidable

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 y dt 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.