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