Linear High-Order Deterministic Tree Transducers with Regular Look-Ahead

Authors Paul D. Gallot, Aurélien Lemay, Sylvain Salvati

Thumbnail PDF


  • Filesize: 461 kB
  • 13 pages

Document Identifiers

Author Details

Paul D. Gallot
  • INRIA, Université de Lille, Villeneuve d'Ascq, France
Aurélien Lemay
  • Université de Lille, INRIA, CNRS, Villeneuve d'Ascq, France
Sylvain Salvati
  • Université de Lille, INRIA, CNRS, Villeneuve d'Ascq, France

Cite AsGet BibTex

Paul D. Gallot, Aurélien Lemay, and Sylvain Salvati. Linear High-Order Deterministic Tree Transducers with Regular Look-Ahead. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 38:1-38:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


We introduce the notion of high-order deterministic top-down tree transducers (HODT) whose outputs correspond to single-typed lambda-calculus formulas. These transducers are natural generalizations of known models of top-tree transducers such as: Deterministic Top-Down Tree Transducers, Macro Tree Transducers, Streaming Tree Transducers... We focus on the linear restriction of high order tree transducers with look-ahead (HODTR_lin), and prove this corresponds to tree to tree functional transformations defined by Monadic Second Order (MSO) logic. We give a specialized procedure for the composition of those transducers that uses a flow analysis based on coherence spaces and allows us to preserve the linearity of transducers. This procedure has a better complexity than classical algorithms for composition of other equivalent tree transducers, but raises the order of transducers. However, we also indicate that the order of a HODTR_lin can always be bounded by 3, and give a procedure that reduces the order of a HODTR_lin to 3. As those resulting HODTR_lin can then be transformed into other equivalent models, this gives an important insight on composition algorithm for other classes of transducers. Finally, we prove that those results partially translate to the case of almost linear HODTR: the class corresponds to the class of tree transformations performed by MSO with unfolding (not closed by composition), and provide a mechanism to reduce the order to 3 in this case.

Subject Classification

ACM Subject Classification
  • Theory of computation → Transducers
  • Theory of computation → Lambda calculus
  • Theory of computation → Tree languages
  • Transducers
  • λ-calculus
  • Trees


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


  1. R. Alur and L. D'Antoni. Streaming tree transducers. J. ACM, 64(5):31:1-31:55, 2017. Google Scholar
  2. Roderick Bloem and Joost Engelfriet. A comparison of tree transductions defined by monadic second order logic and by attribute grammars. J. Comput. Syst. Sci., 61(1):1-50, 2000. URL:
  3. C. Choffrut. A generalization of Ginsburg and Rose’s characterisation of g-s-m mappings. In ICALP 79, number 71 in LNCS, pages 88-103. SV, 1979. Google Scholar
  4. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. Löding, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications, 2007. URL:
  5. B. Courcelle. Monadic second-order definable graph transductions: a survey. Theoretical Computer Science, 126(1):53-75, 1994. Google Scholar
  6. B. Courcelle. Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. In Rozenberg, editor, Handbook of Graph Grammars, 1997. Google Scholar
  7. S. Eilenberg. Automata, Languages and Machines. Acad. Press, 1974. Google Scholar
  8. C. C. Elgot and G. Mezei. On relations defined by generalized finite automata. IBM J. of Res. and Dev., 9:88-101, 1965. Google Scholar
  9. J. Engelfriet and S. Maneth. Macro tree transducers, attribute grammars, and mso definable tree translations. Information and Computation, 154(1):34-91, 1999. Google Scholar
  10. J. Engelfriet and S. Maneth. The equivalence problem for deterministic MSO tree transducers is decidable. Inf. Process. Lett., 100(5):206-212, 2006. Google Scholar
  11. J. Engelfriet and H. Vogler. Macro tree transducers. J. Comput. Syst. Sci., 31(1):71-146, 1985. Google Scholar
  12. Joost Engelfriet and Heiko Vogler. High level tree transducers and iterated pushdown tree transducers. Acta Informatica, 26(1):131-192, October 1988. URL:
  13. J. Y. Girard. Linear logic. TCS, 50:1-102, 1987. Google Scholar
  14. M Kanazawa and R Yoshinaka. Distributional learning and context/substructure enumerability in nonlinear tree grammars. In Formal Grammar, pages 94-111. Springer, 2016. Google Scholar
  15. Makoto Kanazawa. Almost affine lambda terms. National Institute of Informatics, 2012. Google Scholar
  16. Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. SIGPLAN Not., 45(1):495-508, January 2010. URL:
  17. J. Thatcher and J. Wright. Generalized Finite Automata Theory With an Application to a Decision Problem of Second-Order Logic. Mathematical Systems Theory, 2(1):57-81, 1968. Google Scholar
  18. Akihiko Tozawa. Xml type checking using high-level tree transducer. In Masami Hagiya and Philip Wadler, editors, Functional and Logic Programming, pages 81-96, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail