Abstract
Extensions of Girard's linear logic by least and greatest fixed point operators (µMALL) have been an active field of research for almost two decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this paper, we compare the relative expressivity, at the level of provability, of two complementary infinitary proof systems: finitely branching non-wellfounded proofs (µMALL8) vs. infinitely branching well-founded proofs (µMALL?,8). Our main result is that µMALL8 is strictly contained in µMALL?,8. For inclusion, we devise a novel technique involving infinitary rewriting of non-wellfounded proofs that yields a wellfounded proof in the limit. For strictness of the inclusion, we improve previously known lower bounds on µMALL8 provability from ?01 -hard to S11 -hard, by encoding a sort of Büchi condition for Minsky machines.
Original language | English |
---|---|
Title of host publication | 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023) |
Editors | Patricia Bouyer, Srikanth Srinivasan, Srikanth Srinivasan |
Publisher | Schloss Dagstuhl |
Pages | 40:1-40:17 |
ISBN (Electronic) | 9783959773041 |
DOIs | |
Publication status | Published - 12 Dec 2023 |
Event | 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023 - Hyderabad, India Duration: 18 Dec 2023 → 20 Dec 2023 |
Publication series
Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 284 |
ISSN (Print) | 1868-8969 |
Conference
Conference | 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023 |
---|---|
Country/Territory | India |
City | Hyderabad |
Period | 18/12/23 → 20/12/23 |
Bibliographical note
Funding Information:Funding The first and second authors are supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1. The third author is partially funded by the ANR project RECIPROG, project reference ANR-21-CE48-019-01.
Publisher Copyright:
© 2023 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.
Keywords
- analytical hierarchy
- fixed points
- linear logic
- non-wellfounded proofs
- omega-branching proofs
ASJC Scopus subject areas
- Software