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