While this submission is a draft, it cannot be used by other submissions.

Probabilistic databases and marginal probabilities

Lax392996.ProbabilisticDatabases · concepts/Lax392996/ProbabilisticDatabases.lean · lax-392996

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A probability assignment on a finite set XX of Boolean variables gives each variable a rational probability in [0,1][0, 1], the variables being independent: a valuation ν:X→{⊥,⊤}\nu : X \to \{\bot, \top\} has probability Pr⁡(ν)=∏ν(x)=⊤Pr⁡(x)⋅∏ν(x)=⊥(1−Pr⁡(x))\Pr(\nu) = \prod_{\nu(x) = \top} \Pr(x) \cdot \prod_{\nu(x) = \bot} (1 - \Pr(x)), and a Boolean function ff has probability Pr⁡(f)=∑ν⊨fPr⁡(ν)\Pr(f) = \sum_{\nu \models f} \Pr(\nu). A B[X]\mathcal{B}[X]-instance I^\hat I is a probabilistic database: its random world under ν\nu is the plain database of the tuples whose annotation holds at ν\nu. The marginal probability of a tuple tt in the answer of a query qq is ∑νPr⁡(ν)⋅[t∈[ ⁣[q] ⁣]I^(ν)]\sum_\nu \Pr(\nu) \cdot [t \in [\![q]\!]_{\hat I(\nu)}], and the annotation of tt in an annotated relation is the disjunction ⋁(t,α)α\bigvee_{(t, \alpha)} \alpha of the annotations of its copies.

    Concept map
    7 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Group.Finset.Basic
    2import Mathlib.Algebra.Order.BigOperators.Group.Finset
    3import Mathlib.Data.Fintype.Pi
    4import Mathlib.Data.Multiset.Basic
    5import Mathlib.Data.Rat.Defs
    6import Lax392996.SemiringsWithMonus
    7import Lax392996.BooleanFunctions
    8import Lax392996.Databases
    9import Lax392996.AnnotatedDatabases
    10import Lax392996.RelationalAlgebra
    11import Lax392996.MultisetSemantics
    12
    13/-!
    14---
    15title: Probabilistic databases and marginal probabilities
    16type: definition
    17---
    18A probability assignment on a finite set XX of Boolean variables gives each
    19variable a rational probability in [0,1][0, 1], the variables being
    20independent: a valuation ν:X→{⊥,⊤}\nu : X \to \{\bot, \top\} has probability
    21Pr⁡(ν)=∏ν(x)=⊤Pr⁡(x)⋅∏ν(x)=⊥(1−Pr⁡(x))\Pr(\nu) = \prod_{\nu(x) = \top} \Pr(x) \cdot \prod_{\nu(x) = \bot} (1 - \Pr(x))
    22, and a Boolean function ff has probability Pr⁡(f)=∑ν⊨fPr⁡(ν)\Pr(f) = \sum_{\nu \models f} \Pr(\nu)
    23. A B[X]\mathcal{B}[X]-instance I^\hat I is a
    24probabilistic database: its random world under ν\nu is the plain database
    25of the tuples whose annotation holds at ν\nu. The marginal probability of
    26a tuple tt in the answer of a query qq is ∑νPr⁡(ν)⋅[t∈[ ⁣[q] ⁣]I^(ν)]\sum_\nu \Pr(\nu) \cdot [t \in [\![q]\!]_{\hat I(\nu)}]
    27, and the annotation of tt in an
    28annotated relation is the disjunction ⋁(t,α)α\bigvee_{(t, \alpha)} \alpha of
    29the annotations of its copies.
    30-/
    31
    32namespace Lax392996.ProbabilisticDatabases
    33
    34open Lax392996.SemiringsWithMonus Lax392996.BooleanFunctions Lax392996.Databases
    35open Lax392996.AnnotatedDatabases Lax392996.RelationalAlgebra Lax392996.MultisetSemantics
    36
    37variable {X : Type} [Fintype X] [DecidableEq X]
    38
    39/-- A probability assignment to a finite set `X` of Boolean variables: each
    40variable is assigned a rational probability in `[0, 1]`. -/
    41structure 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
    49namespace ProbAssignment
    50
    51variable (P : ProbAssignment X)
    52
    53/-- Probability of a single valuation `v : X → Bool`, under the independence
    54assumption: `Pr(v) = ∏_{v(x)=⊤} Pr(x) · ∏_{v(x)=⊥} (1 - Pr(x))`. -/
    55def 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)`. -/
    59def funcProb (f : BoolFunc X) : ℚ :=
    60 ∑ v : X → Bool, if f v then P.valProb v else 0
    61
    62end ProbAssignment
    63
    64/-- Membership of a tuple in a relation, that of multisets. -/
    65instance 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. -/
    71instance instDecidableMemRelation {T : Type} [ValueType T] {n : ℕ}
    72 (t : Tuple T n) (r : Relation T n) : Decidable (t ∈ r) :=
    73 Multiset.decidableMem t r
    74
    75variable {T : Type} [ValueType T]
    76
    77/-- The disjunctive tuple annotation `tupleAnnotation r t = ⋁_{(t,α) ∈ r} α`:
    78the OR over the annotations of all annotated tuples in `r` whose data part
    79equals `t`. -/
    80def 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
    88whose annotation evaluates to `true` at `v`. -/
    89def 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
    96relation is replaced by its random world. -/
    97def 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
    101namespace ProbAssignment
    102
    103variable (P : ProbAssignment X)
    104
    105/-- Marginal probability that the tuple `t` appears in the output of `q`
    106when evaluated on a random world of `Î`. -/
    107noncomputable 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
    112end ProbAssignment
    113
    114end Lax392996.ProbabilisticDatabases
    115

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…