Lax Lean Archive

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

Annotated semantics of the relational algebra

Lax392996.AnnotatedSemantics · concepts/Lax392996/AnnotatedSemantics.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

    Definition

    The semantics ⟨ ⁣⟨q⟩ ⁣⟩I^\langle\!\langle q \rangle\!\rangle_{\hat I} of a source query qq on a K\mathbb{K}-instance I^\hat I, for an m-semiring K\mathbb{K}, clause by clause: ⟨ ⁣⟨R⟩ ⁣⟩I^=I^(R)\langle\!\langle R \rangle\!\rangle_{\hat I} = \hat I(R); projection and selection act on the data part and carry the annotation along; the cross product annotates (u1,u2)(u_1, u_2) by α1⊗α2\alpha_1 \otimes \alpha_2; the multiset sum adds the two annotated relations; duplicate elimination collapses the copies of a tuple into one, annotated by the ⊕\oplus-sum of their annotations; and difference keeps every tuple (u,α)(u, \alpha) of the left argument, annotated by α⊖β\alpha \ominus \beta where β\beta is the ⊕\oplus-sum of the annotations of the copies of uu in the right argument. The seven claims are the clauses of the paper.

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

    This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.

    1 aeval_dedup proven

    2 aeval_diff proven

    3 aeval_prod proven

    4 aeval_proj proven

    5 aeval_rel proven

    6 aeval_sel proven

    7 aeval_sum proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Fin.Tuple.Basic
    2import Mathlib.Data.Multiset.MapFold
    3import Mathlib.Data.Multiset.Count
    4import Mathlib.Data.Multiset.Bind
    5import Lax392996.SemiringsWithMonus
    6import Lax392996.Databases
    7import Lax392996.AnnotatedDatabases
    8import Lax392996.RelationalAlgebra
    9
    10/-!
    11---
    12title: Annotated semantics of the relational algebra
    13type: definition
    14---
    15The semantics ⟨ ⁣⟨q⟩ ⁣⟩I^\langle\!\langle q \rangle\!\rangle_{\hat I} of a source query
    16qq on a K\mathbb{K}-instance I^\hat I, for an m-semiring K\mathbb{K}, clause by
    17clause: ⟨ ⁣⟨R⟩ ⁣⟩I^=I^(R)\langle\!\langle R \rangle\!\rangle_{\hat I} = \hat I(R)
    18; projection and selection act on the data part and carry the
    19annotation along; the cross product annotates (u1,u2)(u_1, u_2) by α1⊗α2\alpha_1 \otimes \alpha_2
    20; the multiset sum adds the two annotated relations;
    21duplicate elimination collapses the copies of a tuple into one, annotated by
    22the ⊕\oplus-sum of their annotations; and difference keeps every tuple
    23(u,α)(u, \alpha) of the left argument, annotated by α⊖β\alpha \ominus \beta
    24where β\beta is the ⊕\oplus-sum of the annotations of the copies of uu in
    25the right argument. The seven claims are the clauses of the paper.
    26-/
    27
    28namespace Lax392996.AnnotatedSemantics
    29
    30open Lax392996.SemiringsWithMonus Lax392996.Databases Lax392996.AnnotatedDatabases
    31open Lax392996.RelationalAlgebra
    32
    33variable {T : Type} [ValueType T]
    34variable {K : Type} [SemiringWithMonus K]
    35
    36@[reducible] def Selection.evalDecidableAnnotated {n : ℕ} (φ : Selection T n) :
    37 DecidablePred (λ (ta: AnnotatedTuple T K n) ↦ φ.eval ta.fst) :=
    38 λ t => match φ.evalDecidable t.fst with
    39 | isTrue h => isTrue (by simp [h])
    40 | isFalse h => isFalse (by simp [h])
    41
    42/-- The `⊕`-sum of the annotations of the copies of the data part `u` in an
    43annotated relation. -/
    44def annotationSum {n : ℕ} (r : Multiset (Tuple T n × K)) (u : Tuple T n) : K :=
    45 (Multiset.map Prod.snd
    46 (@Multiset.filter _ (fun p : Tuple T n × K => p.1 = u)
    47 (fun p => instDecidableEqTuple p.1 u) r)).sum
    48
    49/-- Grouping of annotated tuples by their data part: each distinct data
    50part once, with the `⊕`-sum of the annotations of its copies. -/
    51def groupByKey {n : ℕ} (r : Multiset (Tuple T n × K)) : Multiset (Tuple T n × K) :=
    52 Multiset.map (fun u => (u, annotationSum r u)) (Multiset.dedup (Multiset.map Prod.fst r))
    53
    54/-- Annotated (m-semiring) semantics of a source query.
    55
    56The `Diff` case follows ProvSQL: every tuple slot `(u, α)` of `r₁` is kept,
    57with its annotation rewritten to `α ⊖ Σ β` where `Σ β` is the semiring sum of
    58the annotations of all copies of `u` in `r₂`. Duplicate elimination keeps
    59each data part once, annotated by the `⊕`-sum of the annotations of its
    60copies. -/
    61def Query.evaluateAnnotated {n : ℕ} (q: Query T n) (hq: q.source) (d: AnnotatedDatabase T K) :
    62 AnnotatedRelation T K n := match q with
    63| Query.Rel n s =>
    64 match h : d.find n s with
    65 | none => (∅: Multiset (AnnotatedTuple T K n))
    66 | some rn => rn
    67| @Query.Proj _ n m ts q' =>
    68 let r := evaluateAnnotated q' (Query.source_proj hq rfl) d
    69 r.map (λ t ↦ ⟨λ k ↦ (ts k).eval t.fst, t.snd⟩)
    70| Query.Sel φ q =>
    71 let r := evaluateAnnotated q (Query.source_sel hq rfl) d
    72 @Multiset.filter _ (λ ta ↦ φ.eval ta.fst) (Selection.evalDecidableAnnotated φ) r
    73| @Query.Prod _ n₁ n₂ n hn q₁ q₂ =>
    74 let r₁ := evaluateAnnotated q₁ (Query.source_prod hq rfl).left d
    75 let r₂ := evaluateAnnotated q₂ (Query.source_prod hq rfl).right d
    76 Multiset.map (λ (x,y) ↦ ⟨
    77 Eq.mp (by simp[hn]; rfl)
    78 (Fin.append x.fst y.fst),
    79 x.snd*y.snd
    80 ⟩) (Multiset.product r₁ r₂)
    81| Query.Sum q₁ q₂ =>
    82 let r₁ := evaluateAnnotated q₁ (Query.source_sum hq rfl).left d
    83 let r₂ := evaluateAnnotated q₂ (Query.source_sum hq rfl).right d
    84 r₁+r₂
    85| Query.Dedup q =>
    86 let r := evaluateAnnotated q (Query.source_dedup hq rfl) d
    87 groupByKey r
    88| Query.Diff q₁ q₂ =>
    89 let r₁ := evaluateAnnotated q₁ (Query.source_diff hq rfl).left d
    90 let r₂ := evaluateAnnotated q₂ (Query.source_diff hq rfl).right d
    91 r₁.map
    92 λ (u,α) ↦ ⟨u, α - annotationSum r₂ u⟩
    93| Query.ProvSum _ _ _ => False.elim (by
    94 simp[Query.source] at hq
    95)
    96
    97/-- **relation**: `⟪R⟫_Î ≝ Î(R)`. -/
    98axiom aeval_rel : ∀ {n : ℕ} (R : String) (hq : (Query.Rel n R).source) (d : AnnotatedDatabase T K),
    99 Query.evaluateAnnotated (Query.Rel n R) hq d
    100 = (d.find n R).getD (∅ : Multiset (AnnotatedTuple T K n))
    101
    102/-- **projection**: the annotation rides along unchanged. -/
    103axiom aeval_proj : ∀ {n k : ℕ} (ts : Tuple (Term T k) n) (q : Query T k)
    104 (hq : (Query.Proj ts q).source) (d : AnnotatedDatabase T K),
    105 Query.evaluateAnnotated (Query.Proj ts q) hq d
    106 = (Query.evaluateAnnotated q (Query.source_proj hq rfl) d).map
    107 (fun p => ⟨fun l => (ts l).eval p.fst, p.snd⟩)
    108
    109/-- **selection**: the predicate reads the data part only. -/
    110axiom aeval_sel : ∀ {n : ℕ} (φ : Selection T n) (q : Query T n) (hq : (Query.Sel φ q).source)
    111 (d : AnnotatedDatabase T K),
    112 Query.evaluateAnnotated (Query.Sel φ q) hq d
    113 = @Multiset.filter _ (fun p => φ.eval p.fst) (Selection.evalDecidableAnnotated φ)
    114 (Query.evaluateAnnotated q (Query.source_sel hq rfl) d)
    115
    116/-- **cross product**: annotations multiply, `α ⊗ β`. -/
    117axiom aeval_prod : ∀ {n k₁ k₂ : ℕ} {hn : k₁ + k₂ = n} (q₁ : Query T k₁) (q₂ : Query T k₂)
    118 (hq : (Query.Prod (hn := hn) q₁ q₂).source) (d : AnnotatedDatabase T K),
    119 Query.evaluateAnnotated (Query.Prod (hn := hn) q₁ q₂) hq d
    120 = Multiset.map
    121 (fun (xy : AnnotatedTuple T K k₁ × AnnotatedTuple T K k₂) =>
    122 (⟨Eq.mp (by simp [hn]; rfl) (Fin.append xy.1.fst xy.2.fst), xy.1.snd * xy.2.snd⟩ :
    123 AnnotatedTuple T K n))
    124 (Multiset.product (Query.evaluateAnnotated q₁ (Query.source_prod hq rfl).left d)
    125 (Query.evaluateAnnotated q₂ (Query.source_prod hq rfl).right d))
    126
    127/-- **multiset sum**: the two annotated relations are added. -/
    128axiom aeval_sum : ∀ {n : ℕ} (q₁ q₂ : Query T n) (hq : (Query.Sum q₁ q₂).source)
    129 (d : AnnotatedDatabase T K),
    130 Query.evaluateAnnotated (Query.Sum q₁ q₂) hq d
    131 = Query.evaluateAnnotated q₁ (Query.source_sum hq rfl).left d
    132 + Query.evaluateAnnotated q₂ (Query.source_sum hq rfl).right d
    133
    134/-- **duplicate elimination**: the copies of a tuple are collapsed into one,
    135annotated by the `⊕`-sum of their annotations. -/
    136axiom aeval_dedup : ∀ {n : ℕ} (q : Query T n) (hq : (Query.Dedup q).source)
    137 (d : AnnotatedDatabase T K),
    138 Query.evaluateAnnotated (Query.Dedup q) hq d
    139 = groupByKey (Query.evaluateAnnotated q (Query.source_dedup hq rfl) d)
    140
    141/-- **multiset difference**: a tuple of the left argument keeps its slot, with
    142annotation `α ⊖ Σβ` where `Σβ` is the `⊕`-sum of the annotations of its copies
    143in the right argument. -/
    144axiom aeval_diff : ∀ {n : ℕ} (q₁ q₂ : Query T n) (hq : (Query.Diff q₁ q₂).source)
    145 (d : AnnotatedDatabase T K),
    146 Query.evaluateAnnotated (Query.Diff q₁ q₂) hq d
    147 = (Query.evaluateAnnotated q₁ (Query.source_diff hq rfl).left d).map
    148 (fun (u, a) =>
    149 (u, a - annotationSum (Query.evaluateAnnotated q₂ (Query.source_diff hq rfl).right d) u))
    150
    151end Lax392996.AnnotatedSemantics
    152
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…