On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs

Ugo Dal Lago 1, 2 Davide Sangiorgi 2, 1 Michele Alberti 3
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We study bisimulation and context equivalence in a probabilistic λ-calculus. The contributions of this paper are threefold. Firstly we show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. Secondly we show that, while bisimilarity is in general strictly finer than context equivalence, coincidence between the two relations is attained on pure λ-terms. The resulting equality is that induced by Levy-Longo trees, generally accepted as the finest extensional equivalence on pure λ-terms under a lazy regime. Finally, we derive a coinductive characterisation of context equivalence on the whole probabilistic language, via an extension in which terms akin to distributions may appear in redex position. Another motivation for the extension is that its operational semantics allows us to experiment with a different congruence technique, namely that of logical bisimilarity.
Type de document :
Communication dans un congrès
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. 〈10.1145/2535838.2535872〉
Liste complète des métadonnées

Littérature citée [46 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01091573
Contributeur : Ugo Dal Lago <>
Soumis le : vendredi 2 janvier 2015 - 16:21:58
Dernière modification le : samedi 27 janvier 2018 - 01:30:54
Document(s) archivé(s) le : vendredi 3 avril 2015 - 10:05:41

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Ugo Dal Lago, Davide Sangiorgi, Michele Alberti. On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs. The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. 〈10.1145/2535838.2535872〉. 〈hal-01091573〉

Partager

Métriques

Consultations de la notice

148

Téléchargements de fichiers

175