广义度量空间 enrichment 的自治范畴的语形侧面

具有连续状态空间或与物理过程交互的程序往往需要超越标准二元设定的等价概念，在标准设定中等价要么成立要么不成立。在本文中，我们探讨取价值于 quantale V 的等价思想，它涵盖了（不）等式与（超）度量等式等情形。我们的主要结果是引入线性 {\lambda}-演算的 V-等式演绎系统，并证明其可靠且完备。事实上我们更进一步，证明基于该 V-等式系统的线性 {\lambda}-理论构成一个范畴，它等价于一个在“广义度量空间”上 enrichment 的自治范畴的范畴。若将此结果实例化为不等式，则得到与在偏序上 enrichment 的自治范畴的等价；在（超）度量等式情形下，得到与在（超）度量空间上 enrichment 的自治范畴的等价。我们额外展示了该语形-语义对应可推广至仿射设定。我们利用所得结果开发了实时、概率与量子计算设定下用于高阶编程的不等式与度量等式系统的实例。