Metric Reasoning About λ-Terms: The Affine Case

Raphaëlle Crubillé 1 Ugo Dal Lago 2, 3
3 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Terms of Church's λ-calculus can be considered equivalent along many different definitions, but context equivalence is certainly the most direct and universally accepted one. If the underlying calculus becomes probabilistic, however, equivalence is too discriminating: terms which have totally unrelated behaviours are treated the same as terms which behave very similarly. We study the problem of evaluating the distance between affine λ-terms. A natural generalisation of context equivalence , is shown to be characterised by a notion of trace distance, and to be bounded from above by a coinductively defined distance based on the Kantorovich metric on distributions. A different, again fully-abstract, tuple-based notion of trace distance is shown to be able to handle nontrivial examples.
Type de document :
Communication dans un congrès
LICS 2015, Jul 2015, Kyoto, Japan. 2015, Proceedings of LICS 2015. 〈10.1109/LICS.2015.64〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger
Contributeur : Ugo Dal Lago <>
Soumis le : vendredi 20 novembre 2015 - 17:23:33
Dernière modification le : mercredi 10 octobre 2018 - 10:09:25
Document(s) archivé(s) le : vendredi 28 avril 2017 - 20:19:00


Fichiers produits par l'(les) auteur(s)




Raphaëlle Crubillé, Ugo Dal Lago. Metric Reasoning About λ-Terms: The Affine Case. LICS 2015, Jul 2015, Kyoto, Japan. 2015, Proceedings of LICS 2015. 〈10.1109/LICS.2015.64〉. 〈hal-01231814〉



Consultations de la notice


Téléchargements de fichiers