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方程系统的线性λ-理论构成一个范畴，该范畴等价于基于"广义度量空间"丰富的自洽范畴。将此结果实例化为不等式情形时，可得到与基于偏序集丰富的自洽范畴的等价性；在（超）度量方程情形下，则得到与基于（超）度量空间丰富的自洽范畴的等价性。此外，我们还证明这种语法-语义对应关系可推广至仿射设定。基于这些结果，我们为实时计算、概率计算和量子计算中的高阶编程开发了不等式和度量方程系统的实例。