More Web Proxy on the site http://driver.im/

research-article

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

Authors:

Sebastian Maneth,

Gregor KemperAuthors Info & Claims

Journal of the ACM (JACM), Volume 65, Issue 4

Article No.: 21, Pages 1 - 30

https://doi.org/10.1145/3182653

Published: 12 April 2018 Publication History

Abstract

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.

References

[1]

Chritiene Aarts, Roland Carl Backhouse, Eerke A. Boiten, Henk Doornbos, Netty van Gasteren, Rik van Geldrop, Paul F. Hoogendijk, Ed Voermans, and Jaap van der Woude. 1995. Fixed-point calculus. Inf. Process. Lett. 53, 3 (1995), 131--136.

Digital Library

[2]

Rajeev Alur and Loris D’Antoni. 2017. Streaming tree transducers. J. ACM 64, 5 (2017), 31:1--31:55.

Digital Library

[3]

K. R. Apt and G. D. Plotkin. 1986. Countable nondeterminism and random assignment. J. ACM 33, 4 (1986), 724--767.

Digital Library

[4]

Thomas Becker and Volker Weispfenning. 1998. Gröbner Bases. A Computational Approach to Commutative Algebra, 2nd ed. Springer-Verlag, Berlin.

Digital Library

[5]

Michael Benedikt, Timothy Duff, Aditya Sharad, and James Worrell. 2017. Polynomial automata: Zeroness and applications. In LICS. 1--12.

[6]

Scott Boag, Don Chamberlin, Mary F. Fernández, Daniela Florescu, Jonathan Robie, and Jérôme Siméon. 2010. XQuery 1.0: An XML Query Language (Second Edition). Technical Report. W3C Recommendation.

[7]

Adrien Boiret and Raphaela Palenta. 2016. Deciding equivalence of linear tree-to-word transducers in polynomial time. In DLT. 355--367.

Digital Library

[8]

F. Braune, N. Seemann, D. Quernheim, and A. Maletti. 2013. Shallow local multi-bottom-up tree transducers in statistical machine translation. In ACL. 811--821.

[9]

Michael Colón. 2007. Polynomial approximations of the relational semantics of imperative programs. Sci. Comput. Program. 64, 1 (2007), 76--96.

Digital Library

[10]

K. Culik II and J. Karhumäki. 1986. A new proof for the D0L sequence equivalence problem and its implications. In The Book of L, G. Rozenberg and A. Salomaa (Eds.). Springer, Berlin, 63--74.

[11]

Joost Engelfriet. 1977. Top-down tree transducers with regular look-ahead. Math. Syst. Theory 10, 1 (1977), 289--303.

[12]

Joost Engelfriet. 1978. On tree transducers for partial functions. Inf. Process. Lett. 7, 4 (1978), 170--172.

[13]

Joost Engelfriet. 1980. Some open questions and recent results on tree transducers and tree languages. In Formal Language Theory: Perspectives and Open Problems, R. V. Book (ed.). Academic Press, New York, 241--286.

[14]

Joost Engelfriet and S. Maneth. 1999. Macro tree transducers, attribute grammars, and MSO definable tree translations. Inf. Comput. 154, 1 (1999), 34--91.

Digital Library

[15]

Joost Engelfriet and S. Maneth. 2002. Output string languages of compositions of deterministic macro tree transducers. J. Comput. Syst. Sci. 64, 2 (2002), 350--395.

Digital Library

[16]

Joost Engelfriet and S. Maneth. 2003a. A comparison of pebble tree transducers with macro tree transducers. Acta Inf. 39, 9 (2003), 613--698.

Digital Library

[17]

Joost Engelfriet and S. Maneth. 2003b. Macro tree translations of linear size increase are MSO definable. SIAM J. Comput. 32, 4 (2003), 950--1006.

[18]

Joost Engelfriet and S. Maneth. 2006. The equivalence problem for deterministic MSO tree transducers is decidable. Inform. Proc. Letters 100, 5 (2006), 206--212.

Digital Library

[19]

Joost Engelfriet, Sebastian Maneth, and Helmut Seidl. 2009. Deciding equivalence of top-down XML transformations in polynomial time. J. Comput. Syst. Sci. 75, 5 (2009), 271--286.

Digital Library

[20]

Joost Engelfriet and H. Vogler. 1985. Macro tree transducers. J. Comp. Syst. Sci. 31, 1 (1985), 71--146.

[21]

Z. Ésik. 1980. Decidability results concerning tree transducers I. Acta Cybernet. 5, 1 (1980), 1--20.

[22]

Z. Fülöp and H. Vogler. 1998. Syntax-Directed Semantics; Formal Models Based on Tree Transducers. Springer-Verlag.

Digital Library

[23]

Ferenc Gécseg and Magnus Steinby. 1997. Tree languages. In Handbook of Formal Languages, Vol. 3, Grzegorz Rozenberg and Arto Salomaa (Eds.). 1--68.

Digital Library

[24]

T. V. Griffiths. 1968. The unsolvability of the equivalence problem for lambda-free nondeterministic generalized machines. J. ACM 15, 3 (1968), 409--413.

Digital Library

[25]

S. Hakuta, S. Maneth, K. Nakano, and H. Iwasaki. 2014. XQuery streaming by forest transducers. In ICDE. 952--963.

[26]

G. H. Hardy and E. M. Wright. 2008. An Introduction to the Theory of Numbers (sixth ed.). Oxford University Press, Oxford.

[27]

J. Honkala. 2000. A short solution for the HDT0L sequence equivalence problem. Theor. Comput. Sci. 244, 1--2 (2000), 267--270.

Digital Library

[28]

Simon Holm Jensen, Magnus Madsen, and Anders Møller. 2011. Modeling the HTML DOM and browser API in static analysis of javascript web applications. In SIGSOFT FSE. 59--69.

Digital Library

[29]

Ralf Küsters and Thomas Wilke. 2007. Transducer-based analysis of cryptographic protocols. Inf. Comput. 205, 12 (2007), 1741--1776.

Digital Library

[30]

G. Laurence, A. Lemay, J. Niehren, S. Staworko, and M. Tommasi. 2011. Normalization of sequential top-down tree-to-word transducers. In LATA. 354--365.

Digital Library

[31]

G. Laurence, A. Lemay, J. Niehren, S. Staworko, and M. Tommasi. 2014. Learning sequential tree-to-word transducers. In LATA. 490--502.

Digital Library

[32]

Aurélien Lemay, Sebastian Maneth, and Joachim Niehren. 2010. A learning algorithm for top-down XML transformations. In PODS. 285--296.

Digital Library

[33]

A.A. Letichevsky and M.S. Lvov. 1993. Discovery of invariant equalities in programs over data fields. Applic. Alg. Eng. Commun. Comput. 4, 4 (1993), 21--29.

[34]

Yang Liu, Yun Huang, Qun Liu, and Shouxun Lin. 2007. Forest-to-string statistical translation rules. In ACL, Vol. 45. 704.

[35]

Yang Liu, Qun Liu, and Shouxun Lin. 2006. Tree-to-string alignment template for statistical machine translation. In ACL. 609--616.

Digital Library

[36]

Clara Löh. 2015. Geometric Group Theory, an Introduction. Technical Report. Fakultät für Mathematik, Universität Regensburg, Germany.

[37]

Andreas Maletti, Jonathan Graehl, Mark Hopkins, and Kevin Knight. 2009. The power of extended top-down tree transducers. SIAM J. Comput. 39, 2 (2009), 410--430.

Digital Library

[38]

S. Maneth. 2003. Models of Tree Translation. Ph.D. thesis. University of Leiden.

[39]

Sebastian Maneth. 2015. A survey on decidable equivalence problems for tree transducers. Int. J. Found. Comput. Sci. 26, 8 (2015), 1069--1100.

[40]

S. Maneth, A. Berlea, T. Perst, and H. Seidl. 2005. XML type checking with macro tree transducers. In PODS. 283--294.

Digital Library

[41]

S. Maneth and F. Neven. 1999. Structured document transformations based on XSL. In DBPL. 80--98.

Digital Library

[42]

S. Maneth, T. Perst, and H. Seidl. 2007. Exact XML type checking in polynomial time. In ICDT. 254--268.

Digital Library

[43]

Simon Marlow and Philip Wadler. 1993. Deforestation for higher-order functions. In Functional Programming. 154--165.

Digital Library

[44]

K. Matsuda, K. Inaba, and K. Nakano. 2012. Polynomial-time inverse computation for accumulative functions with multiple data traversals. In PEPM. 5--14.

Digital Library

[45]

Markus Müller-Olm and Helmut Seidl. 2004a. Computing polynomial program invariants. Inf. Process. Lett. 91, 5 (2004), 233--244.

Digital Library

[46]

Markus Müller-Olm and Helmut Seidl. 2004b. A note on karr’s algorithm. In ICALP. 1016--1028.

[47]

T. Perst and H. Seidl. 2004. Macro forest transducers. Inf. Process. Lett. 89 (2004), 141--149.

Digital Library

[48]

W. Plandowski. 1994. Testing equivalence of morphisms on context-free languages. In ESA. 460--470.

Digital Library

[49]

W. C. Rounds. 1970. Mappings and grammars on trees. Math. Syst. Theory 4, 3 (1970), 257--287.

[50]

K. Ruohonen. 1986. Equivalence problems for regular sets of word morphisms. In The Book of L, G. Rozenberg and A. Salomaa (Eds.). Springer, Berlin, 393--401.

[51]

Helmut Seidl. 1990. Deciding equivalence of finite tree automata. SIAM J. Comput. 19, 3 (1990), 424--437.

Digital Library

[52]

Helmut Seidl, Sebastian Maneth, and Gregor Kemper. 2015. Equivalence of deterministic top-down tree-to-string transducers is decidable. In FOCS. 943--962.

Digital Library

[53]

S. Staworko, G. Laurence, A. Lemay, and J. Niehren. 2009. Equivalence of deterministic nested word to word transducers. In FCT. 310--322.

Digital Library

[54]

J. W. Thatcher. 1970. Generalized sequential machine maps. J. Comput. Syst. Sci. 4, 4 (1970), 339--367.

Digital Library

[55]

Janis Voigtländer. 2005. Tree Transducer Composition as Program Transformation. Ph.D. thesis. TU Dresden.

[56]

Janis Voigtländer and Armin Kühnemann. 2004. Composition of functions with accumulating parameters. J. Funct. Program. 14, 3 (2004), 317--363.

Digital Library

[57]

W3C 1999. XSL Transformations (XSLT). W3C. Retrieved from http://www.w3.org/TR/xslt.

[58]

Philip Wadler. 1990. Deforestation: Transforming programs to eliminate trees. Theor. Comput. Sci. 73, 2 (1990), 231--248.

Digital Library

Cited By

Bojańczyk MKlin B(2024)Polyregular Functions on Unordered Trees of Bounded HeightProceedings of the ACM on Programming Languages10.1145/36328878:POPL(1326-1351)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632887
Hashimoto KManeth S(2023)Characterizing attributed tree translations in terms of macro tree transducersTheoretical Computer Science10.1016/j.tcs.2023.113943963(113943)Online publication date: Jun-2023
https://doi.org/10.1016/j.tcs.2023.113943
Maneth SSeidl H(2023)Deciding origin equivalence of weakly self-nesting macro tree transducersInformation Processing Letters10.1016/j.ipl.2022.106332180(106332)Online publication date: Feb-2023
https://doi.org/10.1016/j.ipl.2022.106332
Show More Cited By

Index Terms

Equivalence of Deterministic Top-Down Tree-to-String Transducers Is Decidable
1. Theory of computation
  1. Formal languages and automata theory
    1. Automata extensions
      1. Transducers
    2. Tree languages

Recommendations

The equivalence problem for deterministic MSO tree transducers is decidable

It is decidable for deterministic MSO definable graph-to-string or graph-to-tree transducers whether they are equivalent on a context-free set of graphs.
Copyful Streaming String Transducers
Special Issue on the 11th International Workshop on Reachability Problems (RP 2017)
Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Černý in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a ...
The Equivalence Problem for Deterministic Two-Way Sequential Transducers is Decidable

The equivalence problem for deterministic two-way sequential transducers is a long time open problem which is known to be decidable for some restricted cases. Here, the problem is shown to be decidable also for the general case. In fact, the result holds ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 65, Issue 4

Distributed Computing, Cryptography, Distributed Computing, Cryptography, Coding Theory, Automata Theory, Complexity Theory, Programming Languages, Algorithms, Invited Paper Foreword and Databases

August 2018

307 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/3208081

Editor:
Éva Tardos
Cornell University

Issue’s Table of Contents

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 April 2018

Accepted: 01 January 2018

Revised: 01 January 2018

Received: 01 February 2017

Published in JACM Volume 65, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
254
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)1

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bojańczyk MKlin B(2024)Polyregular Functions on Unordered Trees of Bounded HeightProceedings of the ACM on Programming Languages10.1145/36328878:POPL(1326-1351)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632887
Hashimoto KManeth S(2023)Characterizing attributed tree translations in terms of macro tree transducersTheoretical Computer Science10.1016/j.tcs.2023.113943963(113943)Online publication date: Jun-2023
https://doi.org/10.1016/j.tcs.2023.113943
Maneth SSeidl H(2023)Deciding origin equivalence of weakly self-nesting macro tree transducersInformation Processing Letters10.1016/j.ipl.2022.106332180(106332)Online publication date: Feb-2023
https://doi.org/10.1016/j.ipl.2022.106332
Lemerre M(2023)Reverse Template Processing Using Abstract InterpretationStatic Analysis10.1007/978-3-031-44245-2_18(403-433)Online publication date: 24-Oct-2023
https://doi.org/10.1007/978-3-031-44245-2_18
Löbel RLuttenberger MSeidl H(2021)On the Balancedness of Tree-to-Word TransducersInternational Journal of Foundations of Computer Science10.1142/S012905412142007732:06(761-783)Online publication date: 14-Jul-2021
https://doi.org/10.1142/S0129054121420077
Takahashi YAsada KNakano K(2021)Streaming ranked-tree-to-string transducersTheoretical Computer Science10.1016/j.tcs.2020.12.033870(165-187)Online publication date: May-2021
https://doi.org/10.1016/j.tcs.2020.12.033
Löbel RLuttenberger MSeidl H(2020)On the Balancedness of Tree-to-Word TransducersDevelopments in Language Theory10.1007/978-3-030-48516-0_17(222-236)Online publication date: 26-May-2020
https://doi.org/10.1007/978-3-030-48516-0_17
Löbel RLuttenberger MSeidl H(2020)Equivalence of Linear Tree Transducers with Output in the Free GroupDevelopments in Language Theory10.1007/978-3-030-48516-0_16(207-221)Online publication date: 11-May-2020
https://dl.acm.org/doi/10.1007/978-3-030-48516-0_16
Takahashi YAsada KNakano K(2019)Streaming Ranked-Tree-to-String TransducersImplementation and Application of Automata10.1007/978-3-030-23679-3_19(235-247)Online publication date: 26-Jun-2019
https://doi.org/10.1007/978-3-030-23679-3_19
Seidl HPalenta RManeth S(2019)Deciding Equivalence of Separated Non-nested Attribute Systems in Polynomial TimeFoundations of Software Science and Computation Structures10.1007/978-3-030-17127-8_28(488-504)Online publication date: 5-Apr-2019
https://doi.org/10.1007/978-3-030-17127-8_28

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents