Metric Reasoning About λ-Terms: The General Case (Long Version)
Metric Reasoning About λ-Terms: The General Case (Long Version)
复制标题
关于 λ 项的度量推理：一般情况（长版）
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Ugo Dal Lago
中科院分区：
文献类型：
--
作者：
Raphaëlle Crubillé;Ugo Dal Lago
在可观察到的属性具有定量风味的任何情况下，自然可以通过\ emph {Metrics}而不是等价或部分顺序比较计算对象。尤其是对于概率的高阶计划而言。因此，比较的自然概念变成了上下文距离，即莫里斯上下文等效的度量类似物。在本文中，我们分析了上下文距离的主要属性，以符合成熟的概率$ \ lambda $ -calculi，这是超出了最新技术的状态，在这种状态下，仅考虑了仿射计算。首先，我们研究了上下文距离琐碎的程度，从而为琐碎的情况提供了足够的条件。然后，我们通过在其中一个计算中的一个基于元组的距离概念来表征上下文距离，称为$ \ lambda^\ oplus _！$。我们最终得出了逐个名称和呼叫概率概率$ \ lambda $ -calculi的伪征象，并证明它们完全提交。
In any setting in which observable properties have a quantitative flavour, it is natural to compare computational objects by way of \emph{metrics} rather than equivalences or partial orders. This holds, in particular, for probabilistic higher-order programs. A natural notion of comparison, then, becomes context distance, the metric analogue of Morris' context equivalence. In this paper, we analyze the main properties of the context distance in fully-fledged probabilistic $\lambda$-calculi, this way going beyond the state of the art, in which only affine calculi were considered. We first of all study to which extent the context distance trivializes, giving a sufficient condition for trivialization. We then characterize context distance by way of a coinductively defined, tuple-based notion of distance in one of those calculi, called $\Lambda^\oplus_!$. We finally derive pseudometrics for call-by-name and call-by-value probabilistic $\lambda$-calculi, and prove them fully-abstract.