Skip to Main content Skip to Navigation
New interface
Journal articles

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Davide Sangiogi Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2013 - 11:08:16 AM
Last modification on : Thursday, February 3, 2022 - 3:43:27 AM

Links full text



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



Record views