一句话：引入 Feller 连续性，证明连续采样 λ 演算中多种程序等价与上下文等价一致。
论文研究带连续分布采样算子的 λ 演算中，applicative bisimilarity 等程序等价的语义性质与上下文等价的关系。作者为 labelled Markov processes 提出 Feller 连续性概念，并据此建立一类广泛的 LMP，使余归纳式等价与逻辑式等价重合。主要结果表明：当实数只能通过连续函数被操作时，bisimilarity、逻辑等价和测试等价都与上下文等价一致，从而获得 full abstraction；若不对实数操作施加限制，上下文等价难以刻画，且上述多数等价甚至不健全。工作为概率程序的指称/操作语义与共归纳推理提供了统一视角。
We study the nature of applicative bisimilarity in λ-calculi endowed with operators for sampling from contin- uous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with contextual equivalence when real numbers can be manipulated through continuous functions only. The key ingredient towards this result is a notion of Feller-continuity for labelled Markov processes, which we believe of independent interest, giving rise a broad class of LMPs for which coinductive and logically inspired equivalences coincide. On the other hand, we show that if no constraint is put on the way real numbers are manipulated, characterizing contextual equivalence turns out to be hard, and most of the aforementioned notions of equivalence are even unsound.
@article{paperbot1502,
title = {On Feller continuity and full abstraction},
author = {Gilles Barthe and Raphaëlle Crubillé and Ugo Dal Lago and Francesco Gavazzo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547651}
}