A Probabilistic Call-by-Need Lambda-Calculus -- Extended Version

TL;DR

This paper introduces a probabilistic lambda-calculus with lazy evaluation and sharing, providing a formal framework for reasoning about probabilistic programs and their equivalences.

Contribution

It presents a novel probabilistic call-by-need lambda-calculus with techniques for proving program equivalences based on contextual semantics.

Findings

Developed a probabilistic lambda-calculus with fair binary choice

Established methods for proving contextual equivalences

Validated correctness of program transformations

Abstract

To support the understanding of declarative probabilistic programming languages, we introduce a lambda-calculus with a fair binary probabilistic choice that chooses between its arguments with equal probability. The reduction strategy of the calculus is a call-by-need strategy that performs lazy evaluation and implements sharing by recursive let-expressions. Expected convergence of expressions is the limit of the sum of all successful reduction outputs weighted by their probability. We use contextual equivalence as program semantics: two expressions are contextually equivalent if and only if the expected convergence of the expressions plugged into any program context is always the same. We develop and illustrate techniques to prove equivalences including a context lemma, two derived criteria to show equivalences and a syntactic diagram-based method. This finally enables us to show correctness of a large set of program transformations with respect to the contextual equivalence.