On Feller continuity and full abstraction - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Proceedings of the ACM on Programming Languages Année : 2022

On Feller continuity and full abstraction

Résumé

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.
Fichier principal
Vignette du fichier
icfp2022a.pdf (460.73 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03923488 , version 1 (04-01-2023)

Identifiants

Citer

Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo. On Feller continuity and full abstraction. Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.826-854. ⟨10.1145/3547651⟩. ⟨hal-03923488⟩
25 Consultations
14 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More