一句话：为概率高阶语言定义环境互模拟，并证明其相对于上下文前序与上下文等价的全抽象性。
论文研究概率高阶语言中的环境互模拟。与应用式互模拟不同，环境互模拟更稳健，在同余性证明中无需 Howe 方法等复杂技术。作者以按名调用、按值调用 λ 演算，以及带引用（存储）的按值调用 λ 演算为代表，分别给出概率环境相似与互模拟相对于上下文前序和上下文等价的全抽象结果；并讨论若干 up-to 技术增强。概率对非概率环境互模拟的定义带来多种修改，其中一些专属于概率，另一些也可推广到非概率语言；文中通过多个例子说明这些修改与差异。
Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence. As representative calculi, call-by-name and call-by-value λ-calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case, full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as “up-to techniques,” are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.
@article{paperbot701,
title = {Environmental Bisimulations for Probabilistic Higher-order Languages},
author = {Davide Sangiorgi and Valeria Vignudelli},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {4},
year = {2019},
doi = {10.1145/3350618}
}