Lax Lean Archive

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

The relational algebra with multiset semantics, as syntax

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

definition

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 syntax of the queries. Terms over a tuple of arity kk are constants, attributes #i\#i for i<ki < k, and sums, differences and products of terms; selection conditions are Boolean combinations of comparisons between terms. The queries of arity kk are generated by the grammar of the paper: relation names RR, projections Πt1,…,tn(q)\Pi_{t_1, \dots, t_n}(q) on a tuple of terms, selections σφ(q)\sigma_\varphi(q), cross products q1×q2q_1 \times q_2, multiset sums q1⊎q2q_1 \uplus q_2, duplicate elimination ε(q)\varepsilon(q) and multiset difference q1−q2q_1 - q_2; the join q1⋈φq2=σφ(q1×q2)q_1 \bowtie_\varphi q_2 = \sigma_\varphi(q_1 \times q_2) and the set union q1∪q2=ε(q1⊎q2)q_1 \cup q_2 = \varepsilon(q_1 \uplus q_2) are syntactic sugar. The type carries two further operators, the provenance aggregation γ\gamma that the rewriting of duplicate elimination and difference emits, and a fused HAVINGHAVING operator; a source query is one written without them.

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

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Logic.Basic
    2import Mathlib.Data.Nat.Init
    3import Mathlib.Order.Defs.LinearOrder
    4import Mathlib.Data.Fin.VecNotation
    5import Mathlib.Data.Multiset.Basic
    6import Lax392996.Databases
    7
    8/-!
    9---
    10title: The relational algebra with multiset semantics, as syntax
    11type: definition
    12---
    13The syntax of the queries. Terms over a tuple of arity kk are constants,
    14attributes #i\#i for i<ki < k, and sums, differences and products of terms;
    15selection conditions are Boolean combinations of comparisons between terms.
    16The queries of arity kk are generated by the grammar of the paper:
    17relation names RR, projections Πt1,…,tn(q)\Pi_{t_1, \dots, t_n}(q) on a tuple of
    18terms, selections σφ(q)\sigma_\varphi(q), cross products q1×q2q_1 \times q_2,
    19multiset sums q1⊎q2q_1 \uplus q_2, duplicate elimination ε(q)\varepsilon(q) and
    20multiset difference q1−q2q_1 - q_2; the join q1⋈φq2=σφ(q1×q2)q_1 \bowtie_\varphi q_2 = \sigma_\varphi(q_1 \times q_2)
    21 and the set union q1∪q2=ε(q1⊎q2)q_1 \cup q_2 = \varepsilon(q_1 \uplus q_2)
    22 are syntactic sugar. The type carries two
    23further operators, the provenance aggregation γ\gamma that the rewriting of
    24duplicate elimination and difference emits, and a fused `HAVING` operator;
    25a source query is one written without them.
    26-/
    27
    28namespace Lax392996.RelationalAlgebra
    29
    30open Lax392996.Databases
    31
    32universe u v
    33
    34variable {T : Type} [ValueType T]
    35
    36/-- Comparison operator, as used by the `HAVING` operator. -/
    37inductive CompOp where
    38 | eq | ne | lt | le | gt | ge
    39 deriving DecidableEq, Repr
    40
    41/-- Semantics of a comparison operator over any linearly ordered value
    42domain. -/
    43def CompOp.eval {V : Type u} [LinearOrder V] : CompOp → V → V → Prop
    44 | .eq, a, b => a = b
    45 | .ne, a, b => a ≠ b
    46 | .lt, a, b => a < b
    47 | .le, a, b => a ≤ b
    48 | .gt, a, b => a > b
    49 | .ge, a, b => a ≥ b
    50
    51instance instDecidableEval {V : Type u} [LinearOrder V] (op : CompOp) (a b : V) :
    52 Decidable (op.eval a b) := by
    53 cases op <;> simp only [CompOp.eval] <;> infer_instance
    54
    55/-- A term over a tuple of arity `n`: a constant, an attribute, or an
    56arithmetic combination. -/
    57inductive Term (T : Sort u) (n : ℕ) where
    58| const : T → Term T n
    59| index : Fin n → Term T n
    60| add : Term T n → Term T n → Term T n
    61| sub : Term T n → Term T n → Term T n
    62| mul : Term T n → Term T n → Term T n
    63
    64/-- A term read on the composite tuple: constants become data values,
    65attributes keep their index, the annotation column being the last one. -/
    66def Term.castToAnnotatedTuple {n : ℕ} {K : Type v} (t: Term T n) : Term (T⊕K) (n+1) := match t with
    67| Term.const c => Term.const (Sum.inl c)
    68| Term.index k => Term.index (k.castLT (k.val_lt_of_le (Nat.le_add_right n 1)))
    69| Term.add t₁ t₂ => Term.add t₁.castToAnnotatedTuple t₂.castToAnnotatedTuple
    70| Term.sub t₁ t₂ => Term.sub t₁.castToAnnotatedTuple t₂.castToAnnotatedTuple
    71| Term.mul t₁ t₂ => Term.mul t₁.castToAnnotatedTuple t₂.castToAnnotatedTuple
    72
    73/-- The value of a term on a tuple. -/
    74def Term.eval {n : ℕ} (term: Term T n) (tuple: Tuple T n) := match term with
    75 | Term.const a => a
    76 | Term.index k => tuple k
    77 | Term.add t₁ t₂ => (t₁.eval tuple) + (t₂.eval tuple)
    78 | Term.sub t₁ t₂ => (t₁.eval tuple) - (t₂.eval tuple)
    79 | Term.mul t₁ t₂ => (t₁.eval tuple) * (t₂.eval tuple)
    80
    81/-- A comparison between two terms. -/
    82inductive BoolTerm (T : Sort u) (n: ℕ) where
    83| EQ : Term T n → Term T n → BoolTerm T n
    84| NE : Term T n → Term T n → BoolTerm T n
    85| LE : Term T n → Term T n → BoolTerm T n
    86| LT : Term T n → Term T n → BoolTerm T n
    87| GE : Term T n → Term T n → BoolTerm T n
    88| GT : Term T n → Term T n → BoolTerm T n
    89
    90/-- A comparison read on the composite tuple. -/
    91def BoolTerm.castToAnnotatedTuple {n : ℕ} {K : Type v} (bt: BoolTerm T n): BoolTerm (T⊕K) (n+1) :=
    92 match bt with
    93 | BoolTerm.EQ a b => BoolTerm.EQ a.castToAnnotatedTuple b.castToAnnotatedTuple
    94 | BoolTerm.NE a b => BoolTerm.NE a.castToAnnotatedTuple b.castToAnnotatedTuple
    95 | BoolTerm.LE a b => BoolTerm.LE a.castToAnnotatedTuple b.castToAnnotatedTuple
    96 | BoolTerm.LT a b => BoolTerm.LT a.castToAnnotatedTuple b.castToAnnotatedTuple
    97 | BoolTerm.GE a b => BoolTerm.GE a.castToAnnotatedTuple b.castToAnnotatedTuple
    98 | BoolTerm.GT a b => BoolTerm.GT a.castToAnnotatedTuple b.castToAnnotatedTuple
    99
    100/-- The truth of a comparison on a tuple. -/
    101def BoolTerm.eval {n : ℕ} (φ: BoolTerm T n) (tuple: Tuple T n) := match φ with
    102| BoolTerm.EQ t₁ t₂ => (t₁.eval tuple) = (t₂.eval tuple)
    103| BoolTerm.NE t₁ t₂ => (t₁.eval tuple) ≠ (t₂.eval tuple)
    104| BoolTerm.LE t₁ t₂ => (t₁.eval tuple) ≤ (t₂.eval tuple)
    105| BoolTerm.LT t₁ t₂ => (t₁.eval tuple) < (t₂.eval tuple)
    106| BoolTerm.GE t₁ t₂ => (t₁.eval tuple) ≥ (t₂.eval tuple)
    107| BoolTerm.GT t₁ t₂ => (t₁.eval tuple) > (t₂.eval tuple)
    108
    109@[reducible] def BoolTerm.evalDecidable {n : ℕ} (φ: BoolTerm T n) : DecidablePred φ.eval :=
    110 λ t => by
    111 cases φ with
    112 | EQ x y => simp [BoolTerm.eval]; exact (inferInstance : Decidable (x.eval t = y.eval t))
    113 | NE x y => simp [BoolTerm.eval]; exact (inferInstance : Decidable (x.eval t ≠ y.eval t))
    114 | LE x y => simp [BoolTerm.eval]; exact (inferInstance : Decidable (x.eval t ≤ y.eval t))
    115 | LT x y => simp [BoolTerm.eval]; exact (inferInstance : Decidable (x.eval t < y.eval t))
    116 | GE x y => simp [BoolTerm.eval]; exact (inferInstance : Decidable (y.eval t ≤ x.eval t))
    117 | GT x y => simp [BoolTerm.eval]; exact (inferInstance : Decidable (y.eval t < x.eval t))
    118
    119/-- A selection condition: a Boolean combination of comparisons. -/
    120inductive Selection (T : Sort u) (n: ℕ) where
    121| BT : BoolTerm T n → Selection T n
    122| Not : Selection T n → Selection T n
    123| And : Selection T n → Selection T n → Selection T n
    124| Or : Selection T n → Selection T n → Selection T n
    125| True : Selection T n
    126
    127/-- A selection condition read on the composite tuple. -/
    128def Selection.castToAnnotatedTuple {n : ℕ} {K : Type v} (f: Selection T n): Selection (T⊕K) (n+1) := match f with
    129| Selection.BT t => Selection.BT t.castToAnnotatedTuple
    130| Selection.Not φ => Selection.Not φ.castToAnnotatedTuple
    131| Selection.And φ₁ φ₂ => Selection.And φ₁.castToAnnotatedTuple φ₂.castToAnnotatedTuple
    132| Selection.Or φ₁ φ₂ => Selection.Or φ₁.castToAnnotatedTuple φ₂.castToAnnotatedTuple
    133| Selection.True => Selection.True
    134
    135/-- The truth of a selection condition on a tuple. -/
    136def Selection.eval {n : ℕ} (φ: Selection T n) (tuple: Tuple T n) := match φ with
    137| Selection.BT φ => φ.eval tuple
    138| Selection.Not φ => ¬ (φ.eval tuple)
    139| Selection.And φ₁ φ₂ => (φ₁.eval tuple) ∧ (φ₂.eval tuple)
    140| Selection.Or φ₁ φ₂ => (φ₁.eval tuple) ∨ (φ₂.eval tuple)
    141| Selection.True => true
    142
    143@[reducible] def Selection.evalDecidable {n : ℕ} (φ : Selection T n) : DecidablePred φ.eval :=
    144 λ t => match φ with
    145 | Selection.BT φ => φ.evalDecidable t
    146 | Selection.Not φ => match φ.evalDecidable t with
    147 | isTrue h => isFalse (by simp [Selection.eval, h])
    148 | isFalse h => isTrue (by simp [Selection.eval, h])
    149 | Selection.And φ₁ φ₂ => match φ₁.evalDecidable t, φ₂.evalDecidable t with
    150 | isTrue h₁, isTrue h₂ => isTrue (by simp [Selection.eval, h₁, h₂])
    151 | isFalse h, _ | _, isFalse h => isFalse (by simp [Selection.eval, h])
    152 | Selection.Or φ₁ φ₂ => match φ₁.evalDecidable t, φ₂.evalDecidable t with
    153 | isTrue h, _ | _, isTrue h => isTrue (by simp [Selection.eval, h])
    154 | isFalse h₁, isFalse h₂ => isFalse (by simp [Selection.eval, h₁, h₂])
    155 | Selection.True => isTrue (rfl)
    156
    157/-- An aggregate function on sequences of values, the aggregate interface
    158of the fused `HAVING` operator. -/
    159def SeqAggFunc (T : Type) := List T → T
    160
    161/-- The queries, indexed by arity: the operators of the paper's grammar,
    162the provenance aggregation `ProvSum` that the rewriting emits, and the
    163fused `HAVING` operator. -/
    164inductive Query (T: Type) : ℕ → Type
    165| Rel : (n: ℕ) → String → Query T n
    166| Proj {n m : ℕ} : Tuple (Term T n) m → Query T n → Query T m
    167| Sel {n : ℕ} : Selection T n → Query T n → Query T n
    168| Prod {n₁ n₂ n : ℕ} {hn: n₁+n₂=n} : Query T n₁ → Query T n₂ → Query T n
    169| Sum {n : ℕ} : Query T n → Query T n → Query T n
    170| Dedup {n : ℕ} : Query T n → Query T n
    171| Diff {n : ℕ} : Query T n → Query T n → Query T n
    172/-- Provenance aggregation: group by the key columns of the first
    173argument and `⊕`-sum the term of the second over each group into a single
    174trailing output column. It is the target of the rewriting of duplicate
    175elimination and of difference. -/
    176| ProvSum {m n₁ : ℕ} : Tuple (Fin m) n₁ → Term T m → Query T m → Query T (n₁+1)
    177/-- The fused `HAVING` operator: grouping by the indices of the first
    178argument, computing the sequence aggregates of the third argument applied
    179to the terms of the second, each group read in the canonical tuple order,
    180and keeping only the groups whose aggregate value in column `l` compares,
    181through the comparison operator, with the value of the term on the group
    182key. The output has the group key followed by the aggregate values. -/
    183| Having {m n₁ n₂ : ℕ} : Tuple (Fin m) n₁ → Tuple (Term T m) n₂ → Tuple (SeqAggFunc T) n₂ →
    184 CompOp → Fin n₂ → Term T n₁ → Query T m → Query T (n₁+n₂)
    185
    186/-- The source fragment: the queries written with the operators of the
    187paper's grammar only, without `ProvSum` and `Having`. -/
    188def Query.source {n : ℕ} (q: Query T n): Prop := match q with
    189| Query.Rel n s => True
    190| Query.Proj _ q => q.source
    191| Query.Sel _ q => q.source
    192| Query.Prod q₁ q₂ => q₁.source ∧ q₂.source
    193| Query.Sum q₁ q₂ => q₁.source ∧ q₂.source
    194| Query.Dedup q => q.source
    195| Query.Diff q₁ q₂ => q₁.source ∧ q₂.source
    196| Query.ProvSum _ _ q => False
    197| Query.Having _ _ _ _ _ _ _ => False
    198
    199/-- The arguments of a source cross product are source queries. A proof
    200carried as a definition, since the concept dialect has no theorem command;
    201the recursive definitions over source queries use it. -/
    202def Query.source_prod {n n₂ : ℕ} {q: Query T n} :
    203 q.source → ∀ {n₁} {q₁: Query T n₁} {q₂: Query T n₂} {hn: n₁+n₂=n}
    204 (_: q = @Query.Prod T n₁ n₂ n hn q₁ q₂), q₁.source ∧ q₂.source := by
    205 intro hna n₁ q₁ q₂ hn₁ hq
    206 unfold Query.source at hna
    207 simp[hq] at hna
    208 assumption
    209
    210/-- The arguments of a source multiset sum are source queries. -/
    211def Query.source_sum {n : ℕ} {q: Query T n} :
    212 q.source → ∀ {q₁: Query T n} {q₂: Query T n} (_: q = Query.Sum q₁ q₂), q₁.source ∧ q₂.source := by
    213 intro hna q₁ q₂ hq
    214 unfold Query.source at hna
    215 simp[hq] at hna
    216 assumption
    217
    218/-- The arguments of a source difference are source queries. -/
    219def Query.source_diff {n : ℕ} {q: Query T n} :
    220 q.source → ∀ {q₁: Query T n} {q₂: Query T n} (_: q = Query.Diff q₁ q₂), q₁.source ∧ q₂.source := by
    221 intro hna q₁ q₂ hq
    222 unfold Query.source at hna
    223 simp[hq] at hna
    224 assumption
    225
    226/-- The argument of a source projection is a source query. -/
    227def Query.source_proj {n : ℕ} {q: Query T n} :
    228 q.source → ∀ {m} {t} {q': Query T m} (_: q = Query.Proj t q'), q'.source := by
    229 intro hna m t q' hq
    230 unfold Query.source at hna
    231 rw[hq] at hna
    232 assumption
    233
    234/-- The argument of a source selection is a source query. -/
    235def Query.source_sel {n : ℕ} {q: Query T n} :
    236 q.source → ∀ {φ} {q': Query T n} (_: q = Query.Sel φ q'), q'.source := by
    237 intro hna φ q' hq
    238 unfold Query.source at hna
    239 rw[hq] at hna
    240 assumption
    241
    242/-- The argument of a source duplicate elimination is a source query. -/
    243def Query.source_dedup {n : ℕ} {q: Query T n} :
    244 q.source → ∀ {q': Query T n} (_: q = Query.Dedup q'), q'.source := by
    245 intro hna q' hq
    246 unfold Query.source at hna
    247 rw[hq] at hna
    248 assumption
    249
    250/-- The arity of a query. -/
    251def Query.arity {n : ℕ} (_: Query T n) := n
    252
    253/-- The measure the recursive semantics is defined along: the depth of the
    254query, aggregation operators counting for three. -/
    255def Query.aggdepth2_plus_depth {n : ℕ} (q: Query T n) : ℕ := match q with
    256| Query.Rel n s => 0
    257| Query.Proj _ q => let d := q.aggdepth2_plus_depth; d+1
    258| Query.Sel _ q => let d := q.aggdepth2_plus_depth; d+1
    259| Query.Prod q₁ q₂ =>
    260 let d₁ := q₁.aggdepth2_plus_depth
    261 let d₂ := q₂.aggdepth2_plus_depth
    262 (max d₁ d₂)+1
    263| Query.Sum q₁ q₂ =>
    264 let d₁ := q₁.aggdepth2_plus_depth
    265 let d₂ := q₂.aggdepth2_plus_depth
    266 (max d₁ d₂)+1
    267| Query.Dedup q => let d := q.aggdepth2_plus_depth; d+1
    268| Query.Diff q₁ q₂ =>
    269 let d₁ := q₁.aggdepth2_plus_depth
    270 let d₂ := q₂.aggdepth2_plus_depth
    271 (max d₁ d₂)+1
    272| Query.ProvSum _ _ q => let d := q.aggdepth2_plus_depth; (d+3)
    273| Query.Having _ _ _ _ _ _ q => let d := q.aggdepth2_plus_depth; (d+3)
    274
    275end Lax392996.RelationalAlgebra
    276
    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…