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