-
Notifications
You must be signed in to change notification settings - Fork 0
/
meta.yml
113 lines (85 loc) · 4.98 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
---
fullname: ALEA
shortname: alea
organization: coq-community
community: true
action: true
coqdoc: false
doi: 10.1016/j.scico.2007.09.002
synopsis: Coq library for reasoning on randomized algorithms
description: |-
ALEA is a library for reasoning on randomized algorithms
in Coq, based on interpreting programs inside a monad
as probability distributions.
publications:
- pub_url: https://hal.inria.fr/inria-00431771
pub_title: Proofs of randomized algorithms in Coq
pub_doi: 10.1016/j.scico.2007.09.002
authors:
- name: Christine Paulin-Mohring
initial: true
- name: David Baelde
initial: true
- name: Pierre Courtieu
initial: true
maintainers:
- name: Anton Trunov
nickname: anton-trunov
- name: Vladimir Gladstein
nickname: volodeyka
opam-file-maintainer: vovaglad00@gmail.com
license:
fullname: GNU Lesser General Public License v2.1
identifier: LGPL-2.1-only
file: LICENSE
supported_coq_versions:
text: 8.11 or later (use releases for other Coq versions)
opam: '{(>= "8.11" & < "8.15~") | (= "dev")}'
tested_coq_nix_versions:
- version_or_url: https://github.com/coq/coq-on-cachix/tarball/master
tested_coq_opam_versions:
- version: dev
- version: '8.11'
- version: '8.12'
- version: '8.13'
- version: '8.14'
dependencies:
namespace: ALEA
keywords:
- name: randomized algorithm
- name: probability
- name: monad
categories:
- name: Computer Science/Data Types and Data Structures
documentation: |
## Files described in the paper
The library and its underlying theory is described in the paper
[Proofs of randomized algorithms in Coq][random],
Science of Computer Programming 74(8), 2009, pp. 568-589.
This repository used to be maintained at [coq-contribs/random](https://github.com/coq-contribs/random).
For more information visit https://www.lri.fr/~paulin/ALEA.
Coq source files mentioned in the paper are described below.
### `Misc.v`
A few preliminary notions, in particular primitives for reasoning classically in Coq, are defined.
### `Ccpo.v`
The definition of structures for ordered sets and ω-complete partial orders (a monotonic sequence has a least upper bound).
We define the type O1 → m O2 of monotonic functions and define the fixpoint-construction for monotonic functionals. Continuity is also defined.
### `Utheory.v`
An axiomatisation of the interval [0,1]. The type [0,1] is given a cpo structure.
We have the predicates ≤ and ==, a least element 0 and a least upper bound on all monotonic sequences of elements of [0,1].
### `Uprop.v`
Derived operations and properties of operators on [0,1].
### `Monads.v`
Definition of the basic monad for randomized constructions, the type α is mapped to the type (α → [0,1]) → m [0,1] of measure functions. We define the unit and star constructions and prove that they satisfy the basic monadic properties. A measure will be a function of type (α → [0,1]) → m [0,1] which enjoys extra properties such as stability with respect to basic operations and continuity. We prove that functions produced by unit and star satisfy these extra properties under appropriate assumptions.
### `Probas.v`
Definition of a dependent type for distributions on a type α. A distribution on a type α is a record containing a function µ of type (α → [0,1]) → m [0,1] and proofs that this function enjoys the stability properties of measures.
### `Prog.v`
Definition of randomized programs constructions. We define the probabilistic choice and conditional constructions and a fixpoint operator obtained by iterating a monotonic functional. We introduce an axiomatic semantics for these randomized programs --
let e be a randomized expression of type τ, p be an element of [0,1] and q be a function of type τ → [0,1], we define p ≤ \[e\](q) to be the property --
the measure of q by the distribution associated to the expression e is not less than p. In the case q is the characteristic function of a predicate Q, p ≤ \[e\](q) can be interpreted as "the probability for the result of the evaluation of e to satisfy Q is not less than p". In the particular case where q is the constant function equal to 1, the relation p ≤ \[e\](q) can be interpreted as "the probability for the evaluation of e to terminate is not less than p".
### `Cover.v`
A definition of what it means for a function f to be the characteristic function of a predicate P. Defines also characteristic functions for decidable predicates.
### `Choice.v`
A proof of composition of two runs of a probabilistic program, when a choice can improve the quality of the result. Given two randomized expressions p1 and p2 of type τ and a function Q to be estimated, we consider a choice function such that the value of Q for choice(x,y) is not less than Q(x)+Q(y). We prove that if pi evaluates Q not less than ki and terminates with probability 1 then the expression choice(p1,p2) evaluates Q not less than k1(1-k2)+k2 (which is greater than both k1 and k2 when k1 and k2 are not equal to 0).
[random]: https://hal.inria.fr/inria-00431771
---