论文标题
具有概率和非确定性的公理推理的信任单元
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
论文作者
论文摘要
概率选择和非确定性选择的组合的代数特性长期以来一直是程序语义上的研究主题。本文解释了配备了这两种选择的单子的COQ证明助手的形式化：几何凸起的单元。这种形式化具有即时应用：它为单木提供了一个模型，该模型实现了非平凡的界面，该界面允许使用概率和非确定效应通过方程推理进行证明。我们解释了我们从文献到完整的COQ形式化所做的技术选择，从中我们可以从中确定有关数学结构（例如凸空间和具体类别）的可重复使用的理论，并将我们整合到一个单调方程推理的框架中。
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.
