Lax Lean Archive

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

Multiset semantics of the relational algebra

Lax392996.MultisetSemantics · concepts/Lax392996/MultisetSemantics.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[\![q]\!]_I of a query qq on a database II, clause by clause: [ ⁣[R] ⁣]I=I(R)[\![R]\!]_I = I(R); [ ⁣[Πt1,…,tn(q)] ⁣]I={ ⁣∣(t1(u),…,tn(u))∣u∈[ ⁣[q] ⁣]I∣ ⁣}[\![\Pi_{t_1, \dots, t_n}(q)]\!]_I = \{\!|(t_1(u), \dots, t_n(u)) \mid u \in [\![q]\!]_I|\!\}; [ ⁣[σφ(q)] ⁣]I={ ⁣∣u∈[ ⁣[q] ⁣]I∣φ(u)∣ ⁣}[\![\sigma_\varphi(q)]\!]_I = \{\!|u \in [\![q]\!]_I \mid \varphi(u)|\!\}; [ ⁣[q1×q2] ⁣]I=[ ⁣[q1] ⁣]I×[ ⁣[q2] ⁣]I[\![q_1 \times q_2]\!]_I = [\![q_1]\!]_I \times [\![q_2]\!]_I; [ ⁣[q1⊎q2] ⁣]I=[ ⁣[q1] ⁣]I⊎[ ⁣[q2] ⁣]I[\![q_1 \uplus q_2]\!]_I = [\![q_1]\!]_I \uplus [\![q_2]\!]_I; [ ⁣[ε(q)] ⁣]I[\![\varepsilon(q)]\!]_I keeps one copy of each tuple of [ ⁣[q] ⁣]I[\![q]\!]_I; and [ ⁣[q1−q2] ⁣]I[\![q_1 - q_2]\!]_I removes from [ ⁣[q1] ⁣]I[\![q_1]\!]_I every copy of a tuple occurring in [ ⁣[q2] ⁣]I[\![q_2]\!]_I. The definition also interprets the two extra operators: the provenance aggregation γ\gamma sums its term over each group of the key columns, and the fused HAVINGHAVING operator computes its aggregates over each group read in the canonical tuple order. The seven claims are the clauses of the paper.

    Concept map
    3 concepts; 8 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 eval_dedup proven

    2 eval_diff proven

    3 eval_prod proven

    4 eval_proj proven

    5 eval_rel proven

    6 eval_sel proven

    7 eval_sum proven

    In the paper

    • page 16 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Multiset.Dedup
    2import Mathlib.Data.Multiset.Filter
    3import Mathlib.Data.Multiset.Sort
    4import Mathlib.Data.Multiset.Basic
    5import Mathlib.Data.Multiset.MapFold
    6import Mathlib.Data.Fin.VecNotation
    7import Lax392996.Databases
    8import Lax392996.RelationalAlgebra
    9
    10/-!
    11---
    12title: Multiset semantics of the relational algebra
    13type: definition
    14---
    15The semantics [ ⁣[q] ⁣]I[\![q]\!]_I of a query qq on a database II, clause by
    16clause: [ ⁣[R] ⁣]I=I(R)[\![R]\!]_I = I(R); [ ⁣[Πt1,…,tn(q)] ⁣]I={ ⁣∣(t1(u),…,tn(u))∣u∈[ ⁣[q] ⁣]I∣ ⁣}[\![\Pi_{t_1, \dots, t_n}(q)]\!]_I = \{\!|(t_1(u), \dots, t_n(u)) \mid u \in [\![q]\!]_I|\!\}
    17;
    18[ ⁣[σφ(q)] ⁣]I={ ⁣∣u∈[ ⁣[q] ⁣]I∣φ(u)∣ ⁣}[\![\sigma_\varphi(q)]\!]_I = \{\!|u \in [\![q]\!]_I \mid \varphi(u)|\!\};
    19[ ⁣[q1×q2] ⁣]I=[ ⁣[q1] ⁣]I×[ ⁣[q2] ⁣]I[\![q_1 \times q_2]\!]_I = [\![q_1]\!]_I \times [\![q_2]\!]_I; [ ⁣[q1⊎q2] ⁣]I=[ ⁣[q1] ⁣]I⊎[ ⁣[q2] ⁣]I[\![q_1 \uplus q_2]\!]_I = [\![q_1]\!]_I \uplus [\![q_2]\!]_I
    20; [ ⁣[ε(q)] ⁣]I[\![\varepsilon(q)]\!]_I
    21keeps one copy of each tuple of [ ⁣[q] ⁣]I[\![q]\!]_I; and [ ⁣[q1−q2] ⁣]I[\![q_1 - q_2]\!]_I
    22removes from [ ⁣[q1] ⁣]I[\![q_1]\!]_I every copy of a tuple occurring in
    23[ ⁣[q2] ⁣]I[\![q_2]\!]_I. The definition also interprets the two extra operators:
    24the provenance aggregation γ\gamma sums its term over each group of the
    25key columns, and the fused `HAVING` operator computes its aggregates over
    26each group read in the canonical tuple order. The seven claims are the
    27clauses of the paper.
    28-/
    29
    30namespace Lax392996.MultisetSemantics
    31
    32open Lax392996.Databases Lax392996.RelationalAlgebra
    33
    34variable {T : Type} [ValueType T]
    35
    36/-- Addition as a binary function, the fold of the `⊕`-sum performed by
    37the provenance aggregation `Query.ProvSum`. -/
    38def addFn (a b : T) := a + b
    39
    40instance instCommutativeAddFn : @Std.Commutative T addFn where
    41 comm := add_comm
    42
    43instance instAssociativeAddFn : @Std.Associative T addFn where
    44 assoc := add_assoc
    45
    46/-- The occurrences of the group of key `g` in relation `r`: the multiset of
    47matching tuples, as a list sorted by the canonical linear order on tuples.
    48The sort order plays the role of the ordering along which
    49non-commutative sequence aggregates read the occurrences of a group; for
    50commutative aggregates it is irrelevant. -/
    51def Relation.groupSeq {m n₁ : ℕ} (is : Tuple (Fin m) n₁) (r : Relation T m) (g : Tuple T n₁) :
    52 List (Tuple T m) :=
    53 Multiset.sort
    54 (@Multiset.filter _ (fun u => ∀ k' : Fin n₁, u (is k') = g k')
    55 (fun u => @Nat.decidableForallFin n₁ (fun k' => u (is k') = g k') (fun _ => inferInstance)) r)
    56 (· ≤ ·)
    57
    58/-- Multiset semantics of a query over a plain database.
    59
    60The `Diff` case is all-or-nothing difference: every copy of a tuple that
    61occurs at all in `r₂` is removed from `r₁`, which is what the monus-based
    62annotated semantics of difference gives on `0`/`1`-annotated inputs. -/
    63def Query.evaluate {n : ℕ} (q: Query T n) (d: Database T): Relation T n := match q with
    64| Query.Rel n s =>
    65 match d.find n s with
    66 | none => (∅: Multiset (Tuple T n))
    67 | some rn => rn
    68| Query.Proj ts q => let r := evaluate q d; Multiset.map (λ t ↦ λ k ↦ (ts k).eval t) r
    69| Query.Sel φ q => let r := evaluate q d; @Multiset.filter _ φ.eval φ.evalDecidable r
    70| @Query.Prod _ n₁ n₂ n hn q₁ q₂ =>
    71 let r₁ := evaluate q₁ d
    72 let r₂ := evaluate q₂ d
    73 (r₁ * r₂).cast hn
    74| Query.Sum q₁ q₂ => let r₁ := evaluate q₁ d; let r₂ := evaluate q₂ d; r₁ + r₂
    75| Query.Dedup q => let r := evaluate q d; Multiset.dedup r
    76| Query.Diff q₁ q₂ =>
    77 let r₁ := evaluate q₁ d
    78 let r₂ : Multiset (Tuple T _) := evaluate q₂ d
    79 r₁.filter (fun t ↦ t ∉ r₂)
    80| @Query.ProvSum _ m n₁ is t q =>
    81 let r := evaluate (Query.Dedup (Query.Proj (λ (k: Fin n₁) ↦ Term.index (is k)) q)) d
    82 let s := evaluate q d
    83 r.map (λ g ↦ Fin.append g (
    84 λ _: Fin 1 ↦ (
    85 (@Multiset.filter _ (λ u ↦ ∀ k': Fin n₁, u (is k') = g k')
    86 (fun u => @Nat.decidableForallFin n₁ (fun k' => u (is k') = g k') (fun _ => inferInstance))
    87 s).map (λ u ↦ t.eval u)
    88 ).fold addFn 0
    89 ))
    90| @Query.Having _ m n₁ n₂ is ts fs op l s q =>
    91 let keys := evaluate (Query.Dedup (Query.Proj (λ (k: Fin n₁) ↦ Term.index (is k)) q)) d
    92 let r := evaluate q d
    93 Multiset.map
    94 (λ g ↦ Fin.append g
    95 (λ (k: Fin n₂) ↦ (fs k) ((Relation.groupSeq is r g).map (ts k).eval)))
    96 (@Multiset.filter _
    97 (λ g ↦ op.eval ((fs l) ((Relation.groupSeq is r g).map (ts l).eval)) (s.eval g))
    98 (fun g => instDecidableEval op _ _)
    99 keys)
    100termination_by q.aggdepth2_plus_depth
    101decreasing_by
    102 all_goals simp[Query.aggdepth2_plus_depth]
    103 any_goals refine Nat.lt_add_one_of_le ?_
    104 any_goals exact Nat.le_max_left _ _
    105 any_goals exact Nat.le_max_right _ _
    106
    107/-- **relation**: `⟦R⟧_I ≝ I(R)`. -/
    108axiom eval_rel : ∀ {n : ℕ} (R : String) (d : Database T),
    109 Query.evaluate (Query.Rel n R) d = (d.find n R).getD (∅ : Multiset (Tuple T n))
    110
    111/-- **projection**: `⟦Π_{t₁,…,t_n}(q)⟧_I ≝ {|(t₁(u),…,t_n(u)) | u ∈ ⟦q⟧_I|}`. -/
    112axiom eval_proj : ∀ {n k : ℕ} (ts : Tuple (Term T k) n) (q : Query T k) (d : Database T),
    113 Query.evaluate (Query.Proj ts q) d = (Query.evaluate q d).map (fun u l => (ts l).eval u)
    114
    115/-- **selection**: `⟦σ_φ(q)⟧_I ≝ {|u | u ∈ ⟦q⟧_I, φ(u)|}`. -/
    116axiom eval_sel : ∀ {n : ℕ} (φ : Selection T n) (q : Query T n) (d : Database T),
    117 Query.evaluate (Query.Sel φ q) d = @Multiset.filter _ φ.eval φ.evalDecidable (Query.evaluate q d)
    118
    119/-- **cross product**: `⟦q₁ × q₂⟧_I ≝ ⟦q₁⟧_I × ⟦q₂⟧_I`. -/
    120axiom eval_prod : ∀ {n k₁ k₂ : ℕ} {hn : k₁ + k₂ = n} (q₁ : Query T k₁) (q₂ : Query T k₂) (d : Database T),
    121 Query.evaluate (Query.Prod (hn := hn) q₁ q₂) d = ((Query.evaluate q₁ d) * (Query.evaluate q₂ d)).cast hn
    122
    123/-- **multiset sum**: `⟦q₁ ⊎ q₂⟧_I ≝ ⟦q₁⟧_I ⊎ ⟦q₂⟧_I`. -/
    124axiom eval_sum : ∀ {n : ℕ} (q₁ q₂ : Query T n) (d : Database T),
    125 Query.evaluate (Query.Sum q₁ q₂) d = Query.evaluate q₁ d + Query.evaluate q₂ d
    126
    127/-- **duplicate elimination**: `⟦ε(q)⟧_I` maps `t` to `1` when `⟦q⟧_I(t) > 0`
    128and to `0` otherwise. -/
    129axiom eval_dedup : ∀ {n : ℕ} (q : Query T n) (d : Database T),
    130 Query.evaluate (Query.Dedup q) d = (Query.evaluate q d).dedup
    131
    132/-- **multiset difference**: every copy of a tuple occurring at all in `⟦q₂⟧_I`
    133is removed from `⟦q₁⟧_I`. -/
    134axiom eval_diff : ∀ {n : ℕ} (q₁ q₂ : Query T n) (d : Database T) (r₂ : Multiset (Tuple T n)),
    135 r₂ = Query.evaluate q₂ d →
    136 Query.evaluate (Query.Diff q₁ q₂) d = (Query.evaluate q₁ d).filter (fun u => u ∉ r₂)
    137
    138end Lax392996.MultisetSemantics
    139
    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…