Publication:5152658

DOI10.1017/S0956796821000137zbMATH Open1493.03004arXiv2003.09993MaRDI QIDQ5152658FDOQ5152658

Jacques Garrigue, Takafumi Saikawa, Reynald Affeldt, David Nowak

Publication date: 24 September 2021

Published in: Journal of Functional Programming (Search for Journal in Brave)

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 non-trivial 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.

Full work available at URL: https://arxiv.org/abs/2003.09993

zbMATH Keywords

monadCoqprobabilistic choicenondeterministic choiceconvex powerset monadgeometrically convex monadmonadic equational reasoning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Semantic domains for combining probability and non-determinism
• An invitation to general algebra and universal constructions.
• Distributing probability over non-determinism
• Formalization of Shannon's theorems
• Abstraction, Refinement and Proof for Probabilistic Systems
• Convexity, Duality and Effects
• Axioms for probability and nondeterminism
• Packaging Mathematical Structures
• Unifying Theories of Programming with Monads
• Postulates for the barycentric calculus
• Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
• Verified tail bounds for randomized programs
• Just do it
• Formal adventures in convex and conical spaces
• Canonical Structures for the Working Coq User
• Combining probabilistic and non-deterministic choice via weak distributive laws
• A hierarchy of monadic effects for program verification using equational reasoning
• Experience Implementing a Performant Category-Theory Library in Coq
• Category Theory in Coq 8.5
• Probabilistic Completion of Nondeterministic Models

Cited In (4)

• Truthful Monadic Abstractions
• Measure construction by extension in dependent type theory with application to integration
• Towards a practical library for monadic equational reasoning in Coq
• Monads and Quantitative Equational Theories for Nondeterminism and Probability

Uses Software

• Coq
• Irdis
• UniMath
• Idris
• GitHub
• finmap

This page was built for publication: A trustful monad for axiomatic reasoning with probability and nondeterminism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5152658)