Document Open Access Logo

Slightly Non-Linear Higher-Order Tree Transducers

Authors Lê Thành Dũng (Tito) Nguyễn , Gabriele Vanoni

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.STACS.2025.68.pdf
  • Filesize: 0.92 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.STACS.2025.68.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Transducers
Keywords
  • Almost affine lambda-calculus
  • geometry of interaction
  • reversibility
  • tree transducers
  • tree-walking automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We investigate the tree-to-tree functions computed by "affine λ-transducers": tree automata whose memory consists of an affine λ-term instead of a finite state. They can be seen as variations on Gallot, Lemay and Salvati’s Linear High-Order Deterministic Tree Transducers.
When the memory is almost purely affine (à la Kanazawa), we show that these machines can be translated to tree-walking transducers (and with a purely affine memory, we get a reversible tree-walking transducer). This leads to a proof of an inexpressivity conjecture of Nguyễn and Pradic on "implicit automata" in an affine λ-calculus. We also prove that a more powerful variant, extended with preprocessing by an MSO relabeling and allowing a limited amount of non-linearity, is equivalent in expressive power to Engelfriet, Hoogeboom and Samwel’s invisible pebble tree transducers.
The key technical tool in our proofs is the Interaction Abstract Machine (IAM), an operational avatar of Girard’s geometry of interaction, a semantics of linear logic. We work with ad-hoc specializations to λ-terms of low exponential depth of a tree-generating version of the IAM.

Cite As Get BibTex

Lê Thành Dũng (Tito) Nguyễn and Gabriele Vanoni. Slightly Non-Linear Higher-Order Tree Transducers. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 68:1-68:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.68

Author Details

Lê Thành Dũng (Tito) Nguyễn
  • CNRS & Aix-Marseille University, France
Gabriele Vanoni
  • IRIF, Université Paris Cité, France

Funding

  • Nguyễn, Lê Thành Dũng (Tito): Supported by the DyVerSe project (ANR-19-CE48-0010).
  • Vanoni, Gabriele: Supported by the ANR PPS Project (ANR-19-CE48-0014) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101034255.

Acknowledgements

We thank Damiano Mazza and Cécilia Pradic for discussions on the possible applications of the Geometry of Interaction to implicit complexity and automata theory.

References

  1. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The machinery of interaction. In PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020, pages 4:1-4:15. ACM, 2020. URL: https://doi.org/10.1145/3414080.3414108.
  2. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The space of interaction. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470726.
  3. Beniamino Accattoli and Delia Kesner. The structural λ-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 381-395. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_30.
  4. Rajeev Alur and Loris D'Antoni. Streaming Tree Transducers. Journal of the ACM, 64(5):1-55, August 2017. URL: https://doi.org/10.1145/3092842.
  5. Toshiyasu Arai. 10th Asian Logic Conference. The Bulletin of Symbolic Logic, 15(2):246-265, 2009. URL: https://doi.org/10.2178/bsl/1243948490.
  6. Andrew Barber. Dual Intuitionistic Linear Logic. Technical report ECS-LFCS-96-347, LFCS, University of Edinburgh, 1996. URL: http://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/.
  7. Roderick Bloem and Joost Engelfriet. A Comparison of Tree Transductions Defined by Monadic Second Order Logic and by Attribute Grammars. Journal of Computer and System Sciences, 61(1):1-50, August 2000. URL: https://doi.org/10.1006/jcss.1999.1684.
  8. Mikołaj Bojańczyk. Who to cite: MSO transductions, December 2019. URL: https://web.archive.org/web/20230810161232/https://www.mimuw.edu.pl/~bojan/posts/who-to-cite-mso-transductions.
  9. Mikołaj Bojańczyk and Thomas Colcombet. Tree-walking automata do not recognize all regular languages. SIAM Journal on Computing, 38(2):658-701, 2008. URL: https://doi.org/10.1137/050645427.
  10. Mikołaj Bojańczyk and Amina Doumane. First-order tree-to-tree functions, 2020. Corrected version with erratum of a LICS 2020 paper. URL: https://arxiv.org/abs/2002.09307v2.
  11. Pierre Clairambault and Andrzej S. Murawski. On the Expressivity of Linear Recursion Schemes. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of Leibniz International Proceedings in Informatics (LIPIcs), pages 50:1-50:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.50.
  12. Bruno Courcelle and Joost Engelfriet. Graph structure and monadic second-order logic. A language-theoretic approach. Encyclopedia of Mathematics and its applications, Vol. 138. Cambridge University Press, June 2012. Collection Encyclopedia of Mathematics and Applications, Vol. 138. URL: https://hal.archives-ouvertes.fr/hal-00646514.
  13. Ugo Dal Lago and Ulrich Schöpp. Computation by interaction for space-bounded functional programming. Information and Computation, 248:150-194, 2016. URL: https://doi.org/10.1016/j.ic.2015.04.006.
  14. Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal λ-machines. Theoretical Computer Science, 227(1):79-97, September 1999. URL: https://doi.org/10.1016/S0304-3975(99)00049-3.
  15. Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote. On reversible transducers. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 113:1-113:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.113.
  16. Joost Engelfriet. The time complexity of typechecking tree-walking tree transducers. Acta Informatica, 46(2):139-154, 2009. URL: https://doi.org/10.1007/s00236-008-0087-y.
  17. Joost Engelfriet. Context-free grammars with storage, 2014. Revised version of a 1986 technical report. URL: https://arxiv.org/abs/1408.0683.
  18. Joost Engelfriet, Hendrik Jan Hoogeboom, and Bart Samwel. XML navigation and transformation by tree-walking automata and transducers with visible and invisible pebbles. Theoretical Computer Science, 850:40-97, January 2021. URL: https://doi.org/10.1016/j.tcs.2020.10.030.
  19. Joost Engelfriet, Kazuhiro Inaba, and Sebastian Maneth. Linear-bounded composition of tree-walking tree transducers: linear size increase and complexity. Acta Informatica, 58(1-2):95-152, 2021. URL: https://doi.org/10.1007/s00236-019-00360-8.
  20. Joost Engelfriet and Sebastian Maneth. Macro Tree Transducers, Attribute Grammars, and MSO Definable Tree Translations. Information and Computation, 154(1):34-91, October 1999. URL: https://doi.org/10.1006/inco.1999.2807.
  21. Joost Engelfriet and Heiko Vogler. High level tree transducers and iterated pushdown tree transducers. Acta Informatica, 26(1/2):131-192, 1988. URL: https://doi.org/10.1007/BF02915449.
  22. Paul Gallot, Aurélien Lemay, and Sylvain Salvati. Linear high-order deterministic tree transducers with regular look-ahead. In Javier Esparza and Daniel Král', editors, 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic, volume 170 of LIPIcs, pages 38:1-38:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.38.
  23. Paul D. Gallot. Safety of transformations of data trees: tree transducer theory applied to a verification problem on shell scripts. PhD thesis, Université de Lille, December 2021. URL: https://theses.hal.science/tel-03773108.
  24. Dan R. Ghica. Geometry of Synthesis: A Structured Approach to VLSI Design. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 363-375. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190269.
  25. Tsutomu Kamimura and Giora Slutzki. Parallel and two-way automata on directed ordered acyclic graphs. Information and Control, 49(1):10-51, 1981. URL: https://doi.org/10.1016/S0019-9958(81)90438-1.
  26. Makoto Kanazawa. A lambda calculus characterization of MSO definable tree transductions, September 2008. Talk given at the 10th Asian Logic Conference, Kobe University, Japan. Slides available at https://makotokanazawa.ws.hosei.ac.jp/talks/asian_logic.pdf. Abstract available at [Arai, 2009].
  27. Makoto Kanazawa. Almost affine lambda terms. In Andrzej Indrzejczak, Janusz Kaczmarek, and Michał Zawidzki, editors, Trends in Logic XIII. Gentzen’s and Jaśkowski’s Heritage. 80 Years of Natural Deduction and Sequent Calculi, pages 131-148. Wydawnictwo Uniwersytetu Łódzkiego, 2014. Google Scholar
  28. Makoto Kanazawa. Parsing and generation as datalog query evaluation. IfCoLog Journal of Logics and their Applications (FLAP), 4(4), 2017. Long version of an ACL 2007 paper. URL: http://www.collegepublications.co.uk/downloads/ifcolog00013.pdf.
  29. Shin-ya Katsumata. Attribute grammars and categorical semantics. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 271-282. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_23.
  30. Donald E. Knuth. The genesis of attribute grammars. In Pierre Deransart and Martin Jourdan, editors, Attribute Grammars and their Applications, International Conference WAGA, Paris, France, September 19-21, 1990, Proceedings, volume 461 of Lecture Notes in Computer Science, pages 1-12. Springer, 1990. URL: https://doi.org/10.1007/3-540-53101-7_1.
  31. Damiano Mazza. Simple parsimonious types and logarithmic space. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 24-40. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.24.
  32. Damiano Mazza. Polyadic Approximations in Logic and Computation. Habilitation à diriger des recherches, Université Paris XIII (Sorbonne Paris Nord), November 2017. URL: https://theses.hal.science/tel-04238579.
  33. Anca Muscholl and Gabriele Puppis. The Many Facets of String Transducers. In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019), volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.STACS.2019.2.
  34. Lê Thành Dũng Nguy~ên. Implicit automata in linear logic and categorical transducer theory. PhD thesis, Université Paris XIII (Sorbonne Paris Nord), December 2021. URL: https://theses.hal.science/tel-04132636.
  35. Lê Thành Dũng Nguyễn. Two or three things i know about tree transducers, 2024. URL: https://arxiv.org/abs/2409.03169.
  36. Lê Thành Dũng Nguyễn, Camille Noûs, and Cécilia Pradic. Two-way automata and transducers with planar behaviours are aperiodic, 2023. URL: https://arxiv.org/abs/2307.11057.
  37. Lê Thành Dũng Nguyễn and Cécilia Pradic. Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 135:1-135:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.135.
  38. Lê Thành Dũng Nguyễn and Gabriele Vanoni. Slightly non-linear higher-order tree transducers. CoRR, abs/2402.05854, 2024. URL: https://doi.org/10.48550/arXiv.2402.05854.
  39. Alexander Okhotin. Graph-walking automata: From whence they come, and whither they are bound. In Michal Hospodár and Galina Jirásková, editors, Implementation and Application of Automata - 24th International Conference, CIAA 2019, Košice, Slovakia, July 22-25, 2019, Proceedings, volume 11601 of Lecture Notes in Computer Science, pages 10-29. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-23679-3_2.
  40. Cécilia Pradic and Ian Price. Implicit automata in λ-calculi iii: affine planar string-to-string functions. Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL, December 2024. URL: https://doi.org/10.46298/entics.14804.
  41. Sylvain Salvati. Encoding second order string ACG with deterministic tree walking transducers. In Shuly Wintner, editor, The 11th conference on Formal Grammar, FG Online Proceedings, pages 143-156, Malaga, Spain, 2006. Paola Monachesi; Gerald Penn; Giorgio Satta; Shuly Wintner, CSLI Publications. URL: https://web.stanford.edu/group/cslipublications/cslipublications/FG/2006/salvati.pdf.
  42. Sylvain Salvati. Lambda-calculus and formal language theory. Habilitation à diriger des recherches, Université de Bordeaux, December 2015. URL: https://theses.hal.science/tel-01253426.
  43. Sylvain Salvati and Igor Walukiewicz. Simply typed fixpoint calculus and collapsible pushdown automata. Mathematical Structures in Computer Science, 26(7):1304-1350, October 2016. URL: https://doi.org/10.1017/S0960129514000590.
  44. Ulrich Schöpp. Space-efficient computation by interaction. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 606-621. Springer, 2006. URL: https://doi.org/10.1007/11874683_40.
  45. Ulrich Schöpp. Stratified bounded affine logic for logarithmic space. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 411-420. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.45.
  46. Gabriele Vanoni. On Reasonable Space and Time Cost Models for the λ-Calculus. PhD thesis, Alma Mater Studiorum - Università di Bologna, June 2022. URL: https://doi.org/10.48676/unibo/amsdottorato/10276.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact