Document Open Access Logo

Unbounded Data Nesting for Loops in Higher-Order Programs

Authors Adriana Baldacchino , Andrzej S. Murawski

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.12.pdf
  • Filesize: 0.94 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Program semantics
Keywords
  • Automata theory
  • automata over infinite alphabets
  • programming language semantics
  • contextual equivalence
  • game semantics

Metrics

Abstract

We study contextual interactions in an ML-like language equipped with general references and continuations, focusing on the reachability and approximation problems.
Previous work addressed higher-order programs with first-order references in the absence of loops using automata over nested data; however, extending these techniques to programs with loops encountered fundamental technical obstacles, stemming from the need to bound the depth of data.
We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops.
This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

Cite As Get BibTex

Adriana Baldacchino and Andrzej S. Murawski. Unbounded Data Nesting for Loops in Higher-Order Programs. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.12

Author Details

Adriana Baldacchino
  • School of Computer Science, University of Birmingham, UK
Andrzej S. Murawski
  • Department of Computer Science, University of Oxford, UK

Funding

  • Baldacchino, Adriana: The research work disclosed in this publication is partially funded by the ENDEAVOUR II Scholarships Scheme (Malta). Project is co-funded by the ESF+ 2021-2027.

Acknowledgements

We thank the anonymous reviewers for their very helpful feedback.

References

  1. Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In Zhong Shao and Benjamin C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 340-353. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480925.
  2. Henrik Björklund and Mikolaj Bojanczyk. Shuffle expressions and words with nested data. In Ludek Kucera and Antonín Kucera, editors, Mathematical Foundations of Computer Science 2007, 32nd International Symposium, MFCS 2007, Ceský Krumlov, Czech Republic, August 26-31, 2007, Proceedings, Lecture Notes in Computer Science, pages 750-761. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74456-6_66.
  3. Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. Theor. Comput. Sci., 411(4-5):702-715, 2010. URL: https://doi.org/10.1016/j.tcs.2009.10.009.
  4. Benedict Bunting and Andrzej S. Murawski. Contextual equivalence for state and control via nested data. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 19:1-19:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662109.
  5. Conrad Cotton-Barratt. Using class memory automata in algorithmic game semantics. PhD thesis, University of Oxford, UK, 2016. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.735894.
  6. Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong. Weak and Nested Class Memory Automata. In Language and Automata Theory and Applications, pages 188-199. Springer International Publishing, 2015. URL: https://doi.org/10.1007/978-3-319-15579-1_14.
  7. Normann Decker, Peter Habermehl, Martin Leucker, and Daniel Thoma. Ordered navigation on multi-attributed data words. In Paolo Baldan and Daniele Gorla, editors, Proceedings of CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 497-511. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_34.
  8. Emanuele D'Osualdo and C.-H. Luke Ong. On hierarchical communication topologies in the π-calculus. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 149-175. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_7.
  9. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program., 22(4-5):477-528, 2012. URL: https://doi.org/10.1017/S095679681200024X.
  10. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  11. Guilhem Jaber and Andrzej S. Murawski. Complete trace models of state and control. In Proceedings of ESOP, pages 348-374. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_13.
  12. Guilhem Jaber and Andrzej S. Murawski. Complete trace models of state and control (full version). Preprint, January 2021. URL: https://hal.science/hal-03116698.
  13. Neil D. Jones and Steven S. Muchnick. The complexity of finite memory programs with recursion. J. ACM, 25(2):312-321, 1978. URL: https://doi.org/10.1145/322063.322074.
  14. Ugo Dal Lago and Gabriele Vanoni. (not so) boring abstract machines. In Giuseppa Castiglione and Marinella Sciortino, editors, Proceedings of the 24th Italian Conference on Theoretical Computer Science, Palermo, Italy, September 13-15, 2023, volume 3587 of CEUR Workshop Proceedings, pages 225-240. CEUR-WS.org, 2023. URL: https://ceur-ws.org/Vol-3587/9878.pdf.
  15. Ralph Loader. Finitary PCF is not decidable. Theor. Comput. Sci., 266(1-2):341-364, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00194-8.
  16. Roland Meyer. On boundedness in depth in the pi-calculus. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and C.-H. Luke Ong, editors, Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, volume 273 of IFIP, pages 477-489. Springer, 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_32.
  17. Andrzej S. Murawski. Functions with local state: Regularity and undecidability. Theor. Comput. Sci., 338(1-3):315-349, 2005. URL: https://doi.org/10.1016/j.tcs.2004.12.036.
  18. C.-H. Luke Ong and Nikos Tzevelekos. Functional reachability. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 286-295. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.48.
  19. A. M. Pitts and I. D. B. Stark. Operational Reasoning for Functions with Local State, pages 227-274. Cambridge University Press, USA, 1999. Google Scholar
  20. Sylvain Schmitz and Philippe Schnoebelen. Algorithmic Aspects of WQO Theory. Lecture Notes, August 2012. URL: https://cel.hal.science/cel-00727025.
  21. Géraud Sénizergues. L(A)=L(B)? decidability results from complete formal systems. Theor. Comput. Sci., 251(1-2):1-166, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00285-1.
  22. Thomas Wies, Damien Zufferey, and Thomas A. Henzinger. Forward analysis of depth-bounded processes. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 94-108. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_8.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact