Combining nondeterminism, probability, and termination: equational and metric reasoning

TL;DR

This paper develops equational and metric reasoning tools for monads that combine nondeterminism, probability, and termination, aiding in the analysis of program semantics.

Contribution

It introduces presentation results for these combined monads, enabling formal reasoning about program equivalences and distances.

Findings

Provides equational reasoning tools for combined monads.

Establishes methods for measuring program distances.

Enhances understanding of program semantics with nondeterminism and probability.

Abstract

We study monads resulting from the combination of nondeterministic and probabilistic behaviour with the possibility of termination, which is essential in program semantics. Our main contributions are presentation results for the monads, providing equational reasoning tools for establishing equivalences and distances of programs.