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等人针对这些空间定义的直接自由指数提供了一个双层分解。