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等式的交互复杂性远超线性或笛卡尔情形。我们的核心成果是：为基于Lipschitz指数余单子解释分级模态类型的λ演算，构建了一个完备且可靠的V等式系统。我们还展示了如何通过泛构造方法规范性构建此类余单子，并利用研究成果为含时间与概率行为的程序推导出分级度量等式系统（及相应模型）。