a1 Universitàdi Bologna & EPI FOCUS, Dipartimento di Scienze dell’Informazione Mura Anteo Zamboni, 7, 40127 Bologna, Italy. firstname.lastname@example.org
a2 Laboratoire d’Informatique L.I.P.N., Université Paris-Nord, supported by ANR Complice Project, France; email@example.com
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.
(Received August 23 2011)
(Accepted April 18 2012)
(Online publication June 22 2012)
Mathematics Subject Classification: