一句话：为线性λ演算引入取值于quantale的V-等式演绎系统，证明其可靠完备，并建立其理论与广义度量空间富集自治范畴的等价。
许多程序具有连续状态空间或需与物理过程交互，其行为等价常非简单二值关系，而需取不等式、(超)度量等式等更一般的值。本文研究等价取值于quantale V的情形，为线性λ演算引入V-等式演绎系统，并证明其相对于广义度量空间富集的自治范畴可靠且完备。进一步，作者证明基于该系统的线性λ理论构成范畴，并与广义度量空间富集的自治范畴等价。实例化到不等式得到偏序富集的自治范畴；实例化到(超)度量等式得到(超)度量空间富集的自治范畴；对应还可推广到affine情形。最后在实时、概率与量子计算中给出高阶编程的不等式与度量等式系统实例。
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 {\lambda}-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear {\lambda}-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.
@article{paperbot2169,
title = {The syntactic side of autonomous categories enriched over generalised metric spaces},
author = {Fredrik Dahlqvist and Renato Neves},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:31)2023}
}