Double Glueing over Free Exponential: with Measure Theoretic Applications

TL;DR

This paper introduces a measure-theoretic method to lift the free exponential construction over double glueing in orthogonality categories, with applications to s-finite transition kernels and probabilistic coherent spaces.

Contribution

It presents a new measure-theoretic approach to lift free exponential constructions in orthogonality categories, extending to s-finite kernels and probabilistic spaces.

Findings

TsK^op has the free exponential described via measure theory

Orthogonality between measures and functions is reciprocal in TsK

The lifted free exponential subsumes probabilistic coherent spaces

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.