Double Glueing over Free Exponential: with Measure Theoretic Applications
Masahiro Hamano
TL;DR
The paper develops a two-pronged approach to modelling linear logic exponentials: abstract lifting of the free exponential via reciprocity of focused orthogonality in a double-glueing setting, and a measure-theoretic realization using s-finite transition kernels. It first builds a general lifting framework for the free exponential in an orthogonality category ${\bf O}_J(\mathcal{C})$, then develops the monoidal category ${\sf TsK}$ of s-finite kernels with countable biproducts and constructs the free exponential in ${\sf TsK}^{\text{op}}$. The core contribution is the measure-theoretic orthogonality category ${\bf O}_{\mathcal I}({\sf TsK}^{\text{op}})$, where a focused orthogonality between measures and measurable functions is shown to be reciprocal and compatible with the equalizers and limits that define the exponential; this yields a continuous analogue of the probabilistic coherent spaces and provides a two-layered decomposition of Crubillé et al.'s direct free exponential. The discretisation of this framework recovers Crubillé– Ehrhard–Pagani–Tasson results for probabilistic coherent spaces, thereby connecting a continuous measure-theoretic model with established discrete denotational semantics. Overall, the work advances a cohesive bridge between categorical double-glueing constructions and measure-theoretic semantics for linear logic exponentials, highlighting key theorems (e.g., reciprocity-driven lifting and Fubini–Tonelli-based distribution) and paving the way for a closed structure in the measure-theoretic setting.
Abstract
This paper provides a compact method to lift the free exponential construction of Mellies-Tabareau-Tasson over the Hyland-Schalk double glueing for orthogonality categories. A condition ``reciprocity of orthogonality'' is presented simply enough to lift the free exponential over the double glueing in terms of the orthogonality. Our general method applies to the monoidal category TsK of the s-finite transition kernels with countable biproducts. We show (i) TsK^op has the free exponential, which is shown to be describable in terms of measure theory. (ii) The s-finite transition kernels have an orthogonality between measures and measurable functions in terms of Lebesgue integrals. The orthogonality is reciprocal, hence the free exponential of (i) lifts to the orthogonality category O_I(TsK^op), which subsumes Ehrhard et al's probabilistic coherent spaces as a full subcategory of countable measurable spaces. To lift the free exponential, the measure-theoretic uniform convergence theorem commuting Lebesgue integral and limit plays a crucial role as well as Fubini-Tonelli theorem for double integral in s-finiteness. Our measure-theoretic orthogonality is considered as a continuous version of the orthogonality of the probabilistic coherent spaces for linear logic, and in particular provides a two layered decomposition of Crubille et al's direct free exponential for these spaces.