Probabilistic_While (Q53713)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Probabilistic_While
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Probabilistic_While |
AFP entry Probabilistic_While |
Statements
Andreas Lochbihler
0 references
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.
0 references
5 May 2017
0 references
Probabilistic while loop (English)
0 references
