Modern programming frequently requires generalised notions of program equivalence based on a metric or a similar structure. Previous work addressed this challenge by introducing the notion of a V-equation, i.e. an equation labelled by an element of a quantale V, which covers inter alia (ultra-)metric, classical, and fuzzy (in)equations. It also introduced a V-equational system for the linear variant of lambda-calculus where any given resource must be used exactly once. In this paper we drop the (often too strict) linearity constraint by adding graded modal types which allow multiple uses of a resource in a controlled manner. We show that such a control, whilst providing more expressivity to the programmer, also interacts more richly with V-equations than the linear or Cartesian cases. Our main result is the introduction of a sound and complete V-equational system for a lambda-calculus with graded modal types interpreted by what we call a Lipschitz exponential comonad. We also show how to build such comonads canonically via a universal construction, and use our results to derive graded metric equational systems (and corresponding models) for programs with timed and probabilistic behaviour.

翻译：现代编程经常需要基于度量或类似结构来推广程序等价的概念。先前的工作通过引入V-等式的概念（即由量子V中元素标记的等式，涵盖超度量、经典和模糊（不）等式）来应对这一挑战。该工作还引入了资源必须恰好使用一次的线性λ-演算变体的V-等式系统。本文通过添加分阶模态类型，允许以受控方式多次使用资源，从而放宽了（通常过于严格的）线性约束。我们证明这种控制在为程序员提供更多表达能力的同时，与V-等式的交互比线性情形或笛卡尔情形更为丰富。我们的主要结果为：针对带分阶模态类型的λ-演算，引入了一个可靠且完备的V-等式系统，该系统由我们称为Lipschitz指数余单子的结构解释。我们还展示了如何通过通用构造典范性地构建此类余单子，并利用我们的结果为具有时间和概率行为的程序推导出分阶度量等式系统（及相应模型）。