Geodesic
Probabilistic operational semantics for the lambda calculus
Dal Lago, Ugo1  ; Zorzi, Margherita
1 Università di Bologna & EPI FOCUS, Dipartimento di Scienze dell’Informazione Mura Anteo Zamboni, 7, 40127 Bologna, Italy
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 3, pp. 413-450

Voir la notice de l'article provenant de la source Numdam

Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. 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.

DOI : 10.1051/ita/2012012
Classification : 68Q55, 03B70
Keywords: lambda calculus, probabilistic computaion, operational semantics

Dal Lago, Ugo 1 ; Zorzi, Margherita 

1 Università di Bologna & EPI FOCUS, Dipartimento di Scienze dell’Informazione Mura Anteo Zamboni, 7, 40127 Bologna, Italy 
@article{ITA_2012__46_3_413_0,
     author = {Dal Lago, Ugo and Zorzi, Margherita},
     title = {Probabilistic operational semantics for the lambda calculus},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {413--450},
     publisher = {EDP-Sciences},
     volume = {46},
     number = {3},
     year = {2012},
     doi = {10.1051/ita/2012012},
     mrnumber = {2981677},
     zbl = {1279.68183},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.1051/ita/2012012/}
}
TY  - JOUR
AU  - Dal Lago, Ugo
AU  - Zorzi, Margherita
TI  - Probabilistic operational semantics for the lambda calculus
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2012
SP  - 413
EP  - 450
VL  - 46
IS  - 3
PB  - EDP-Sciences
UR  - http://geodesic.mathdoc.fr/articles/10.1051/ita/2012012/
DO  - 10.1051/ita/2012012
LA  - en
ID  - ITA_2012__46_3_413_0
ER  - 
%0 Journal Article
%A Dal Lago, Ugo
%A Zorzi, Margherita
%T Probabilistic operational semantics for the lambda calculus
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2012
%P 413-450
%V 46
%N 3
%I EDP-Sciences
%U http://geodesic.mathdoc.fr/articles/10.1051/ita/2012012/
%R 10.1051/ita/2012012
%G en
%F ITA_2012__46_3_413_0
Dal Lago, Ugo; Zorzi, Margherita. Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 3, pp. 413-450. doi: 10.1051/ita/2012012

Cité par Sources :