Probabilistic databases and marginal probabilities
Lax392996.ProbabilisticDatabases · concepts/Lax392996/ProbabilisticDatabases.lean · lax-392996
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A probability assignment on a finite set of Boolean variables gives each variable a rational probability in , the variables being independent: a valuation has probability , and a Boolean function has probability . A -instance is a probabilistic database: its random world under is the plain database of the tuples whose annotation holds at . The marginal probability of a tuple in the answer of a query is , and the annotation of in an annotated relation is the disjunction of the annotations of its copies.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Group.Finset.Basic |
| 2 | import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 3 | import Mathlib.Data.Fintype.Pi |
| 4 | import Mathlib.Data.Multiset.Basic |
| 5 | import Mathlib.Data.Rat.Defs |
| 6 | import Lax392996.SemiringsWithMonus |
| 7 | import Lax392996.BooleanFunctions |
| 8 | import Lax392996.Databases |
| 9 | import Lax392996.AnnotatedDatabases |
| 10 | import Lax392996.RelationalAlgebra |
| 11 | import Lax392996.MultisetSemantics |
| 12 | |
| 13 | /-! |
| 14 | --- |
| 15 | title: Probabilistic databases and marginal probabilities |
| 16 | type: definition |
| 17 | --- |
| 18 | A probability assignment on a finite set of Boolean variables gives each |
| 19 | variable a rational probability in , the variables being |
| 20 | independent: a valuation has probability |
| 21 | |
| 22 | , and a Boolean function has probability |
| 23 | . A -instance is a |
| 24 | probabilistic database: its random world under is the plain database |
| 25 | of the tuples whose annotation holds at . The marginal probability of |
| 26 | a tuple in the answer of a query is |
| 27 | , and the annotation of in an |
| 28 | annotated relation is the disjunction of |
| 29 | the annotations of its copies. |
| 30 | -/ |
| 31 | |
| 32 | namespace Lax392996.ProbabilisticDatabases |
| 33 | |
| 34 | open Lax392996.SemiringsWithMonus Lax392996.BooleanFunctions Lax392996.Databases |
| 35 | open Lax392996.AnnotatedDatabases Lax392996.RelationalAlgebra Lax392996.MultisetSemantics |
| 36 | |
| 37 | variable {X : Type} [Fintype X] [DecidableEq X] |
| 38 | |
| 39 | /-- A probability assignment to a finite set `X` of Boolean variables: each |
| 40 | variable is assigned a rational probability in `[0, 1]`. -/ |
| 41 | structure ProbAssignment (X : Type) where |
| 42 | /-- The probability assigned to each variable. -/ |
| 43 | prob : X → ℚ |
| 44 | /-- Probabilities are non-negative. -/ |
| 45 | prob_nonneg : ∀ x, 0 ≤ prob x |
| 46 | /-- Probabilities are at most `1`. -/ |
| 47 | prob_le_one : ∀ x, prob x ≤ 1 |
| 48 | |
| 49 | namespace ProbAssignment |
| 50 | |
| 51 | variable (P : ProbAssignment X) |
| 52 | |
| 53 | /-- Probability of a single valuation `v : X → Bool`, under the independence |
| 54 | assumption: `Pr(v) = ∏_{v(x)=⊤} Pr(x) · ∏_{v(x)=⊥} (1 - Pr(x))`. -/ |
| 55 | def valProb (v : X → Bool) : ℚ := |
| 56 | ∏ x, if v x then P.prob x else 1 - P.prob x |
| 57 | |
| 58 | /-- Probability of a Boolean function: `Pr(f) = ∑_{v ⊨ f} Pr(v)`. -/ |
| 59 | def funcProb (f : BoolFunc X) : ℚ := |
| 60 | ∑ v : X → Bool, if f v then P.valProb v else 0 |
| 61 | |
| 62 | end ProbAssignment |
| 63 | |
| 64 | /-- Membership of a tuple in a relation, that of multisets. -/ |
| 65 | instance instMembershipRelation {T : Type} {n : ℕ} : |
| 66 | Membership (Tuple T n) (Relation T n) := by |
| 67 | show Membership (Tuple T n) (Multiset (Tuple T n)) |
| 68 | infer_instance |
| 69 | |
| 70 | /-- Decidability of membership of a tuple in a relation. -/ |
| 71 | instance instDecidableMemRelation {T : Type} [ValueType T] {n : ℕ} |
| 72 | (t : Tuple T n) (r : Relation T n) : Decidable (t ∈ r) := |
| 73 | Multiset.decidableMem t r |
| 74 | |
| 75 | variable {T : Type} [ValueType T] |
| 76 | |
| 77 | /-- The disjunctive tuple annotation `tupleAnnotation r t = ⋁_{(t,α) ∈ r} α`: |
| 78 | the OR over the annotations of all annotated tuples in `r` whose data part |
| 79 | equals `t`. -/ |
| 80 | def tupleAnnotation {n : ℕ} (r : AnnotatedRelation T (BoolFunc X) n) (t : Tuple T n) : |
| 81 | BoolFunc X := |
| 82 | (Multiset.map Prod.snd |
| 83 | (@Multiset.filter _ (fun p : AnnotatedTuple T (BoolFunc X) n => p.fst = t) |
| 84 | (fun p => instDecidableEqTuple p.fst t) r)).sum |
| 85 | |
| 86 | /-- The random world of a `BoolFunc X`-annotated relation under a valuation |
| 87 | `v`: the plain relation consisting of the data parts of the annotated tuples |
| 88 | whose annotation evaluates to `true` at `v`. -/ |
| 89 | def randomWorld {n : ℕ} (v : X → Bool) (r : AnnotatedRelation T (BoolFunc X) n) : |
| 90 | Multiset (Tuple T n) := |
| 91 | Multiset.map Prod.fst |
| 92 | (@Multiset.filter _ (fun p : AnnotatedTuple T (BoolFunc X) n => p.snd v = true) |
| 93 | (fun p => instDecidableEqBool (p.snd v) true) r) |
| 94 | |
| 95 | /-- The random world of a `BoolFunc X`-annotated database: each annotated |
| 96 | relation is replaced by its random world. -/ |
| 97 | def AnnotatedDatabase.randomWorld |
| 98 | (v : X → Bool) (Î : AnnotatedDatabase T (BoolFunc X)) : Database T := |
| 99 | Î.map (fun e => (e.fst, ⟨e.snd.fst, Lax392996.ProbabilisticDatabases.randomWorld v e.snd.snd⟩)) |
| 100 | |
| 101 | namespace ProbAssignment |
| 102 | |
| 103 | variable (P : ProbAssignment X) |
| 104 | |
| 105 | /-- Marginal probability that the tuple `t` appears in the output of `q` |
| 106 | when evaluated on a random world of `Î`. -/ |
| 107 | noncomputable def marginalProb {n : ℕ} |
| 108 | (q : Query T n) (Î : AnnotatedDatabase T (BoolFunc X)) (t : Tuple T n) : ℚ := |
| 109 | ∑ v : X → Bool, |
| 110 | if t ∈ Query.evaluate q (AnnotatedDatabase.randomWorld v Î) then P.valProb v else 0 |
| 111 | |
| 112 | end ProbAssignment |
| 113 | |
| 114 | end Lax392996.ProbabilisticDatabases |
| 115 |
Builds on
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments