Lax Lean Archive

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

Probabilistic query evaluation by the rewritten query

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

proven

Loading review…

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

    Theorem

    For a probability assignment PP on a finite set XX of variables, a B[X]\mathcal{B}[X]-instance I^\hat I, a source query qq and a tuple tt, if q^\hat q is the query rewritten from qq by the rules (R1) to (R4), then Pr⁡(t∈q(I^))=Pr⁡(⋁(t,α)∈[ ⁣[q^] ⁣]I^α)\Pr(t \in q(\hat I)) = \Pr\big(\bigvee_{(t, \alpha) \in [\![\hat q]\!]_{\hat I}} \alpha\big): the marginal probability of tt is the probability of its annotation in the plain evaluation of q^\hat q on the composite reading of I^\hat I, each answer tuple read back as an annotated one. This is the paper's Corollary 13, combining the correctness of the rewriting with the theorem on probabilistic evaluation; as for the former, the paper states it with the aggregation rule (R5) included, which this submission does not cover.

    Concept map
    9 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Lax392996.SemiringsWithMonus
    2import Lax392996.BooleanFunctions
    3import Lax392996.Databases
    4import Lax392996.AnnotatedDatabases
    5import Lax392996.RelationalAlgebra
    6import Lax392996.MultisetSemantics
    7import Lax392996.RewritingRules
    8import Lax392996.ProbabilisticDatabases
    9
    10/-!
    11---
    12title: Probabilistic query evaluation by the rewritten query
    13type: theorem
    14---
    15For a probability assignment PP on a finite set XX of variables, a
    16B[X]\mathcal{B}[X]-instance I^\hat I, a source query qq and a tuple tt,
    17if q^\hat q is the query rewritten from qq by the rules (R1) to (R4), then
    18Pr⁡(t∈q(I^))=Pr⁡(⋁(t,α)∈[ ⁣[q^] ⁣]I^α)\Pr(t \in q(\hat I)) = \Pr\big(\bigvee_{(t, \alpha) \in [\![\hat q]\!]_{\hat I}} \alpha\big)
    19: the marginal probability of tt is the probability of its
    20annotation in the plain evaluation of q^\hat q on the composite reading of
    21I^\hat I, each answer tuple read back as an annotated one. This is the
    22paper's Corollary 13, combining the correctness of the rewriting with the
    23theorem on probabilistic evaluation; as for the former, the paper states it
    24with the aggregation rule (R5) included, which this submission does not
    25cover.
    26-/
    27
    28namespace Lax392996.ProbabilisticEvaluationByRewriting
    29
    30open Lax392996.SemiringsWithMonus Lax392996.BooleanFunctions Lax392996.Databases
    31open Lax392996.AnnotatedDatabases Lax392996.RelationalAlgebra Lax392996.MultisetSemantics
    32open Lax392996.RewritingRules Lax392996.ProbabilisticDatabases
    33
    34/-- **Corollary 13.** The marginal probability of a tuple is the probability
    35of its annotation in the answer of the rewritten query. -/
    36axiom corollary_13 : ∀ {X : Type} [Fintype X] [DecidableEq X] {T : Type} [ValueType T]
    37 (P : ProbAssignment X) [HasAltLinearOrder (BoolFunc X)] {n : ℕ} (q : Query T n) (hq : q.source)
    38 (Î : AnnotatedDatabase T (BoolFunc X)) (t : Tuple T n),
    39 ProbAssignment.marginalProb P q Î t
    40 = ProbAssignment.funcProb P (tupleAnnotation
    41 (Multiset.map Tuple.fromComposite (Query.evaluate (Query.rewriting q hq) Î.toComposite)) t)
    42
    43end Lax392996.ProbabilisticEvaluationByRewriting
    44
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…