ALEA is a library for reasoning on randomized algorithms in Coq, based on interpreting programs inside a monad as probability distributions.
- Author(s):
- Christine Paulin-Mohring (initial)
- David Baelde (initial)
- Pierre Courtieu (initial)
- Coq-community maintainer(s):
- Anton Trunov (@anton-trunov)
- Vladimir Gladstein (@volodeyka)
- License: GNU Lesser General Public License v2.1
- Compatible Coq versions: 8.11 or later (use releases for other Coq versions)
- Additional dependencies: none
- Coq namespace:
ALEA - Related publication(s):
The easiest way to install the latest released version of ALEA is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-aleaTo instead build and install manually, do:
git clone https://github.com/coq-community/alea.git
cd alea
make # or make -j <number-of-cores-on-your-machine>
make installThe library and its underlying theory is described in the paper Proofs of randomized algorithms in Coq, Science of Computer Programming 74(8), 2009, pp. 568-589. This repository used to be maintained at coq-contribs/random. For more information visit https://www.lri.fr/~paulin/ALEA.
Coq source files mentioned in the paper are described below.
A few preliminary notions, in particular primitives for reasoning classically in Coq, are defined.
The definition of structures for ordered sets and ω-complete partial orders (a monotonic sequence has a least upper bound). We define the type O1 → m O2 of monotonic functions and define the fixpoint-construction for monotonic functionals. Continuity is also defined.
An axiomatisation of the interval [0,1]. The type [0,1] is given a cpo structure. We have the predicates ≤ and ==, a least element 0 and a least upper bound on all monotonic sequences of elements of [0,1].
Derived operations and properties of operators on [0,1].
Definition of the basic monad for randomized constructions, the type α is mapped to the type (α → [0,1]) → m [0,1] of measure functions. We define the unit and star constructions and prove that they satisfy the basic monadic properties. A measure will be a function of type (α → [0,1]) → m [0,1] which enjoys extra properties such as stability with respect to basic operations and continuity. We prove that functions produced by unit and star satisfy these extra properties under appropriate assumptions.
Definition of a dependent type for distributions on a type α. A distribution on a type α is a record containing a function µ of type (α → [0,1]) → m [0,1] and proofs that this function enjoys the stability properties of measures.
Definition of randomized programs constructions. We define the probabilistic choice and conditional constructions and a fixpoint operator obtained by iterating a monotonic functional. We introduce an axiomatic semantics for these randomized programs -- let e be a randomized expression of type τ, p be an element of [0,1] and q be a function of type τ → [0,1], we define p ≤ [e](q) to be the property -- the measure of q by the distribution associated to the expression e is not less than p. In the case q is the characteristic function of a predicate Q, p ≤ [e](q) can be interpreted as "the probability for the result of the evaluation of e to satisfy Q is not less than p". In the particular case where q is the constant function equal to 1, the relation p ≤ [e](q) can be interpreted as "the probability for the evaluation of e to terminate is not less than p".
A definition of what it means for a function f to be the characteristic function of a predicate P. Defines also characteristic functions for decidable predicates.
A proof of composition of two runs of a probabilistic program, when a choice can improve the quality of the result. Given two randomized expressions p1 and p2 of type τ and a function Q to be estimated, we consider a choice function such that the value of Q for choice(x,y) is not less than Q(x)+Q(y). We prove that if pi evaluates Q not less than ki and terminates with probability 1 then the expression choice(p1,p2) evaluates Q not less than k1(1-k2)+k2 (which is greater than both k1 and k2 when k1 and k2 are not equal to 0).