On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice

Applicative bisimiliarity is a coinductively-defined program equivalence in which programs are tested as argument-passing processes. Starting with the seminal work by Abramsky, applicative bisimiliarity has been proved to be a powerful technique for higher-order program equivalence. Recently, applicative bisimiliarity has also been generalised to lambda calculi with algebraic effects, and with discrete probabilistic choice in particular. In this paper, we show that applicative bisimiliarity behaves well in a lambda-calculus in which probabilistic choice is available in a more general form, namely through an operator for sampling of values from continuous distributions. Our main result shows that applicative bisimilarity is sound for contextual equivalence, hence providing a new reasoning principle for higher-order probabilistic languages.