Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2022.112
URN: urn:nbn:de:0030-drops-164533
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16453/
Barozzini, David ; Parys, Paweł ; Wróblewski, Jan
Unboundedness for Recursion Schemes: A Simpler Type System
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{barozzini_et_al:LIPIcs.ICALP.2022.112,
author = {Barozzini, David and Parys, Pawe{\l} and Wr\'{o}blewski, Jan},
title = {{Unboundedness for Recursion Schemes: A Simpler Type System}},
booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
pages = {112:1--112:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-235-8},
ISSN = {1868-8969},
year = {2022},
volume = {229},
editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16453},
URN = {urn:nbn:de:0030-drops-164533},
doi = {10.4230/LIPIcs.ICALP.2022.112},
annote = {Keywords: Higher-order recursion schemes, boundedness, intersection types, safe schemes}
}
| Keywords: | Higher-order recursion schemes, boundedness, intersection types, safe schemes | |
| Seminar: | 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 28.06.2022 | |
| Supplementary Material: |
Implementation of the presented algorithm is available at: Software (Source Code): https://github.com/xi-business/infsat archived at: https://archive.softwareheritage.org/swh:1:dir:075c57b341bf44dc0abeb89fe48ed8aec1691828 |
