### Abstract

This AFP entry defines a probabilistic while operator based on sub-probability mass functions and formalises zero-one laws and variant rules for probabilistic loop termination. As applications, we implement probabilistic algorithms for the Bernoulli, geometric and arbitrary uniform distributions that only use fair coin flips, and prove them correct and terminating with probability 1.

### License

BSD License

### History

February 2, 2018
  Added a proof that probabilistic conditioning can be implemented by repeated sampling. (revision 305867c4e911)

### Topics

- Computer science/Functional programming
- Mathematics/Probability theory
- Computer science/Algorithms/Randomized

### Session Probabilistic_While

- While_SPMF
- Bernoulli
- Geometric
- Fast_Dice_Roll
- Resampling

### Depends on

- A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks

### Used by

- Executable Randomized Algorithms
- CryptHOL

## Cite

×

Probabilistic_While-AFP

    @article{Probabilistic_While-AFP,
      author  = {Andreas Lochbihler},
      title   = {Probabilistic while loop},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Probabilistic_While.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- May 11, 2017 : Isabelle2016-1