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.
翻译:本文提出一种紧凑方法,将Mellies-Tabareau-Tasson的自由指数构造提升到Hyland-Schalk适用于正交范畴的双胶合框架上。我们提出一个足够简洁的"正交互惠"条件,使得自由指数能以正交性为基础在双胶合上提升。该通用方法适用于具有可数双积的s-有限转移核构成的幺半范畴TsK。我们证明:(i)TsK^op具有自由指数,且该指数可用测度论术语描述;(ii)s-有限转移核在测度与可测函数之间具有基于勒贝格积分的正交关系。该正交关系满足互惠性,因此(i)中的自由指数可提升至正交范畴O_I(TsK^op),后者将Ehrhard等人的概率相干空间作为可数可测空间的全子范畴包含进来。在提升自由指数过程中,涉及勒贝格积分与极限交换的测度论一致收敛定理,以及s-有限性条件下双重积分的Fubini-Tonelli定理均起到关键作用。本文提出的测度论正交性可视为线性逻辑概率相干空间正交性的连续版本,特别地,它为Crubille等人针对该类空间直接构造的自由指数提供了双层分解结构。