In this work, we prove the undecidability (and Σ⁰₁-completeness) of several theories of semirings with fixed points. The generality of our results stems from recursion theoretic methods, namely the technique of effective inseparability. Our result applies to many theories proposed in the literature, including Conway μ-semirings, Park μ-semirings, and Chomsky algebras.

Alternating parity automata (APAs) provide a robust formalism for modelling infinite behaviours and play a central role in formal verification. Despite their widespread use, the algebraic theory underlying APAs has remained largely unexplored. In recent work [10], a notation for non-deterministic finite automata (NFAs) was introduced, along with a sound and complete axiomatisation of their equational theory via right-linear algebras. In this paper, we extend that line of work to the setting of infinite words. In particular, we present a dualised syntax, yielding a notation for APAs based on right-linear lattice expressions, and provide a natural axiomatisation of their equational theory with respect to the standard language model of ω-regular languages. The design of this axiomatisation is guided by the theory of fixed point logics; in fact, the completeness factors cleanly through the completeness of the linear-time µ-calculus.

Abstract $$\omega $$ ω -regular languages are a natural extension of the regular languages to the setting of infinite words. Likewise, they are recognised by a host of automata models, one of the most important being Alternating Parity Automata (APAs), a generalisation of Büchi automata that symmetrises both the transitions (with universal as well as existential branching) and the acceptance condition (by a parity condition). In this work, we develop a cyclic proof system manipulating APAs, represented by an algebraic notation of Right Linear Lattice expressions. This syntax dualises that of previously introduced Right Linear Algebras, which comprised a notation for non-deterministic finite automata. Our main result is the soundness and completeness of our system for $$\omega $$ ω -language inclusion, heavily exploiting game-theoretic techniques from the theory of $$\omega $$ ω -regular languages.

Abstract We investigate the proof theory of regular expressions with fixed points, construed as a notation for ( $$\omega $$ ω -)context-free grammars. Starting with a hypersequential system for regular expressions due to Das and Pous [15], we define its extension by least fixed points and prove the soundness and completeness of its non-wellfounded proofs for the standard language model. From here we apply proof-theoretic techniques to recover an infinitary axiomatisation of the resulting equational theory, complete for inclusions of context-free languages. Finally, we extend our syntax by greatest fixed points, now computing $$\omega $$ ω -context-free languages. We show the soundness and completeness of the corresponding system using a mixture of proof-theoretic and game-theoretic techniques.

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.

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 (μMALL^∞) vs. infinitely branching well-founded proofs (μMALL_{ω,∞}). Our main result is that μMALL^∞ is strictly contained in μMALL_{ω,∞}. 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 μMALL^∞ provability from Π⁰₁-hard to Σ¹₁-hard, by encoding a sort of Büchi condition for Minsky machines.

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.

The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (μMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this paper, we extend the phase semantics of multiplicative additive linear logic (a.k.a. MALL) to μMALL with explicit (co)induction (i.e. μMALL^{ind}). We introduce a Tait-style system for μMALL called μMALL_ω where proofs are wellfounded but potentially infinitely branching. We study its phase semantics and prove that it does not have the finite model property.

Non-wellfounded and circular proofs have been recognised over the past decade as a valuable tool to study logics expressing (co)inductive properties, e.g. μ-calculi. Such proofs are non-wellfounded sequent derivations together with a global validity condition expressed in terms of progressing threads. While the cut-free fragment of circular proofs is satisfactory, cuts are poorly treated and the non-canonicity of sequent proofs becomes a major issue in the non-wellfounded setting. The present paper develops for (multiplicative linear logic with fixed points) the theory of infinets – proof-nets for non-wellfounded proofs. Our structures handles infinitely many cuts therefore solving a crucial shortcoming of the previous work [19]. We characterise correctness, define a more complete cut-reduction system and proving a cut-elimination theorem. To that end, we also provide an alternate cut reduction for non-wellfounded sequent calculus.