Abstract
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 corandomized 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.
time for total transducers with unary output alphabet (over a given top-down regular domain language), and corandomized 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.
Original language | English |
---|---|
Title of host publication | Foundations of Computer Science (FOCS), 2015 IEEE 56th Annual Symposium on |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 943 - 962 |
Number of pages | 20 |
DOIs | |
Publication status | Published - 20 Oct 2015 |