Isbell 核中的类型演算
A calculus of types in Isbell nuclei
AI总结：
本文证明线性逻辑中的双正交闭包与富化Isbell对偶中的核构造在给定最小数据（执行乘积和实值度量）下产生相同对象，并由此导出非交换Lambek演算。
摘要：
我们识别了来自不同数学传统的两种构造。在线性逻辑和实现性中，逻辑类型是生成的而非预先固定的：从一个配备执行（execution）的实现者宇宙开始，使用正交性测试它们的交互，并将类型取为双正交闭子集。在富化Isbell对偶中，一个定量关系诱导一个伴随，其不动点构成一个范畴，即它的核。这些构造通过不同方式进行；我们证明，在当前设定下，它们产生相同的对象。共享的数据是最小的：一个称为执行的结合性乘积，以及一个实值度量，两者之间不假设任何兼容性。度量非加性这一点同时是定义正交性的关系以及我们形成其Isbell核的定量关系，而由正交性切割出的类型恰好是相关伴随的不动点。这一识别在双向都有收益。最自然的类型乘积不满足结合性；修复这一缺陷迫使采用不同的类型概念，对复合的两侧都敏感，使得诱导的乘积是结合的，并且当执行有单位时，携带两个余项。由此产生的是一个非交换的Lambek演算，直接从执行和正交性导出而非强加。在反向方向上，每个这样的类型，从范畴侧解读，生成它自己的定量关系，并随之产生一个导出的伴随和进一步的类型生成；这些导出的类型再次是原始情况的类型，由Lambek演算的余项计算。我们还证明了这一构造的三重排列的相干定理，并在有限维情形下给出了乘积的显式公式。
英文摘要：
We identify two constructions from different mathematical traditions. In linear logic and realisability, logical types are generated rather than fixed in advance: one begins with a universe of realisers equipped with execution, uses orthogonality to test their interactions, and takes types to be the biorthogonally closed subsets. In enriched Isbell duality, a quantitative relation induces an adjunction whose fixed points form a category, its nucleus. These constructions proceed by different means; we show that, in the present setting, they produce the same objects. The shared datum is minimal: an associative product, called execution, and a real-valued measurement, with no compatibility assumed between them. The failure of the measurement to be additive is at once the relation defining orthogonality and the quantitative relation whose Isbell nucleus we form, and the types cut out by orthogonality are exactly the fixed points of the associated adjunction. The identification pays off in both directions. The most natural product of types fails to be associative; repairing this failure forces a different notion of type, sensitive to both sides of a composite, on which the induced product is associative and, when execution has units, carries two residuals. What emerges is a noncommutative Lambek calculus, derived directly from execution and orthogonality rather than imposed. In the reverse direction, each such type, read on the categorical side, generates a quantitative relation of its own, and with it a derived adjunction and a further generation of types; these derived types are again types of the original situation, computed by the residuals of the Lambek calculus. We also prove a coherence theorem for the threefold arrangements of this construction and, in the finite-dimensional case, give explicit formulas for the product.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
