A library for reasoning on randomized algorithms in Coq

Christine Paulin

This library forms a basis for reasoning on randomised algorithms in the proof assistant Coq [3].

As proposed by Kozen [1, 2], we interpret probabilistic programs as measure transformers; the originality of our approach is to view this interpretation as a monadic transformation on functional programs. Using this semantics, we derive general rules for estimating the probability for a randomised algorithm to satisfy certain properties. We apply this for formally proving in the proof assistant Coq randomised algorithms such as the Bernoulli distribution from a coin flip or the termination of a random walk.

The library is composed of the following files :
U_base
An axiomatisation of the interval [0.1]
U_prop
Derived operations and properties of operators on [0,1]
Monads
Definition of the basic monad for randomized constructions, the type a is mapped to the type (a [0,1]) [0,1] of measure functions.
Probas
Definition of a dependent type for distributions on a type a, which is a record containing a measure function of type (a [0,1]) [0,1] and proofs that this function enjoys the measure properties of stability. We define the interpretation of specific random primitives.
Prog
Definition of randomized programs constructions and rules for axiomatic semantics on these randomized programs.
IterFlip
A proof of probabilistic termination for a random walk.
Choice
A proof of composition of two runs of a probabilistic program, when a choice can improve the quality of the result.
Bernouilli
Construction of a bernouilli distribution from the flip distribution.
Transitions
A probabilistic transition system is defined by a set of states and a probabilistic transition function which associates to a state a the probability to go to a state b. In our system it corresponds to a function from states to distribution on states. We use this function in order to define the corresponding distribution on paths of length k for a given integer k.

References

[1]
Dexter Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 1981.

[2]
Dexter Kozen. A probabilistic PDL. In 15th ACM Symposium on Theory of Computing, 1983.

[3]
The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.0, April 2004. .

This document was translated from LATEX by HEVEA.