{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:12:38Z","timestamp":1751688758607,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["2022\/46\/A\/ST6\/00072"],"award-info":[{"award-number":["2022\/46\/A\/ST6\/00072"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            We consider injective first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>k<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e. given two such interpretations, one can decide whether, for every input tree, the two output trees are isomorphic.\n          <\/jats:p>\n          <jats:p>We also give a calculus of typed functions and combinators which derives exactly injective first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, coproducts and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus.<\/jats:p>\n          <jats:p>\n            As an application, we show that the equivalence problem is decidable for first-order interpretations between classes of graphs that have bounded tree-depth. In all cases studied in this paper, first-order logic and\n            <jats:sc>mso<\/jats:sc>\n            have the same expressive power, and hence all results apply also to\n            <jats:sc>mso<\/jats:sc>\n            interpretations.\n          <\/jats:p>","DOI":"10.1145\/3632887","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1326-1351","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Polyregular Functions on Unordered Trees of Bounded Height"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7758-1072","authenticated-orcid":false,"given":"Miko\u0142aj","family":"Boja\u0144czyk","sequence":"first","affiliation":[{"name":"University of Warsaw, Warsaw, Poland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5793-7425","authenticated-orcid":false,"given":"Bartek","family":"Klin","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","first-page":"48:1","volume-title":"Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, Ahmedabad, India (LIPIcs, Vol. 122)","author":"Boiret Adrien","year":"2018","unstructured":"Adrien Boiret, Radoslaw Pi\u00f3rkowski, and Janusz Schmude. 2018. Reducing Transducer Equivalence to Register Automata Problems Solved by \"Hilbert Method\". In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, Ahmedabad, India (LIPIcs, Vol. 122). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 48:1\u201348:16."},{"key":"e_1_3_1_3_1","unstructured":"Miko\u0142aj Boja\u0144czyk. 2018. Polyregular Functions. CoRR abs\/1810.08760 (2018)."},{"key":"e_1_3_1_4_1","volume-title":"Logic in Computer Science (LICS \u201922)","author":"Boja\u0144czyk Miko\u0142aj","year":"2022","unstructured":"Miko\u0142aj Boja\u0144czyk. 2022. Transducers of Polynomial Growth. In Logic in Computer Science (LICS \u201922). Association for Computing Machinery, New York, NY, USA."},{"key":"e_1_3_1_5_1","volume-title":"Logic in Computer Science (LICS \u201922)","author":"Boja\u0144czyk Miko\u0142aj","year":"2023","unstructured":"Miko\u0142aj Boja\u0144czyk. 2023. Folding Interpretations. In Logic in Computer Science (LICS \u201922). Association for Computing Machinery."},{"key":"e_1_3_1_6_1","first-page":"106:1","volume-title":"46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019","author":"Boja\u0144czyk Mikolaj","year":"2019","unstructured":"Mikolaj Boja\u0144czyk, Sandra Kiefer, and Nathan Lhote. 2019. String-to-String Interpretations With Polynomial-Size Output. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece. 106:1\u2013106:14."},{"key":"e_1_3_1_7_1","first-page":"19:1","volume-title":"45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic (LIPIcs, Vol. 170)","author":"Boja\u0144czyk Miko\u0142aj","year":"2020","unstructured":"Miko\u0142aj Boja\u0144czyk and Janusz Schmude. 2020. Some Remarks on Deciding Equivalence for Graph-To-Graph Transducers. In 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic (LIPIcs, Vol. 170), Javier Esparza and Daniel Kr\u00e1l\u2019 (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 19:1\u201319:14."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Miko\u0142aj Boja\u0144czyk and Bartek Klin. 2023. Polyregular functions on unordered trees of bounded height. CoRR abs\/2311.04180 (2023). https:\/\/doi.org\/10.48550\/arXiv.2311.04180 10.48550\/arXiv.2311.04180","DOI":"10.48550\/arXiv.2311.04180"},{"key":"e_1_3_1_9_1","volume-title":"The classical decision problem","author":"B\u00f6rger Egon","year":"2001","unstructured":"Egon B\u00f6rger, Erich Gr\u00e4del, and Yuri Gurevich. 2001. The classical decision problem. Springer Science & Business Media."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00024-Q"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"James Cheney Sam Lindley and Philip Wadler. 2014. Query Shredding: Efficient Relational Evaluation of Queries over Nested Multisets. In Proceedings of the 2014 ACM SIGMOD International Conference on Management of Data (SIGMOD \u201914). 1027\u20131038. https:\/\/doi.org\/10.1145\/2588555.2612186 10.1145\/2588555.2612186","DOI":"10.1145\/2588555.2612186"},{"key":"e_1_3_1_12_1","volume-title":"Encyclopedia of Mathematics and Its Applications","author":"Courcelle Bruno","year":"2012","unstructured":"Bruno Courcelle and Joost Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach. Encyclopedia of Mathematics and Its Applications, Vol. 138. Cambridge University Press."},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2006.04.003"},{"key":"e_1_3_1_14_1","first-page":"40:1","volume-title":"46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia (LIPIcs, Vol. 202)","author":"Dou\u00e9neau-Tabot Ga\u00ebtan","year":"2021","unstructured":"Ga\u00ebtan Dou\u00e9neau-Tabot. 2021. Pebble Transducers with Unary Output. In 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia (LIPIcs, Vol. 202), Filippo Bonchi and Simon J. Puglisi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 40:1\u201340:17."},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2946799"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(02)00030-2"},{"key":"e_1_3_1_18_1","first-page":"xxiv+","volume-title":"Algorithms and Combinatorics","author":"Ne\u0161et\u0159il Jaroslav","year":"2012","unstructured":"Jaroslav Ne\u0161et\u0159il and Patrice Ossona de Mendez. 2012. Sparsity. In Algorithms and Combinatorics. Vol. 28. Springer, xxiv+\u2013457."},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Wilmer Ricciotti and James Cheney. 2019. Mixing Set and Bag Semantics. In Proceedings of the 17th ACM SIGPLAN International Symposium on Database Programming Languages (DBPL 2019). 70\u201373. https:\/\/doi.org\/10.1145\/3315507.3330202 10.1145\/3315507.3330202","DOI":"10.1145\/3315507.3330202"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90054-P"},{"issue":"4","key":"e_1_3_1_21_1","article-title":"Equivalence of Deterministic Top-Down Tree-to-String Transducers Is Decidable","volume":"65","author":"Seidl Helmut","year":"2018","unstructured":"Helmut Seidl, Sebastian Maneth, and Gregor Kemper. 2018. Equivalence of Deterministic Top-Down Tree-to-String Transducers Is Decidable. J. ACM 65, 4 (April 2018).","journal-title":"J. ACM"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632887","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632887","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:06:02Z","timestamp":1751659562000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632887"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":20,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632887"],"URL":"https:\/\/doi.org\/10.1145\/3632887","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}