On Feller Continuity and Full Abstraction (Long Version)

TL;DR

This paper explores the relationship between applicative bisimilarity, logical, testing, and contextual equivalence in lambda-calculi with continuous distributions, introducing Feller-continuity as a key concept for their coincidence.

Contribution

It introduces a novel notion of Feller-continuity for labelled Markov processes, establishing conditions under which various equivalences coincide in probabilistic lambda-calculi.

Findings

Bisimilarity, logical, and testing equivalences coincide with contextual equivalence under continuous functions.

Feller-continuity ensures the equivalence of coinductive and logical notions.

Without constraints, characterizing contextual equivalence becomes difficult and some equivalences are unsound.

Abstract

We study the nature of applicative bisimilarity in $\lambda$-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.