Probabilistic operational semantics for the lambda calculus

Ugo Dal Lago 1, 2 Margherita Zorzi 3
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Probabilistic operational semantics for a nondeterministic extension of pure lambda calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics are both inductively and coinductively defined. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by- value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions.
Type de document :
Article dans une revue
RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2012, 46 (3), pp.413--450. 〈10.1051/ita/2012012〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909373
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:08:16
Dernière modification le : samedi 27 janvier 2018 - 01:30:41

Lien texte intégral

Identifiants

Collections

Citation

Ugo Dal Lago, Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2012, 46 (3), pp.413--450. 〈10.1051/ita/2012012〉. 〈hal-00909373〉

Partager

Métriques

Consultations de la notice

182