A trustful monad for axiomatic reasoning with probability and nondeterminism. (15th July 2021)

• Record Type: Journal Article
• Authors: AFFELDT, REYNALD; GARRIGUE, JACQUES; NOWAK, DAVID; SAIKAWA, TAKAFUMI
• Is Part Of: Journal of functional programming. Volume 31(2021)
• Publication Date: 2021-07-15
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796821000137
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a nontrivial interface, which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories, and that we integrate in a framework for monadic equational reasoning.