Probabilistic Operational Semantics for the Lambda Calculus
Logic in Computer Science
2011-06-28 v2 Programming Languages
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.
Cite
@article{arxiv.1104.0195,
title = {Probabilistic Operational Semantics for the Lambda Calculus},
author = {Ugo Dal Lago and Margherita Zorzi},
journal= {arXiv preprint arXiv:1104.0195},
year = {2011}
}
Comments
35 pages