Confluence in Probabilistic Rewriting

TL;DR

This paper introduces a notion of distribution confluence in probabilistic rewriting systems, providing criteria and proofs for the uniqueness of normal forms in probabilistic programming languages, including quantum and affine lambda calculi.

Contribution

It defines distribution confluence and adapts classical confluence criteria to probabilistic rewriting, enabling simpler proofs of normalization properties in probabilistic and quantum languages.

Findings

Proves confluence for λ₁, an affine probabilistic λ-calculus.

Establishes confluence for Q* quantum programming language.

Provides criteria that simplify confluence proofs in probabilistic rewriting systems.

Abstract

Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notion of unicity of normal forms for them. To provide a tractable proof method for it, we define a property of distribution confluence which is shown to imply the desired uniqueness (even for infinite sequences of reduction) and further properties. We then carry over several criteria from the classical case, such as Newman's lemma, to simplify proving confluence in concrete languages. Using these criteria, we obtain simple proofs of confluence for $\lambda_1$, an affine probabilistic $\lambda$-calculus, and for Q$^*$, a quantum programming language for which a related property has already been proven in the literature.