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指数余单子进行解释。我们还展示了如何通过泛构造方法规范地构建此类余单子，并利用所得结果为具有时序和概率行为的程序导出分阶度量等式系统（及相应模型）。