×

Proofs of randomized algorithms in Coq. (English) Zbl 1235.68325

Uustalu, Tarmo (ed.), Mathematics of program construction. 8th international conference, MPC 2006, Kuressaare, Estonia, July 3–5, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-35631-8/pbk). Lecture Notes in Computer Science 4014, 49-68 (2006).
Summary: Randomized algorithms are widely used either for finding efficiently approximated solutions to complex problems, for instance primality testing, or for obtaining good average behavior, for instance in distributed computing. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of the programs. Providing tools for the mechanization of reasoning is consequently an important issue. Our paper presents a new method for proving properties of randomized algorithms in a proof assistant based on higher-order logic. It is based on the monadic interpretation of randomized programs as probabilistic distribution [R. Norman and A. Pfeffer, “Stochastic lambda calculus and monads of probability distributions”, in: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2002, 154–165 (2002)]. It does not require the definition of an operational semantics for the language nor the development of a complex formalization of measure theory, but only use functionals and algebraic properties of the unit interval. Using this model, we show the validity of general rules for estimating the probability for a randomized algorithm to satisfy certain properties, in particular in the case of general recursive functions.
We apply this theory for formally proving a program implementing a Bernoulli distribution from a coin flip and the termination of a random walk. All the theories and results presented in this paper have been fully formalized and proved in the Coq proof assistant.
For the entire collection see [Zbl 1107.68016].

MSC:

68W20 Randomized algorithms
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Coq
PDFBibTeX XMLCite
Full Text: DOI