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.