论文标题
关于砍伐者的连续性和完全抽象（长版）
On Feller Continuity and Full Abstraction (Long Version)
论文作者
论文摘要
我们研究了$λ$ -Calculi中应用双元性的性质，并带有运营商，用于从连续分布中进行采样。一方面，我们表明，当只有通过连续函数来操纵实数时，双性恋，逻辑等效性和测试等价都与上下文对等相一致。对此结果的关键要素是标记的马尔可夫过程的新颖概念，我们认为这是一个独立的利益，是一类广泛的LMP，其共同感应和逻辑上启发的等效性一致。另一方面，我们表明，如果对实数的操纵方式没有任何约束，则表征上下文对等的情况很难，而且上述等效的大多数概念甚至不符合。
We study the nature of applicative bisimilarity in $λ$-calculi endowed with operators for sampling from continuous 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 only through continuous functions. The key ingredient towards this result is a novel notion of Feller-continuity for labelled Markov processes, which we believe of independent interest, being 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.
