Lax Modal Lambda Calculi
Nachiappan Valliappan
TL;DR
This work develops a rigorous foundation for lax modal lambda calculi by introducing SLC, RLC, and JLC as sublogics of LL, aligned with subcategories of modal axioms S, R, and J. It pairs these calculi with both possible-world (presheaf-based) and categorical semantics, and delivers constructive normalization through Normalization by Evaluation (NbE) with proof-relevant semantics implemented in Agda. The results include normalization, equational completeness, and inadmissibility theorems for the lax modalities, as well as a unifying semantic framework connecting sublogics to strong functors, pointed functors, and semimonads. Together, these contributions clarify the computational interpretation of lax diamonds and provide a solid semantic and syntactic toolkit for reasoning about non-monadic strong functors in typed functional programming.
Abstract
Intuitionistic modal logics (IMLs) extend intuitionistic propositional logic with modalities such as the box and diamond connectives. Advances in the study of IMLs have inspired several applications in programming languages via the development of corresponding type theories with modalities. Until recently, IMLs with diamonds have been misunderstood as somewhat peculiar and unstable, causing the development of type theories with diamonds to lag behind type theories with boxes. In this article, we develop a family of typed-lambda calculi corresponding to sublogics of a peculiar IML with diamonds known as Lax logic. These calculi provide a modal logical foundation for various strong functors in typed-functional programming. We present possible-world and categorical semantics for these calculi and constructively prove normalization, equational completeness and proof-theoretic inadmissibility results. Our main results have been formalized using the proof assistant Agda.