# Probabilistic while loop

 Title: Probabilistic while loop Author: Andreas Lochbihler Submission date: 2017-05-05 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. Change history: [2018-02-02]: Added a proof that probabilistic conditioning can be implemented by repeated sampling. (revision 305867c4e911) BibTeX: @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}, } License: BSD License Depends on: MFMC_Countable Used by: CryptHOL Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.