Document Open Access Logo

Unboundedness for Recursion Schemes: A Simpler Type System

Authors David Barozzini, Paweł Parys , Jan Wróblewski

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.112.pdf
  • Filesize: 0.76 MB
  • 19 pages

Document Identifiers

Author Details

David Barozzini
  • Institute of Informatics, University of Warsaw, Poland
Paweł Parys
  • Institute of Informatics, University of Warsaw, Poland
Jan Wróblewski
  • Institute of Informatics, University of Warsaw, Poland

Funding

Work supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).

Cite As Get BibTex

David Barozzini, Paweł Parys, and Jan Wróblewski. Unboundedness for Recursion Schemes: A Simpler Type System. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 112:1-112:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ICALP.2022.112

Abstract

Decidability of the problems of unboundedness and simultaneous unboundedness (aka. the diagonal problem) for higher-order recursion schemes was established by Clemente, Parys, Salvati, and Walukiewicz (2016). Then a procedure of optimal complexity was presented by Parys (2017); this procedure used a complicated type system, involving multiple flags and markers. We present here a simpler and much more intuitive type system serving the same purpose. We prove that this type system allows to solve the unboundedness problem for a widely considered subclass of recursion schemes, called safe schemes. For unsafe recursion schemes we only have soundness of the type system: if one can establish a type derivation claiming that a recursion scheme is unbounded then it is indeed unbounded. Completeness of the type system for unsafe recursion schemes is left as an open question. Going further, we discuss an extension of the type system that allows to handle the simultaneous unboundedness problem.
We also design and implement an algorithm that fully automatically checks unboundedness of a given recursion scheme, completing in a short time for a wide variety of inputs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Rewrite systems
  • Mathematics of computing → Lambda calculus
Keywords
  • Higher-order recursion schemes
  • boundedness
  • intersection types
  • safe schemes

Metrics

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

Related Versions

Supplementary Materials

References

  1. Alfred V. Aho. Indexed grammars - an extension of context-free grammars. J. ACM, 15(4):647-671, 1968. URL: https://doi.org/10.1145/321479.321488.
  2. William Blum and C.-H. Luke Ong. The safe lambda calculus. Logical Methods in Computer Science, 5(1), 2009. URL: https://doi.org/10.2168/LMCS-5(1:3)2009.
  3. Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. URL: https://doi.org/10.1142/S0129054196000191.
  4. Christopher H. Broadbent and Naoki Kobayashi. Saturation-based model checking of higher-order recursion schemes. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 129-148. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.129.
  5. Arnaud Carayol and Olivier Serre. Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 165-174. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.73.
  6. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered tree-pushdown systems. In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 163-177. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.163.
  7. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 96-105. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934527.
  8. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A characterization for decidable separability by piecewise testable languages. Discrete Mathematics & Theoretical Computer Science, 19(4), 2017. URL: https://doi.org/10.23638/DMTCS-19-4-1.
  9. Werner Damm. The IO- and OI-hierarchies. Theor. Comput. Sci., 20:95-207, 1982. URL: https://doi.org/10.1016/0304-3975(82)90009-3.
  10. Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 151-163. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837627.
  11. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. ACM Trans. Comput. Log., 18(3):25:1-25:42, 2017. URL: https://doi.org/10.1145/3091122.
  12. Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_15.
  13. Naoki Kobayashi. Model checking higher-order programs. J. ACM, 60(3):20:1-20:62, 2013. URL: https://doi.org/10.1145/2487241.2487246.
  14. Naoki Kobayashi and C.-H. Luke Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logical Methods in Computer Science, 7(4), 2011. URL: https://doi.org/10.2168/LMCS-7(4:9)2011.
  15. Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Predicate abstraction and CEGAR for higher-order model checking. In Mary W. Hall and David A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 222-233. ACM, 2011. URL: https://doi.org/10.1145/1993498.1993525.
  16. Gregory M. Kobele and Sylvain Salvati. The IO and OI hierarchies revisited. Inf. Comput., 243:205-221, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.015.
  17. Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. General decidability results for asynchronous shared-memory programs: Higher-order and beyond. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 449-467. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_24.
  18. Robin P. Neatherway and C.-H. Luke Ong. TravMC2: higher-order model checking for alternating parity tree automata. In Neha Rungta and Oksana Tkachuk, editors, 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014, pages 129-132. ACM, 2014. URL: https://doi.org/10.1145/2632362.2632381.
  19. Robin P. Neatherway, Steven J. Ramsay, and C.-H. Luke Ong. A traversal-based algorithm for higher-order model checking. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 353-364. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364578.
  20. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  21. Paweł Parys. A characterization of lambda-terms transforming numerals. J. Funct. Program., 26:e12, 2016. URL: https://doi.org/10.1017/S0956796816000113.
  22. Paweł Parys. Intersection types and counting. In Naoki Kobayashi, editor, Proceedings Eighth Workshop on Intersection Types and Related Systems, ITRS 2016, Porto, Portugal, 26th June 2016., volume 242 of EPTCS, pages 48-63, 2016. URL: https://doi.org/10.4204/EPTCS.242.6.
  23. Paweł Parys. Homogeneity without loss of generality. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs, pages 27:1-27:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.27.
  24. Paweł Parys. Intersection types for unboundedness problems. In Michele Pagani and Sandra Alves, editors, Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems, DCM/ITRS 2018, Oxford, UK, 8th July 2018, volume 293 of EPTCS, pages 7-27, 2018. URL: https://doi.org/10.4204/EPTCS.293.2.
  25. Paweł Parys. Recursion schemes, the MSO logic, and the U quantifier. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:20)2020.
  26. Paweł Parys. A type system describing unboundedness. Discret. Math. Theor. Comput. Sci., 22(4), 2020. URL: https://doi.org/10.23638/DMTCS-22-4-2.
  27. Sylvain Salvati and Igor Walukiewicz. Simply typed fixpoint calculus and collapsible pushdown automata. Mathematical Structures in Computer Science, 26(7):1304-1350, 2016. URL: https://doi.org/10.1017/S0960129514000590.
  28. Hiroshi Unno, Naoshi Tabuchi, and Naoki Kobayashi. Verification of tree-processing programs via higher-order mode checking. Mathematical Structures in Computer Science, 25(4):841-866, 2015. URL: https://doi.org/10.1017/S0960129513000054.
  29. Georg Zetzsche. An approach to computing downward closures. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 440-451. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_35.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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