Fixpoint constructions in focused orthogonality models of linear logic
Marcelo Fiore, Zeinab Galal, Farzad Jafarrahmani
TL;DR
The paper addresses how to construct models of linear logic that support both least and greatest fixpoints within focused orthogonality, by lifting initial algebras and final coalgebras through relational fibrations to focused orthogonality categories. It develops a general lifting theory, including induction- and coinduction-style principles, and provides a representation theorem that recasts focused orthogonality as a Grothendieck construction over indexed complete lattices with existential quantification. The work unifies and extends existing totality and phase-space models, and demonstrates applicability to a broad class of models, including probabilistic coherence spaces and domain-theoretic settings, enabling new fully complete and fixpoint-enabled interpretations. Overall, it offers a systematic categorical method to build LL models with $μ$- and $ν$-fixpoints and paves the way for further applications in double glueing, domain theory, and fully complete semantics.
Abstract
Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This paper considers the subclass of focused orthogonalities. We develop a theory of fixpoint constructions in focused orthogonality categories. Central results are lifting theorems for initial algebras and final coalgebras. These crucially hinge on the insight that focused orthogonality categories are relational fibrations. The theory provides an axiomatic categorical framework for models of linear logic with least and greatest fixpoints of types. We further investigate domain-theoretic settings, showing how to lift bifree algebras, used to solve mixed-variance recursive type equations, to focused orthogonality categories.