RAIRO - Theoretical Informatics and Applications

Research Article

Probabilistic operational semantics for the lambda calculus

Ugo Dal Lagoa1 and Margherita Zorzia2

a1 Universitàdi Bologna & EPI FOCUS, Dipartimento di Scienze dell’Informazione Mura Anteo Zamboni, 7, 40127 Bologna, Italy. dallago@cs.unibo.it

a2 Laboratoire d’Informatique L.I.P.N., Université Paris-Nord, supported by ANR Complice Project, France; margherita.zorzi@univr.it


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)

Key Words:

  • Lambda calculus;
  • probabilistic computaion;
  • operational semantics

Mathematics Subject Classification:

  • 68Q55;
  • 03B70