INVESTIGADORES
DÍAZ CARO Alejandro
artículos
Título:
Confluence in probabilistic rewriting
Autor/es:
ALEJANDRO DÍAZ-CARO; GUIDO MARTÍNEZ
Revista:
Electronic Notes in Theoretical Computer Science
Editorial:
Elsevier
Referencias:
Año: 2018 vol. 338 p. 115 - 131
ISSN:
1571-0661
Resumen:
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 unicity 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 lambda1, an affine probabilistic lambda-calculus, and for Q*, a quantum programming language for which a related property has already been proven in the literature. Lastly, we show how distribution confluence implies unicity even for distributions that are only reached asymptotically.