| Issue |
RAIRO-Theor. Inf. Appl.
Volume 46, Number 3, July-September 2012
|
|
|---|---|---|
| Page(s) | 413 - 450 | |
| DOI | https://doi.org/10.1051/ita/2012012 | |
| Published online | 22 June 2012 | |
Probabilistic operational semantics for the lambda calculus
1
Universitàdi Bologna & EPI FOCUS, Dipartimento di Scienze
dell’Informazione Mura Anteo Zamboni, 7, 40127
Bologna,
Italy
dallago@cs.unibo.it
2
Laboratoire d’Informatique L.I.P.N., Université
Paris-Nord, supported
by
ANR Complice Project,
France
margherita.zorzi@univr.it
Received: 23 August 2011
Accepted: 18 April 2012
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.
Mathematics Subject Classification: 68Q55 / 03B70
Key words: Lambda calculus / probabilistic computaion / operational semantics
© EDP Sciences 2012
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.