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 the 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. 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等人的概率相干空间作为可数可测空间的满子范畴包含在内。自由指数的提升过程中,测度论中勒贝格积分与极限交换的一致收敛定理发挥了关键作用。本文提出的测度论正交性可视为线性逻辑概率相干空间正交性的连续版本,特别地,它为Crubille等人针对这些空间构造的直接自由指数提供了双层分解结构。