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.

翻译：我们从不同数学传统中识别出两种构造。在线性逻辑与可实现性中，逻辑类型并非预先给定而是生成的：从一个配备执行（execution）的可实现者（realiser）全域出发，利用正交性（orthogonality）检验其交互，并将类型取为双正交闭子集。在富化的Isbell对偶中，一个定量关系诱导出一个伴随（adjunction），其不动点形成一个范畴——即它的核（nucleus）。这两种构造采用不同方式；我们证明在当前设定下它们产生相同的对象。共享的数据是最小化的：一个称为执行的结合性积，以及一个实值度量，两者之间不假定任何相容性。度量的非可加性同时是定义正交性的关系，以及我们据此形成Isbell核的定量关系；而由正交性切割出的类型恰好是相应伴随的不动点。这一识别在两个方向上均有收益。最自然的类型积缺乏结合性；弥补这一缺陷迫使引入一种不同类型的类型——它对复合物的两侧均敏感——在此之上诱导的积是结合的，且当执行具有单位元时，它承载两个剩余（residuals）。由此涌现出一个非交换的Lambek演算，它直接从执行与正交性导出而非外加。反向而言，每一个这样的类型（在范畴侧解读）会生成它自身的定量关系，并随之产生一个导出伴随以及进一步的类型生成；这些导出类型再次成为原始情境中的类型，由Lambek演算的剩余计算得出。我们还证明了该构造三重排列的连贯性定理，并在有限维情形下给出了积的显式公式。