Metric Reasoning About λ-Terms: The General Case

Raphaëlle Crubillé 1, 2 Ugo Dal Lago 1, 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 : In any setting in which observable properties have a quantitative flavor, it is natural to compare computational objects by way of metrics rather than equivalences or partial orders. This holds, in particular , for probabilistic higher-order programs. A natural notion of comparison , then, becomes context distance, the metric analogue of Morris' context equivalence. In this paper, we analyze the main properties of the context distance in fully-fledged probabilistic λ-calculi, this way going beyond the state of the art, in which only affine calculi were considered. We first of all study to which extent the context distance trivializes, giving a sufficient condition for trivialization. We then characterize context distance by way of a coinductively-defined, tuple-based notion of distance in one of those calculi, called Λ ⊕ !. We finally derive pseudomet-rics for call-by-name and call-by-value probabilistic λ-calculi, and prove them fully-abstract.
Type de document :
Communication dans un congrès
Hongseok Yang. ESOP 2017 - 26th European Symposium on Programming, Apr 2017, Uppsala, Sweden. Springer, 10201, pp.341-367, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-662-54434-1_13〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01639369
Contributeur : Ugo Dal Lago <>
Soumis le : lundi 20 novembre 2017 - 13:11:40
Dernière modification le : samedi 27 janvier 2018 - 01:31:17
Document(s) archivé(s) le : mercredi 21 février 2018 - 14:24:06

Fichier

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

Identifiants

Collections

Citation

Raphaëlle Crubillé, Ugo Dal Lago. Metric Reasoning About λ-Terms: The General Case. Hongseok Yang. ESOP 2017 - 26th European Symposium on Programming, Apr 2017, Uppsala, Sweden. Springer, 10201, pp.341-367, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-662-54434-1_13〉. 〈hal-01639369〉

Partager

Métriques

Consultations de la notice

294

Téléchargements de fichiers

29