Comparing Infinitary Systems for Linear Logic with Fixed Points

Anupam Das; Abhishek De; Alexis Saurin

doi:10.4230/LIPIcs.FSTTCS.2023.40

Comparing Infinitary Systems for Linear Logic with Fixed Points

Anupam Das^*, Abhishek De^*, Alexis Saurin^*

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

14 Downloads (Pure)

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	https://doi.org/10.4230/LIPIcs.FSTTCS.2023.40
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

Access to Document

10.4230/LIPIcs.FSTTCS.2023.40Licence: Creative Commons: Attribution (CC BY)

DasA2023ComparingFinal published version, 881 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

Das, A., De, A., & Saurin, A. (2023). Comparing Infinitary Systems for Linear Logic with Fixed Points. In P. Bouyer, S. Srinivasan, & S. Srinivasan (Eds.), 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023) (pp. 40:1-40:17). Article 37 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 284). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.FSTTCS.2023.40

Das, Anupam ; De, Abhishek ; Saurin, Alexis. / Comparing Infinitary Systems for Linear Logic with Fixed Points. 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). editor / Patricia Bouyer ; Srikanth Srinivasan ; Srikanth Srinivasan. Schloss Dagstuhl, 2023. pp. 40:1-40:17 (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{ced8e9c33b1a4c0eb4de238af6438b70,

title = "Comparing Infinitary Systems for Linear Logic with Fixed Points",

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{\"u}chi condition for Minsky machines.",

keywords = "analytical hierarchy, fixed points, linear logic, non-wellfounded proofs, omega-branching proofs",

author = "Anupam Das and Abhishek De and Alexis Saurin",

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: {\textcopyright} 2023 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.; 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023 ; Conference date: 18-12-2023 Through 20-12-2023",

year = "2023",

month = dec,

day = "12",

doi = "10.4230/LIPIcs.FSTTCS.2023.40",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl",

pages = "40:1--40:17",

editor = "Patricia Bouyer and Srikanth Srinivasan and Srikanth Srinivasan",

booktitle = "43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)",

address = "Germany",

}

Das, A , De, A & Saurin, A 2023, Comparing Infinitary Systems for Linear Logic with Fixed Points. in P Bouyer, S Srinivasan & S Srinivasan (eds), 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)., 37, Leibniz International Proceedings in Informatics, LIPIcs, vol. 284, Schloss Dagstuhl, pp. 40:1-40:17, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023, Hyderabad, India, 18/12/23. https://doi.org/10.4230/LIPIcs.FSTTCS.2023.40

Comparing Infinitary Systems for Linear Logic with Fixed Points. / Das, Anupam ; De, Abhishek; Saurin, Alexis.
43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). ed. / Patricia Bouyer; Srikanth Srinivasan; Srikanth Srinivasan. Schloss Dagstuhl, 2023. p. 40:1-40:17 37 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 284).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Comparing Infinitary Systems for Linear Logic with Fixed Points

AU - Das, Anupam

AU - De, Abhishek

AU - Saurin, Alexis

N1 - 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.

PY - 2023/12/12

Y1 - 2023/12/12

N2 - 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.

AB - 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.

KW - analytical hierarchy

KW - fixed points

KW - linear logic

KW - non-wellfounded proofs

KW - omega-branching proofs

UR - http://www.scopus.com/inward/record.url?scp=85180745965&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSTTCS.2023.40

DO - 10.4230/LIPIcs.FSTTCS.2023.40

M3 - Conference contribution

AN - SCOPUS:85180745965

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 40:1-40:17

BT - 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

A2 - Bouyer, Patricia

A2 - Srinivasan, Srikanth

PB - Schloss Dagstuhl

T2 - 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023

Y2 - 18 December 2023 through 20 December 2023

ER -

Das A , De A, Saurin A. Comparing Infinitary Systems for Linear Logic with Fixed Points. In Bouyer P, Srinivasan S, Srinivasan S, editors, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Schloss Dagstuhl. 2023. p. 40:1-40:17. 37. (Leibniz International Proceedings in Informatics, LIPIcs). doi: 10.4230/LIPIcs.FSTTCS.2023.40