  We show 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: polynomial time
for total transducers with unary output alphabet (over a given top-down regular
domain language), and co-randomized polynomial time for linear transducers;
these results are obtained using techniques from multi-linear algebra.
  For our main result, we prove that equivalence can be certified by means of
inductive invariants using polynomial ideals. This allows us to construct two
semi-algorithms, one searching for a proof of equivalence, one for a witness of
non-equivalence. Furthermore, we extend our result to deterministic top-down
tree-to-string transducers which produce output not in a free monoid but in a
free group.
