Relational algebra

This file defines the abstract syntax and semantics of relational algebra queries over plain (unannotated) databases. The language is the extended relational algebra described in Section III of Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data, with multiset semantics, explicit duplicate elimination, multiset difference, and aggregation.

Main definitions

• Term T n – an expression that evaluates to a value of type T in the context of a tuple of arity n (constants, tuple projections, and arithmetic operations)
• Query T – a relational algebra query: selection, projection, union, join, difference, and renaming
• Query.evaluate – the standard set semantics of queries over Database T

References

• Sen, Maniu & Senellart, ProvSQL (Section III)

inductive Term (T : Sort u_1) (n : ℕ) : Sort (max 1 u_1)

• const {T : Sort u_1} {n : ℕ} : T → Term T n
• index {T : Sort u_1} {n : ℕ} : Fin n → Term T n
• add {T : Sort u_1} {n : ℕ} : Term T n → Term T n → Term T n
• sub {T : Sort u_1} {n : ℕ} : Term T n → Term T n → Term T n
• mul {T : Sort u_1} {n : ℕ} : Term T n → Term T n → Term T n

def Term.repr {T : Type} {n : ℕ} [Repr T] : Term T n → ℕ → Std.Format

Equations

• (Term.const a).repr x✝ = reprArg a
• (#k).repr x✝ = Std.Format.text "#" ++ reprArg k
• (t₁.add t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "+" ++ t₂.repr x✝) x✝
• (t₁.sub t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "-" ++ t₂.repr x✝) x✝
• (t₁.mul t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "*" ++ t₂.repr x✝) x✝

@[instance_reducible]

instance instReprTerm {α : Type} {n : ℕ} [Repr α] : Repr (Term α n)

Equations

• instReprTerm = { reprPrec := Term.repr }

def Term.castToAnnotatedTuple {T : Type} {n : ℕ} {K : Type u_1} (t : Term T n) : Term (T ⊕ K) (n + 1)

Equations

• (Term.const c).castToAnnotatedTuple = Term.const (Sum.inl c)
• (#k).castToAnnotatedTuple = #(k.castLT ⋯)
• (t₁.add t₂).castToAnnotatedTuple = t₁.castToAnnotatedTuple.add t₂.castToAnnotatedTuple
• (t₁.sub t₂).castToAnnotatedTuple = t₁.castToAnnotatedTuple.sub t₂.castToAnnotatedTuple
• (t₁.mul t₂).castToAnnotatedTuple = t₁.castToAnnotatedTuple.mul t₂.castToAnnotatedTuple

def Term.eval {T : Type} [ValueType T] {n : ℕ} (term : Term T n) (tuple : Tuple T n) : T

Equations

• (Term.const c).eval tuple = c
• (#k).eval tuple = tuple k
• (t₁.add t₂).eval tuple = t₁.eval tuple + t₂.eval tuple
• (t₁.sub t₂).eval tuple = t₁.eval tuple - t₂.eval tuple
• (t₁.mul t₂).eval tuple = t₁.eval tuple * t₂.eval tuple

theorem Term.castToAnnotatedTuple_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} [HasAltLinearOrder K] [SemiringWithMonus K] (t : Term T n) (tuple : Tuple T n) (α : K) : t.castToAnnotatedTuple.eval (Fin.append (fun (k : Fin n) => Sum.inl (tuple k)) ![Sum.inr α]) = Sum.inl (t.eval tuple)

@[instance_reducible]

instance instCoeTerm {T : Type} {n : ℕ} : Coe T (Term T n)

Equations

• instCoeTerm = { coe := fun (a : T) => Term.const a }

@[instance_reducible]

instance instOfNatTermNat {n a : ℕ} : OfNat (Term ℕ n) a

Equations

• instOfNatTermNat = { ofNat := Term.const a }

def «term#_» : Lean.ParserDescr

Equations

• «term#_» = Lean.ParserDescr.node `«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

inductive BoolTerm (T : Sort u_1) (n : ℕ) : Sort (max 1 u_1)

• EQ {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• NE {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• LE {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• LT {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• GE {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n
• GT {T : Sort u_1} {n : ℕ} : Term T n → Term T n → BoolTerm T n

def BoolTerm.repr {T : Type} {n : ℕ} [Repr T] : BoolTerm T n → ℕ → Std.Format

Equations

• (BoolTerm.EQ t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "==" ++ t₂.repr x✝) x✝
• (BoolTerm.NE t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "!=" ++ t₂.repr x✝) x✝
• (BoolTerm.LE t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "<=" ++ t₂.repr x✝) x✝
• (BoolTerm.LT t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "<" ++ t₂.repr x✝) x✝
• (BoolTerm.GE t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text ">=" ++ t₂.repr x✝) x✝
• (BoolTerm.GT t₁ t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text ">" ++ t₂.repr x✝) x✝

@[instance_reducible]

instance instReprBoolTerm {α : Type} {n : ℕ} [Repr α] : Repr (BoolTerm α n)

Equations

• instReprBoolTerm = { reprPrec := BoolTerm.repr }

def BoolTerm.castToAnnotatedTuple {T : Type} {n : ℕ} {K : Type u_1} (bt : BoolTerm T n) : BoolTerm (T ⊕ K) (n + 1)

Equations

• (BoolTerm.EQ a b).castToAnnotatedTuple = BoolTerm.EQ a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.NE a b).castToAnnotatedTuple = BoolTerm.NE a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.LE a b).castToAnnotatedTuple = BoolTerm.LE a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.LT a b).castToAnnotatedTuple = BoolTerm.LT a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.GE a b).castToAnnotatedTuple = BoolTerm.GE a.castToAnnotatedTuple b.castToAnnotatedTuple
• (BoolTerm.GT a b).castToAnnotatedTuple = BoolTerm.GT a.castToAnnotatedTuple b.castToAnnotatedTuple

def «term_==__1» : Lean.TrailingParserDescr

Equations

• «term_==__1» = Lean.ParserDescr.trailingNode `«term_==__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " == ") (Lean.ParserDescr.cat `term 21))

def «term_!=__1» : Lean.TrailingParserDescr

Equations

• «term_!=__1» = Lean.ParserDescr.trailingNode `«term_!=__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " != ") (Lean.ParserDescr.cat `term 21))

def «term_<=__1» : Lean.TrailingParserDescr

Equations

• «term_<=__1» = Lean.ParserDescr.trailingNode `«term_<=__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <= ") (Lean.ParserDescr.cat `term 21))

def «term_<__1» : Lean.TrailingParserDescr

Equations

• «term_<__1» = Lean.ParserDescr.trailingNode `«term_<__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " < ") (Lean.ParserDescr.cat `term 21))

def «term_>=__1» : Lean.TrailingParserDescr

Equations

• «term_>=__1» = Lean.ParserDescr.trailingNode `«term_>=__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >= ") (Lean.ParserDescr.cat `term 21))

def «term_>__1» : Lean.TrailingParserDescr

Equations

• «term_>__1» = Lean.ParserDescr.trailingNode `«term_>__1» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " > ") (Lean.ParserDescr.cat `term 21))

def BoolTerm.eval {T : Type} [ValueType T] {n : ℕ} (φ : BoolTerm T n) (tuple : Tuple T n) : Prop

Equations

• (BoolTerm.EQ a b).eval tuple = (a.eval tuple = b.eval tuple)
• (BoolTerm.NE a b).eval tuple = (a.eval tuple ≠ b.eval tuple)
• (BoolTerm.LE a b).eval tuple = (a.eval tuple ≤ b.eval tuple)
• (BoolTerm.LT a b).eval tuple = (a.eval tuple < b.eval tuple)
• (BoolTerm.GE a b).eval tuple = (a.eval tuple ≥ b.eval tuple)
• (BoolTerm.GT a b).eval tuple = (a.eval tuple > b.eval tuple)

theorem BoolTerm.castToAnnotatedTuple_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} [HasAltLinearOrder K] [SemiringWithMonus K] (t : BoolTerm T n) (tuple : Tuple T n) (α : K) : t.castToAnnotatedTuple.eval (Fin.append (fun (k : Fin n) => Sum.inl (tuple k)) ![Sum.inr α]) = t.eval tuple

@[reducible]

def BoolTerm.evalDecidable {T : Type} [ValueType T] {n : ℕ} (φ : BoolTerm T n) : DecidablePred φ.eval

Equations

• One or more equations did not get rendered due to their size.

inductive Selection (T : Sort u_1) (n : ℕ) : Sort (max 1 u_1)

• BT {T : Sort u_1} {n : ℕ} : BoolTerm T n → Selection T n
• Not {T : Sort u_1} {n : ℕ} : Selection T n → Selection T n
• And {T : Sort u_1} {n : ℕ} : Selection T n → Selection T n → Selection T n
• Or {T : Sort u_1} {n : ℕ} : Selection T n → Selection T n → Selection T n
• True {T : Sort u_1} {n : ℕ} : Selection T n

def Selection.repr {T : Type} {n : ℕ} [Repr T] : Selection T n → ℕ → Std.Format

Equations

• (Selection.BT t).repr x✝ = t.repr x✝
• f.Not.repr x✝ = Std.Format.text "¬" ++ Repr.addAppParen (f.repr x✝) x✝
• (t₁.And t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "∧" ++ t₂.repr x✝) x✝
• (t₁.Or t₂).repr x✝ = Repr.addAppParen (t₁.repr x✝ ++ Std.Format.text "∨" ++ t₂.repr x✝) x✝
• Selection.True.repr x✝ = Std.Format.text "True"

@[instance_reducible]

instance instReprSelection {α : Type} {n : ℕ} [Repr α] : Repr (Selection α n)

Equations

• instReprSelection = { reprPrec := Selection.repr }

def Selection.castToAnnotatedTuple {T : Type} {n : ℕ} {K : Type u_1} (f : Selection T n) : Selection (T ⊕ K) (n + 1)

Equations

• (Selection.BT t).castToAnnotatedTuple = Selection.BT t.castToAnnotatedTuple
• φ.Not.castToAnnotatedTuple = φ.castToAnnotatedTuple.Not
• (φ₁.And φ₂).castToAnnotatedTuple = φ₁.castToAnnotatedTuple.And φ₂.castToAnnotatedTuple
• (φ₁.Or φ₂).castToAnnotatedTuple = φ₁.castToAnnotatedTuple.Or φ₂.castToAnnotatedTuple
• Selection.True.castToAnnotatedTuple = Selection.True

def Selection.eval {T : Type} [ValueType T] {n : ℕ} (φ : Selection T n) (tuple : Tuple T n) : Prop

Equations

• (Selection.BT t).eval tuple = t.eval tuple
• φ_1.Not.eval tuple = ¬φ_1.eval tuple
• (φ₁.And φ₂).eval tuple = (φ₁.eval tuple ∧ φ₂.eval tuple)
• (φ₁.Or φ₂).eval tuple = (φ₁.eval tuple ∨ φ₂.eval tuple)
• Selection.True.eval tuple = (true = true)

theorem Selection.castToAnnotatedTuple_eval {T : Type} [ValueType T] {K : Type} {n : ℕ} [HasAltLinearOrder K] [SemiringWithMonus K] (φ : Selection T n) (tuple : Tuple T n) (α : K) : φ.castToAnnotatedTuple.eval (Fin.append (fun (k : Fin n) => Sum.inl (tuple k)) ![Sum.inr α]) = φ.eval tuple

@[reducible]

def Selection.evalDecidable {T : Type} [ValueType T] {n : ℕ} (φ : Selection T n) : DecidablePred φ.eval

Equations

• (Selection.BT t_1).evalDecidable t = t_1.evalDecidable t
• φ_1.Not.evalDecidable t = match φ_1.evalDecidable t with | isTrue h => isFalse ⋯ | isFalse h => isTrue ⋯
• (φ₁.And φ₂).evalDecidable t = match φ₁.evalDecidable t, φ₂.evalDecidable t with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h, x => isFalse ⋯ | x, isFalse h => isFalse ⋯
• (φ₁.Or φ₂).evalDecidable t = match φ₁.evalDecidable t, φ₂.evalDecidable t with | isTrue h, x => isTrue ⋯ | x, isTrue h => isTrue ⋯ | isFalse h₁, isFalse h₂ => isFalse ⋯
• Selection.True.evalDecidable t = isTrue ⋯

@[instance_reducible]

instance instCoeBoolTermSelection {T : Type} {n : ℕ} : Coe (BoolTerm T n) (Selection T n)

Equations

• instCoeBoolTermSelection = { coe := fun (bt : BoolTerm T n) => Selection.BT bt }

def addFn {T : Type} [ValueType T] (a b : T) : T

Addition as a binary function, the fold of the ⊕-sum performed by the rewriting-target operator Query.ProvSum (and by its general-syntax counterpart AggQuery.ProvSum).

Equations

• addFn a b = a + b

instance instCommutativeAddFn {T : Type} [ValueType T] : Std.Commutative addFn

instance instAssociativeAddFn {T : Type} [ValueType T] : Std.Associative addFn

def SeqAggFunc (T : Type) : Type

An aggregate function on sequences of values: an arbitrary function from finite sequences over T to T. Beyond the monoid-shaped ⊕-sum of Query.ProvSum, this interface covers non-commutative aggregates – such as PICKFIRST, whose result depends on the order of its input – and non-associative ones. It is the aggregate interface of the fused Having operator, whose possible-world semantics does not need any algebraic structure on the aggregate.

Equations

• SeqAggFunc T = (List T → T)

def SeqAggFunc.sum {T : Type} [ValueType T] : SeqAggFunc T

SUM as a sequence aggregate.

Equations

• SeqAggFunc.sum L = List.foldr (fun (x1 x2 : T) => x1 + x2) 0 L

def SeqAggFunc.count : SeqAggFunc ℕ

COUNT(*) as a sequence aggregate (over an ℕ-valued domain).

Equations

• SeqAggFunc.count = List.length

def SeqAggFunc.minD {T : Type} [ValueType T] : SeqAggFunc T

MIN, with value 0 on the empty sequence (the possible-world semantics only ever applies it to non-empty sequences).

Equations

• SeqAggFunc.minD [] = 0
• SeqAggFunc.minD (x :: xs) = List.foldr min x xs

def SeqAggFunc.maxD {T : Type} [ValueType T] : SeqAggFunc T

MAX, with value 0 on the empty sequence.

Equations

• SeqAggFunc.maxD [] = 0
• SeqAggFunc.maxD (x :: xs) = List.foldr max x xs

def SeqAggFunc.pickFirst {T : Type} [ValueType T] : SeqAggFunc T

PICKFIRST: the first value of the sequence, 0 if empty.

Equations

• SeqAggFunc.pickFirst L = L.headD 0

inductive Query (T : Type) : ℕ → Type

• Rel {T : Type} (n : ℕ) : String → Query T n
• Proj {T : Type} {n m : ℕ} : Tuple (Term T n) m → Query T n → Query T m
• Sel {T : Type} {n : ℕ} : Selection T n → Query T n → Query T n
• Prod {T : Type} {n₁ n₂ n : ℕ} {hn : n₁ + n₂ = n} : Query T n₁ → Query T n₂ → Query T n
• Sum {T : Type} {n : ℕ} : Query T n → Query T n → Query T n
• Dedup {T : Type} {n : ℕ} : Query T n → Query T n
• Diff {T : Type} {n : ℕ} : Query T n → Query T n → Query T n
• ProvSum {T : Type} {m n₁ : ℕ} : Tuple (Fin m) n₁ → Term T m → Query T m → Query T (n₁ + 1)

  Provenance aggregation: group by the key columns of the first argument and ⊕-sum the term of the second over each group into a single trailing output column. It is not a source operator – aggregation as such lives on the general syntax (AggQuery.Gamma) – but the target of the (R1)–(R4) rewriting: the ⊕-gate creation of the ε and ∖ rules of Query.rewriting. Its general-syntax counterpart is AggQuery.ProvSum.

• Having {T : Type} {m n₁ n₂ : ℕ} : Tuple (Fin m) n₁ → Tuple (Term T m) n₂ → Tuple (SeqAggFunc T) n₂ → CompOp → Fin n₂ → Term T n₁ → Query T m → Query T (n₁ + n₂)

  The fused HAVING operator: grouping by the indices of the first argument, computing the sequence aggregates of the third argument applied to the terms of the second (each group read in the canonical tuple order, which plays the role of the ordering ≼ of non-commutative aggregates), and keeping only the groups whose aggregate value in column l (the Fin n₂ argument) compares, via the comparison operator, with the value of the regular term (the Term T n₁ argument, evaluated on the group key – this covers both query constants and group-key attributes). The output has the group key followed by the aggregate values.

def Query.repr {T : Type} {n : ℕ} [Repr T] : Query T n → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• (Query.Rel n s).repr x✝ = Std.Format.text s
• (Π ts q).repr x✝ = Std.Format.text "Π_" ++ Repr.addAppParen (ts.repr x✝) x✝ ++ Repr.addAppParen (q.repr x✝) x✝
• (σ φ q).repr x✝ = Std.Format.text "σ_" ++ Repr.addAppParen (φ.repr x✝) x✝ ++ Repr.addAppParen (q.repr x✝) x✝
• (q₁ × q₂).repr x✝ = Repr.addAppParen (q₁.repr x✝ ++ Std.Format.text "×" ++ q₂.repr x✝) x✝
• (q₁ ⊎ q₂).repr x✝ = Repr.addAppParen (q₁.repr x✝ ++ Std.Format.text "⊎" ++ q₂.repr x✝) x✝
• (ε q).repr x✝ = Std.Format.text "ε" ++ Repr.addAppParen (q.repr x✝) x✝
• (q₁ - q₂).repr x✝ = Repr.addAppParen (q₁.repr x✝ ++ Std.Format.text "-" ++ q₂.repr x✝) x✝
• (Query.ProvSum is t q).repr x✝ = Std.Format.text "γ⊕_" ++ Repr.addAppParen (is.repr x✝) x✝ ++ Repr.addAppParen (t.repr x✝) x✝ ++ Repr.addAppParen (q.repr x✝) x✝

@[instance_reducible]

instance instReprQuery {α : Type} {n : ℕ} [Repr α] : Repr (Query α n)

Equations

• instReprQuery = { reprPrec := Query.repr }

def Query.source {T : Type} {n : ℕ} (q : Query T n) : Prop

The source fragment of the classical syntax: the operators a query is written with, RA⁺(∖). It excludes the two operators that are not source operators – ProvSum, which the (R1)–(R4) rewriting emits, and the fused Having, whose semantics lives on the general syntax – and is exactly the fragment carrying an annotated semantics (Query.evaluateAnnotated) and accepted by Query.rewriting. Its general-syntax counterpart is AggQuery.classical.

Equations

• (Query.Rel n s).source = True
• (Π a q_2).source = q_2.source
• (σ a q_2).source = q_2.source
• (q₁ × q₂).source = (q₁.source ∧ q₂.source)
• (q₁ ⊎ q₂).source = (q₁.source ∧ q₂.source)
• (ε q_2).source = q_2.source
• (q₁ - q₂).source = (q₁.source ∧ q₂.source)
• (Query.ProvSum a a_1 q_2).source = False
• (Query.Having a a_1 a_2 a_3 a_4 a_5 a_6).source = False

@[reducible]

def Query.sourceDecidable {T : Type} {n : ℕ} : DecidablePred source

Equations

• (Query.Rel n s).sourceDecidable = isTrue True.intro
• (Π a q_2).sourceDecidable = match q_2.sourceDecidable with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (σ a q_2).sourceDecidable = match q_2.sourceDecidable with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (q₁ × q₂).sourceDecidable = match q₁.sourceDecidable, q₂.sourceDecidable with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h₁, x => isFalse ⋯ | x, isFalse h₂ => isFalse ⋯
• (q₁ ⊎ q₂).sourceDecidable = match q₁.sourceDecidable, q₂.sourceDecidable with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h₁, x => isFalse ⋯ | x, isFalse h₂ => isFalse ⋯
• (ε q_2).sourceDecidable = match q_2.sourceDecidable with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (q₁ - q₂).sourceDecidable = match q₁.sourceDecidable, q₂.sourceDecidable with | isTrue h₁, isTrue h₂ => isTrue ⋯ | isFalse h₁, x => isFalse ⋯ | x, isFalse h₂ => isFalse ⋯
• (Query.ProvSum a a_1 q_2).sourceDecidable = isFalse Query.sourceDecidable._proof_16
• (Query.Having a a_1 a_2 a_3 a_4 a_5 a_6).sourceDecidable = isFalse Query.sourceDecidable._proof_16

@[instance_reducible]

instance instDecidablePredQuerySource {T : Type} {n : ℕ} : DecidablePred Query.source

Equations

• instDecidablePredQuerySource = Query.sourceDecidable

@[simp]

theorem Query.sourceProd {T : Type} [ValueType T] {n n₂ : ℕ} {q : Query T n} : q.source → ∀ {n₁ : ℕ} {q₁ : Query T n₁} {q₂ : Query T n₂} {hn : n₁ + n₂ = n}, q = q₁ × q₂ → q₁.source ∧ q₂.source

@[simp]

theorem Query.sourceSum {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.source → ∀ {q₁ q₂ : Query T n}, q = (q₁ ⊎ q₂) → q₁.source ∧ q₂.source

@[simp]

theorem Query.sourceDiff {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.source → ∀ {q₁ q₂ : Query T n}, q = (q₁ - q₂) → q₁.source ∧ q₂.source

@[simp]

theorem Query.sourceProj {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.source → ∀ {m : ℕ} {t : Tuple (Term T m) n} {q' : Query T m}, q = Π t q' → q'.source

@[simp]

theorem Query.sourceSel {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.source → ∀ {φ : Selection T n} {q' : Query T n}, q = σ φ q' → q'.source

@[simp]

theorem Query.sourceDedup {T : Type} [ValueType T] {n : ℕ} {q : Query T n} : q.source → ∀ {q' : Query T n}, q = ε q' → q'.source

def «termΠ_» : Lean.ParserDescr

Equations

• «termΠ_» = Lean.ParserDescr.node `«termΠ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Π ") (Lean.ParserDescr.cat `term 1024))

def termσ_ : Lean.ParserDescr

Equations

• termσ_ = Lean.ParserDescr.node `termσ_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "σ ") (Lean.ParserDescr.cat `term 1024))

def «term_×__2» : Lean.TrailingParserDescr

Equations

• «term_×__2» = Lean.ParserDescr.trailingNode `«term_×__2» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " × ") (Lean.ParserDescr.cat `term 81))

def «term_⊎_» : Lean.TrailingParserDescr

Equations

• «term_⊎_» = Lean.ParserDescr.trailingNode `«term_⊎_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊎ ") (Lean.ParserDescr.cat `term 51))

def termε_ : Lean.ParserDescr

Equations

• termε_ = Lean.ParserDescr.node `termε_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ε ") (Lean.ParserDescr.cat `term 1024))

def «term_-__1» : Lean.TrailingParserDescr

Equations

• «term_-__1» = Lean.ParserDescr.trailingNode `«term_-__1» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `term 51))

def «term_⋈_» : Lean.TrailingParserDescr

Equations

• «term_⋈_» = Lean.ParserDescr.trailingNode `«term_⋈_» 1020 1021 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋈ ") (Lean.ParserDescr.cat `term 1021))

def «term_∪__1» : Lean.TrailingParserDescr

Equations

• «term_∪__1» = Lean.ParserDescr.trailingNode `«term_∪__1» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∪ ") (Lean.ParserDescr.cat `term 51))

def Query.arity {T : Type} {n : ℕ} : Query T n → ℕ

Equations

• x✝.arity = n

def Query.aggdepth2_plus_depth {T : Type} {n : ℕ} (q : Query T n) : ℕ

Equations

• (Query.Rel n s).aggdepth2_plus_depth = 0
• (Π a q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 1
• (σ a q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 1
• (q₁ × q₂).aggdepth2_plus_depth = max q₁.aggdepth2_plus_depth q₂.aggdepth2_plus_depth + 1
• (q₁ ⊎ q₂).aggdepth2_plus_depth = max q₁.aggdepth2_plus_depth q₂.aggdepth2_plus_depth + 1
• (ε q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 1
• (q₁ - q₂).aggdepth2_plus_depth = max q₁.aggdepth2_plus_depth q₂.aggdepth2_plus_depth + 1
• (Query.ProvSum a a_1 q_2).aggdepth2_plus_depth = q_2.aggdepth2_plus_depth + 3
• (Query.Having a a_1 a_2 a_3 a_4 a_5 a_6).aggdepth2_plus_depth = a_6.aggdepth2_plus_depth + 3

def Relation.groupSeq {T : Type} [ValueType T] {m n₁ : ℕ} (is : Tuple (Fin m) n₁) (r : Relation T m) (g : Tuple T n₁) : List (Tuple T m)

The occurrences of the group of key g in relation r: the multiset of matching tuples, as a list sorted by the canonical linear order on tuples. The sort order plays the role of the ordering ≼ along which non-commutative sequence aggregates read the occurrences of a group; for commutative aggregates it is irrelevant.

Equations

• Relation.groupSeq is r g = (Multiset.filter (fun (u : Tuple T m) => ∀ (k' : Fin n₁), u (is k') = g k') r).sort fun (x1 x2 : Tuple T m) => x1 ≤ x2

@[irreducible]

def Query.evaluate {T : Type} [ValueType T] {n : ℕ} (q : Query T n) (d : Database T) : Relation T n

Standard multiset semantics of a query over a plain database.

The Diff case is all-or-nothing difference: every copy of a tuple that occurs at all in r₂ is removed from r₁ (deliberately not Multiset.sub, which would subtract multiplicities as in SQL's EXCEPT ALL). This matches the monus-based annotated semantics of difference (Query.evaluateAnnotated) exactly on 0/1-annotated inputs; on general annotations the two disagree over ℕ (see Nat.counterexample_diff_adequacy and Provenance.QueryAdequacy).

Equations

• One or more equations did not get rendered due to their size.
• (Query.Rel n s).evaluate d = match Database.find n s d with | none => ∅ | some rn => rn
• (Π a q_2).evaluate d = Multiset.map (fun (t : Tuple T n_3) (k : Fin n) => (a k).eval t) (q_2.evaluate d)
• (σ a q_2).evaluate d = Multiset.filter a.eval (q_2.evaluate d)
• (q₁ × q₂).evaluate d = Relation.cast hn (q₁.evaluate d * q₂.evaluate d)
• (q₁ ⊎ q₂).evaluate d = q₁.evaluate d + q₂.evaluate d
• (ε q_2).evaluate d = Multiset.dedup (q_2.evaluate d)
• (q₁ - q₂).evaluate d = Multiset.filter (fun (t : Tuple T n) => t ∉ q₂.evaluate d) (q₁.evaluate d)

Home · Documentation · Publications · Contributors · Source · Cite