In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie \emph{in between} the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz.

翻译：本文旨在理解高阶类型演算中程序度量的本质，将其视为程序等价关系的自然推广。我们关注的部分度量是众所周知的，例如基于项在度量空间中的解释的度量，以及通过推广观测等价性得到的度量。我们还引入了一种新的度量，称为交互度量，它通过将著名的Int-构造应用于度量完全偏序范畴而构建。我们的目标是理解这些度量之间的相互关系，即这些度量是否以及在何种情况下细化其他度量，这与关于程序等价关系的经典问题相类似。我们获得的结果具有双重性。首先，我们证明语义起源的度量（即指称度量和交互度量）位于观测度量和等词度量之间，并且在某些情况下这些包含关系是严格的。然后，我们给出了关于指称度量和交互度量之间关系的结果，揭示前者比后者的区分能力更弱。所有结果均针对线性λ-演算给出，其中部分结果可推广至具有分级余单子的演算（Fuzz风格）。