一句话：为含可数非确定性与概率选择的高阶语言构建步进索引逻辑关系，并给出可靠完备的上下文等价理论。
高阶语言中同时包含概率选择与非确定性选择时，指称语义模型的构造非常困难。本文改走操作语义路线，研究一个同时具有参数多态、递归类型、离散概率选择与可数非确定性的高阶语言。作者将 may- 与 must-终止概率分别推广为最优与最差终止概率，并定义步进索引逻辑关系；其中 may-等价在自然数上索引，must-等价则需在可数序数上索引。文中证明这些逻辑关系相对于诱导的上下文前序是可靠且完备的，并表明 may/must 终止概率分别对应所有调度器下的最大与最小终止概率。最后，作者导出上下文等价所诱导的等式理论，证明它验证了概率选择与非确定性选择代数理论的分配式组合。
Developing denotational models for higher-order languages that combine probabilistic and nondeterministic choice is known to be very challenging. In this paper, we propose an alternative approach based on operational techniques. We study a higher-order language combining parametric polymorphism, recursive types, discrete probabilistic choice and countable nondeterminism. We define probabilistic generalizations of may- and must-termination as the optimal and pessimal probabilities of termination. Then we define step-indexed logical relations and show that they are sound and complete with respect to the induced contextual preorders. For may-equivalence we use step-indexing over the natural numbers whereas for must-equivalence we index over the countable ordinals. We then show than the probabilities of may- and must-termination coincide with the maximal and minimal probabilities of termination under all schedulers. Finally we derive the equational theory induced by contextual equivalence and show that it validates the distributive combination of the algebraic theories for probabilistic and nondeterministic choice.
@article{paperbot2062,
title = {Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice},
author = {Alejandro Aguirre and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571195}
}