Probabilistic Operational Semantics for the Lambda Calculus

TL;DR

This paper develops a probabilistic operational semantics for an extended lambda calculus, defining both small-step and big-step semantics, and proves their equivalence and expressive power in modeling computable probability distributions.

Contribution

It introduces a probabilistic semantics for lambda calculus with nondeterminism, extending Plotkin's CPS translation, and establishes soundness and completeness for computable distributions.

Findings

Small-step and big-step semantics are equivalent.

The extended CPS translation is correct for the probabilistic calculus.

The system is sound and complete for computable probability distributions.

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.