Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Probabilistic while loop

Email Gateway (Aug 22 2022 at 15:28):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Probabilistic while loop
by Andreas Lochbihler

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.

Enjoy 3/5

Last updated: Apr 24 2024 at 08:20 UTC