一句话：为带代数效应的高阶 λ-演算建立 quantale 值行为相似与双相似，并证明其分别为相容的广义度量与伪度量。
论文研究 Abramsky 应用相似性与双相似性的定量精化，面向 Fuzz 的一个推广：一个可表达程序敏感性的线性类型 call-by-value λ-演算，并加入 Plotkin–Power 风格的代数操作。为统一处理效应与定量行为，作者依据 Lawvere 对广义度量空间的分析，提出取值于 quantale 的行为关系抽象框架；将 Barr 的 relator（lax extension）推广到 quantale 值关系，并借鉴 monoidal topology 的结果。基于此，论文定义 quantale 值效应应用相似性和双相似性，并在温和条件下分别证明它们是相容的广义度量与伪度量。该工作为高阶效应程序提供了定量行为推理的语义基础。
This paper studies quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value λ-calculus with a linear type system that can express program sensitivity, enriched with algebraic operations à la Plotkin and Power. To do so a general, abstract framework for studying behavioural relations taking values over quantales is introduced according to Lawvere's analysis of generalised metric spaces. Barr's notion of relator (or lax extension) is then extended to quantale-valued relations, adapting and extending results from the field of monoidal topology. Abstract notions of quantale-valued effectful applicative similarity and bisimilarity are then defined and proved to be a compatible generalised metric (in the sense of Lawvere) and pseudometric, respectively, under mild conditions.