Volume 194, Issue 2: Fixed Points in Computer Science 2023
Fixed Points in Computer Science 2023
1. Relative fixed points of functors
We show how the relatively initial or relatively terminal fixed points for a well-behaved functor $F$ form a pair of adjoint functors between $F$-coalgebras and $F$-algebras. We use the language of locally presentable categories to find sufficient conditions for existence of this adjunction. We show that relative fixed points may be characterized as (co)equalizers of the free (co)monad on $F$. In particular, when $F$ is a polynomial functor on $\mathsf{Set}$ the relative fixed points are a quotient or subset of the free term algebra or the cofree term coalgebra. We give examples of the relative fixed points for polynomial functors and an example which is the Sierpinski carpet. Lastly, we prove a general preservation result for relative fixed points.
2. Peano Arithmetic and $μ$MALL
Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use $μ$MALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear logic (MALL) with the addition of the logical connectives universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using $μ$MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $μ$MALL, we obtain $μ$LK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $μ$LK+ (including cut-elimination and the completeness of focusing), we prove that $μ$LK+ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding $μ$LK+ over $μ$MALL.
3. Demystifying $μ$
We explore the theory of illfounded and cyclic proofs for the propositional modal $μ$-calculus. A fine analysis of provability for classical and intuitionistic modal logic provides a novel bridge between finitary, cyclic and illfounded conceptions of proof and re-enforces the importance of two normal form theorems for the logic: guardedness and disjunctiveness.