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 metadatas

https://hal.inria.fr/hal-00909373
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 26, 2013 - 11:08:16 AM
Last modification on : Thursday, February 7, 2019 - 5:52:52 PM

Links full text

Identifiers

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⟩

Share

Metrics

Record views

232