Decision Problems for Linear Logic with Least and Greatest Fixed Points

Anupam Das; Abhishek De; Alexis Saurin

doi:10.4230/LIPIcs.FSCD.2022.20

Decision Problems for Linear Logic with Least and Greatest 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

1 Citation (Scopus)

27 Downloads (Pure)

Abstract

Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting “infinitary” behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (µMALL), in particular, recent systems based on “circular” and “non-wellfounded” reasoning. In this paper, we show that µMALL is undecidable.

More explicitly, we show that the general non-wellfounded system is Π⁰₁-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ⁰₁). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ⁰₁-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ⁰₁-complete.

Original language	English
Title of host publication	7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Editors	Amy P. Felty
Publisher	Schloss Dagstuhl
Number of pages	20
ISBN (Electronic)	9783959772334
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2022.20
Publication status	Published - 28 Jun 2022
Event	7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 - Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Publisher	Schloss Dagstuhl
Volume	228
ISSN (Electronic)	1868-8969

Conference

Conference	7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
Country/Territory	Israel
City	Haifa
Period	2/08/22 → 5/08/22

Bibliographical note

Funding Information:
Funding Anupam Das: This author is supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1. Abhishek De: This author has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 754362. Alexis Saurin: This author has been partially supported by ANR project RECIPROG, project reference ANR-21-CE48-019-01.

Publisher Copyright:
© Anupam Das Abhishek De and Alexis Saurin

Keywords

decidability
fixed points
Linear logic
vector addition systems

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.FSCD.2022.20Licence: Creative Commons: Attribution (CC BY)

DasA2022DecisionFinal published version, 884 KBLicence: Creative Commons: Attribution (CC BY)

Structure vs. Invariants in Proofs (StrIP)
Das, A.
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

@inproceedings{9df20987f04e4561980ed9b4dee9bdc8,

title = "Decision Problems for Linear Logic with Least and Greatest Fixed Points",

abstract = "Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting “infinitary” behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (µMALL), in particular, recent systems based on “circular” and “non-wellfounded” reasoning. In this paper, we show that µMALL is undecidable. More explicitly, we show that the general non-wellfounded system is Π01-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ01). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ01-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ01-complete.",

keywords = "decidability, fixed points, Linear logic, vector addition systems",

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

note = "Funding Information: Funding Anupam Das: This author is supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1. Abhishek De: This author has received funding from the European Union{\textquoteright}s Horizon 2020 research and innovation programme under the Marie Sk{\l}odowska-Curie grant agreement No 754362. Alexis Saurin: This author has been partially supported by ANR project RECIPROG, project reference ANR-21-CE48-019-01. Publisher Copyright: {\textcopyright} Anupam Das Abhishek De and Alexis Saurin; 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 ; Conference date: 02-08-2022 Through 05-08-2022",

year = "2022",

month = jun,

day = "28",

doi = "10.4230/LIPIcs.FSCD.2022.20",

language = "English",

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

publisher = "Schloss Dagstuhl",

editor = "Felty, {Amy P.}",

booktitle = "7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)",

address = "Germany",

}

Das, A, De, A & Saurin, A 2022, Decision Problems for Linear Logic with Least and Greatest Fixed Points. in AP Felty (ed.), 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)., 20, Leibniz International Proceedings in Informatics, LIPIcs, vol. 228, Schloss Dagstuhl, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, Haifa, Israel, 2/08/22. https://doi.org/10.4230/LIPIcs.FSCD.2022.20

Decision Problems for Linear Logic with Least and Greatest Fixed Points. / Das, Anupam; De, Abhishek; Saurin, Alexis.
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). ed. / Amy P. Felty. Schloss Dagstuhl, 2022. 20 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 228).

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

TY - GEN

T1 - Decision Problems for Linear Logic with Least and Greatest Fixed Points

AU - Das, Anupam

AU - De, Abhishek

AU - Saurin, Alexis

N1 - Funding Information: Funding Anupam Das: This author is supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1. Abhishek De: This author has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 754362. Alexis Saurin: This author has been partially supported by ANR project RECIPROG, project reference ANR-21-CE48-019-01. Publisher Copyright: © Anupam Das Abhishek De and Alexis Saurin

PY - 2022/6/28

Y1 - 2022/6/28

N2 - Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting “infinitary” behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (µMALL), in particular, recent systems based on “circular” and “non-wellfounded” reasoning. In this paper, we show that µMALL is undecidable. More explicitly, we show that the general non-wellfounded system is Π01-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ01). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ01-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ01-complete.

AB - Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting “infinitary” behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (µMALL), in particular, recent systems based on “circular” and “non-wellfounded” reasoning. In this paper, we show that µMALL is undecidable. More explicitly, we show that the general non-wellfounded system is Π01-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ01). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ01-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ01-complete.

KW - decidability

KW - fixed points

KW - Linear logic

KW - vector addition systems

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

U2 - 10.4230/LIPIcs.FSCD.2022.20

DO - 10.4230/LIPIcs.FSCD.2022.20

M3 - Conference contribution

AN - SCOPUS:85133678281

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

A2 - Felty, Amy P.

PB - Schloss Dagstuhl

T2 - 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022

Y2 - 2 August 2022 through 5 August 2022

ER -

Decision Problems for Linear Logic with Least and Greatest Fixed Points

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Projects

Structure vs. Invariants in Proofs (StrIP)

Cite this