论文标题
自主类别的句法一面富含广义度量空间
The syntactic side of autonomous categories enriched over generalised metric spaces
论文作者
论文摘要
具有连续状态空间或与物理过程相互作用的程序通常需要等价概念超出等价持有或不存在的标准二进制设置。在本文中，我们探讨了在量化V中取值的等效性的想法，该量子涵盖了（in）方程式和（Ultra）度量方程式的情况。我们的主要结果是引入了线性λ-calculus的V-均等演绎系统，以及证明其声音和完整的证明。实际上，我们远远超过了这一点，通过表明基于此V平等系统的线性λ理论形成了一种类别，其等效于富含“广义度量空间”的自主类别类别。如果我们将此结果实例化，则将获得与部分订单相当的自主类别。在（超）度量方程式的情况下，我们获得了富含（Ultra）度量空间的自主类别的等效性。我们还表明，这种语法 - 符号对应关系扩展到仿射设置。我们利用结果来开发实时，概率和量子计算的设置的不平衡和度量方程系统的示例。
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear λ-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear λ-theories based on this V-equational system form a category that is equivalent to a category of autonomous categories enriched over 'generalised metric spaces'. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. We additionally show that this syntax-semantics correspondence extends to the affine setting. We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing.
