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.

翻译：具有连续状态空间或与物理过程交互的程序，往往需要超越标准二值等价（即等价要么成立要么不成立）的等价概念。本文探索了取值于量子格V中的等价概念，涵盖了(不)等式和(超)度量方程等情形。主要成果是为线性λ-演算引入了V-等式演绎系统，并证明其可靠性与完备性。更进一步，我们证明了基于该V-等式系统的线性λ-理论构成一个范畴，该范畴等价于在"广义度量空间"上丰富的自主范畴范畴。将此结果实例化为不等式情形时，我们得到与偏序集上丰富自主范畴的等价性；在(超)度量方程情形下，则得到与(超)度量空间上丰富自主范畴的等价性。我们还证明此句法-语义对应关系可推广至仿射设定。利用这些结果，我们为实时计算、概率计算和量子计算中的高阶编程开发了不等式和度量方程系统的实例。