Lambda Calculus and Probabilistic Computation

Abstract

We introduce two extensions of the $\lambda$-calculus with a probabilistic choice operator, ${\Lambda }_{\oplus }^{cbv}$ and ${\Lambda }_{\oplus }^{cbn}$, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, ${\Lambda }_{\oplus }^{!}$, which allows for a fine control of the interaction between choice and copying, and which allows us to develop a unified, modular approach.

Extended version of the paper in LICS 2019