Confluence in Probabilistic Rewriting

GUIDO MARTÍNEZ; ALEJANDRO DÍAZ-CARO

Brasilia

Workshop; 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017); 2017

Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notionof uniqueness of normal forms for them. To provide a tractable proof method for it, we define a propertyof distribution confluence which is shown to imply the desired uniqueness (even for infinite sequencesof reduction) and further properties. We then carry over several criteria from the classical case, such asNewman?s lemma, to simplify proving confluence in concrete languages. Using these criteria, we obtainsimple proofs of confluence for λ1 , an affine probabilistic λ-calculus, and for Q* , a quantum programminglanguage for which a related property has already been proven in the literature.