A proof theory of right-linear (ω-)grammars via cyclic proofs

Anupam Das; Abhishek De

doi:10.1145/3661814.3662138

A proof theory of right-linear (ω-)grammars via cyclic proofs

Anupam Das^*
, Abhishek De

^*Corresponding author for this work

Computer Science

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

46 Downloads (Pure)

Abstract

Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with least fixed points but with products restricted to letters as left arguments, giving an alternative to the syntax of regular expressions. In this work, we investigate the resulting logical theory of this syntax. Namely, we propose a theory of right-linear algebras (RLA) over this syntax and a cyclic proof system CRLA for reasoning about them.We show that CRLA is sound and complete for the intended model of regular languages. From here we recover the same completeness result for RLA by extracting inductive invariants from cyclic proofs. Finally, we extend CRLA by greatest fixed points, vCRLA, naturally modelled by languages of ω-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) vCRLA for the model of ω-regular languages, this time requiring game theoretic techniques to handle the interleaving of fixed points.

Original language	English
Title of host publication	LICS '24
Subtitle of host publication	Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
ISBN (Electronic)	9798400706608
DOIs	https://doi.org/10.1145/3661814.3662138
Publication status	Published - 8 Jul 2024
Event	39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024 - Tallinn, Estonia Duration: 8 Jul 2024 → 11 Jul 2024

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
ISSN (Print)	1043-6871

Conference

Conference	39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024
Country/Territory	Estonia
City	Tallinn
Period	8/07/24 → 11/07/24

Bibliographical note

Publisher Copyright:
© 2024 Institute of Electrical and Electronics Engineers Inc.. All rights reserved.

Keywords

automata theory
cyclic proofs
fixed points
games
linear grammars
proof theory
regular languages

ASJC Scopus subject areas

Software
General Mathematics

Access to Document

10.1145/3661814.3662138Licence: Creative Commons: Attribution (CC BY)

DasA2024ProofFinal published version, 730 KBLicence: Creative Commons: Attribution (CC BY)

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

Cite this

@inproceedings{3bb26626bfce4321acfbdaef9468dc7d,

title = "A proof theory of right-linear (ω-)grammars via cyclic proofs",

abstract = "Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with least fixed points but with products restricted to letters as left arguments, giving an alternative to the syntax of regular expressions. In this work, we investigate the resulting logical theory of this syntax. Namely, we propose a theory of right-linear algebras (RLA) over this syntax and a cyclic proof system CRLA for reasoning about them.We show that CRLA is sound and complete for the intended model of regular languages. From here we recover the same completeness result for RLA by extracting inductive invariants from cyclic proofs. Finally, we extend CRLA by greatest fixed points, vCRLA, naturally modelled by languages of ω-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) vCRLA for the model of ω-regular languages, this time requiring game theoretic techniques to handle the interleaving of fixed points.",

keywords = "automata theory, cyclic proofs, fixed points, games, linear grammars, proof theory, regular languages",

author = "Anupam Das and Abhishek De",

note = "Publisher Copyright: {\textcopyright} 2024 Institute of Electrical and Electronics Engineers Inc.. All rights reserved.; 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024 ; Conference date: 08-07-2024 Through 11-07-2024",

year = "2024",

month = jul,

day = "8",

doi = "10.1145/3661814.3662138",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

booktitle = "LICS '24",

}

Das, A & De, A 2024, A proof theory of right-linear (ω-)grammars via cyclic proofs. in LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science., 30, Proceedings - Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers (IEEE), 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, 8/07/24. https://doi.org/10.1145/3661814.3662138

A proof theory of right-linear (ω-)grammars via cyclic proofs. / Das, Anupam; De, Abhishek.
LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science. Institute of Electrical and Electronics Engineers (IEEE), 2024. 30 (Proceedings - Symposium on Logic in Computer Science).

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

TY - GEN

T1 - A proof theory of right-linear (ω-)grammars via cyclic proofs

AU - Das, Anupam

AU - De, Abhishek

PY - 2024/7/8

Y1 - 2024/7/8

N2 - Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with least fixed points but with products restricted to letters as left arguments, giving an alternative to the syntax of regular expressions. In this work, we investigate the resulting logical theory of this syntax. Namely, we propose a theory of right-linear algebras (RLA) over this syntax and a cyclic proof system CRLA for reasoning about them.We show that CRLA is sound and complete for the intended model of regular languages. From here we recover the same completeness result for RLA by extracting inductive invariants from cyclic proofs. Finally, we extend CRLA by greatest fixed points, vCRLA, naturally modelled by languages of ω-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) vCRLA for the model of ω-regular languages, this time requiring game theoretic techniques to handle the interleaving of fixed points.

AB - Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with least fixed points but with products restricted to letters as left arguments, giving an alternative to the syntax of regular expressions. In this work, we investigate the resulting logical theory of this syntax. Namely, we propose a theory of right-linear algebras (RLA) over this syntax and a cyclic proof system CRLA for reasoning about them.We show that CRLA is sound and complete for the intended model of regular languages. From here we recover the same completeness result for RLA by extracting inductive invariants from cyclic proofs. Finally, we extend CRLA by greatest fixed points, vCRLA, naturally modelled by languages of ω-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) vCRLA for the model of ω-regular languages, this time requiring game theoretic techniques to handle the interleaving of fixed points.

KW - automata theory

KW - cyclic proofs

KW - fixed points

KW - games

KW - linear grammars

KW - proof theory

KW - regular languages

UR - https://www.scopus.com/pages/publications/85199034671

U2 - 10.1145/3661814.3662138

DO - 10.1145/3661814.3662138

M3 - Conference contribution

AN - SCOPUS:85199034671

T3 - Proceedings - Symposium on Logic in Computer Science

BT - LICS '24

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024

Y2 - 8 July 2024 through 11 July 2024

ER -

A proof theory of right-linear (ω-)grammars via cyclic proofs

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Projects

Structure vs. Invariants in Proofs (StrIP)

Cite this