### Abstract

In Isabelle, randomized algorithms are usually represented using probability mass functions (PMFs), with which it is possible to verify their correctness, particularly properties about the distribution of their result. However, that approach does not provide a way to generate executable code for such algorithms. In this entry, we introduce a new monad for randomized algorithms, for which it is possible to generate code and simultaneously reason about the correctness of randomized algorithms. The latter works by a Scott-continuous monad morphism between the newly introduced random monad and PMFs. On the other hand, when supplied with an external source of random coin flips, the randomized algorithms can be executed.

### License

BSD License

### Topics

- Computer science/Algorithms/Randomized

### Session Executable_Randomized_Algorithms

- Tau_Additivity
- Coin_Space
- Randomized_Algorithm_Internal
- Randomized_Algorithm
- Tracking_Randomized_Algorithm
- Tracking_SPMF
- Dice_Roll
- Permuted_Congruential_Generator
- Basic_Randomized_Algorithms

### Depends on

- Probabilistic while loop
- The Hurwitz and Riemann ζ Functions

### Auto-related entries

- A Formal Model of the Document Object Model with Shadow Roots
- A Formal Model of the Safely Composable Document Object Model with Shadow Roots
- A Formal Model of the Document Object Model

## Cite

×

Executable_Randomized_Algorithms-AFP

    @article{Executable_Randomized_Algorithms-AFP,
      author  = {Emin Karayel and Manuel Eberl},
      title   = {Executable Randomized Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Executable_Randomized_Algorithms.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Jun 29, 2023 : Isabelle2022