# Lambda Calculus and Probabilistic Computation

## TL;DR

This paper introduces probabilistic extensions of the lambda calculus for call-by-value and call-by-name evaluation strategies, establishing confluence and standardization properties, and unifies them through a linear logic-based calculus for better control of probabilistic choice and copying.

## Contribution

It presents novel probabilistic lambda calculi with confluence and standardization proofs, and unifies them via a linear logic framework for enhanced control over probabilistic computation.

## Key findings

- Both calculi enjoy confluence and standardization.
- A unified calculus based on Linear Logic is developed.
- The approach allows fine control of choice and copying interactions.

## 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.