The compositional closure of the rewriting rules

ProvSQL rewrites whole queries in which classical blocks, GROUP BY … HAVING blocks and bare GROUP BY blocks occur as subqueries. The relation AggQuery.RewritesTo below closes the three base rewritings – the classical rules (AggQuery.rewritingOf), the HAVING site (AggQuery.havingPredRew, the aggregate-exposing shape ProvSQL actually emits, for an arbitrary Boolean combination of aggregate comparisons) and the bare grouping (AggQuery.gammaRew) – under the operators that may sit above them, and AggQuery.rewritesTo_valid extends the correctness to every query so obtained.

Token-bearing outputs

The base rules do not share an output shape: a classical or HAVING block produces all-regular data columns, whereas a bare grouping produces aggregate-token columns. The relation is therefore indexed by the rewritten query's own kind vector, and correctness is stated at the token level, through GenRow.toCompositeRow. On all-regular outputs this specializes to the all-regular statement, AggQuery.rewritesTo_valid_reg.

The natural rewritten kind vector of a query of kinds κ is ColKind.rewKindsOf κ – the source kinds followed by the provenance column. Casting terms, predicates and projection columns into it is uniform: a column keeps its kind, so no all-regular hypothesis is needed anywhere (TermG.castRew and friends), unlike the composite casts of the classical rewriting. The gate TermG.cmpAgg, whose generic semantics is the junk value 𝟘, casts to that constant.

Scope

Selection, projection and union close over arbitrary kinds – in particular over a bare grouping, which is the SELECT … FROM (GROUP BY …) shape. Deduplication closes over any subquery whose output is all-regular, which is what the kind discipline permits: the rewritten rule AggQuery.dedupRew is ProvSQL's ε (group by the data columns, ⊕-sum the provenance column), proven correct against an arbitrary rewritten subquery rather than only against rewriting's output.

Product closes over arbitrary kinds too. Reassembling a join needs a projection column whose kind is read off the operand's kind vector – ProjCol.copy, which dispatches on that kind – and its faithfulness needs the operands' rows to conform; that comes for free from the subderivations, since their rows are embeddings of rows of the general evaluator, which conforms by AggQuery.evaluate_conform.

Difference closes as well (AggQuery.diffRew). The closure is therefore complete for the operators the kind discipline admits above a grouping: there is no remaining structural gap.

The rewritten kind vector

@[reducible, inline]

abbrev ColKind.rewKindsOf {n : ℕ} (κ : Fin n → ColKind) : Fin (n + 1) → ColKind

The rewritten kind vector of a query of kinds κ: the source kinds, followed by the provenance column.

Equations

• ColKind.rewKindsOf κ = Fin.append κ fun (x : Fin 1) => ColKind.prov

@[simp]

theorem ColKind.rewKindsOf_castAdd {n : ℕ} (κ : Fin n → ColKind) (k : Fin n) : rewKindsOf κ (Fin.castAdd 1 k) = κ k

@[simp]

theorem ColKind.rewKindsOf_last {n : ℕ} (κ : Fin n → ColKind) : rewKindsOf κ (Fin.last n) = prov

theorem ColKind.rewKindsOf_base_of_reg {n : ℕ} {κ : Fin n → ColKind} (hκ : ∀ (k : Fin n), κ k = reg) (k : Fin (n + 1)) : (rewKindsOf κ k).base = reg

On all-regular kinds the uniform rewritten kind vector agrees pointwise with the classical rewriting's ColKind.rewKinds.

Uniform casts into the rewritten world

def TermG.castRew {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} : TermG T κ → TermG (T ⊕ K) (ColKind.rewKindsOf κ)

A term over the source kinds, read on the rewritten schema: every column keeps its kind and its position, so no all-regular hypothesis is needed. The gate, whose generic semantics is the junk value 𝟘, casts to that constant.

Equations

• (TermG.const a).castRew = TermG.const (Sum.inl a)
• (TermG.index k h).castRew = TermG.index (Fin.castAdd 1 k) ⋯
• (TermG.provIndex k h).castRew = TermG.provIndex (Fin.castAdd 1 k) ⋯
• (TermG.cmpAgg k a a_1 a_2).castRew = TermG.const (Sum.inl 0)
• (TermG.chiGate a a_1 a_2).castRew = TermG.const (Sum.inl 0)
• (t₁.add t₂).castRew = t₁.castRew.add t₂.castRew
• (t₁.sub t₂).castRew = t₁.castRew.sub t₂.castRew
• (t₁.mul t₂).castRew = t₁.castRew.mul t₂.castRew

def GenPred.castRew {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → GenPred (T ⊕ K) (ColKind.rewKindsOf κ)

An aggregate-atom-free predicate is unnecessary here: the cast is total, aggregate atoms comparing a token's deterministic reading.

Equations

• (GenPred.cmp op t₁ t₂).castRew = GenPred.cmp op t₁.castRew t₂.castRew
• (GenPred.aggCmp k h op t).castRew = GenPred.aggCmp (Fin.castAdd 1 k) ⋯ op t.castRew
• (φ.and ψ).castRew = φ.castRew.and ψ.castRew
• (φ.or ψ).castRew = φ.castRew.or ψ.castRew
• φ.not.castRew = φ.castRew.not

def ProjCol.castRew {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} : ProjCol T κ → ProjCol (T ⊕ K) (ColKind.rewKindsOf κ)

A projection column, read on the rewritten schema.

Equations

• (ProjCol.term t).castRew = ProjCol.term t.castRew
• (ProjCol.token k h).castRew = ProjCol.token (Fin.castAdd 1 k) ⋯
• (ProjCol.provTerm t).castRew = ProjCol.provTerm t.castRew

@[simp]

theorem ProjCol.castRew_kind {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (p : ProjCol T κ) : p.castRew.kind = p.kind

The casts evaluate faithfully

theorem TermG.castRew_evalRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (t : TermG T κ) (r : GenRow T K n) : t.castRew.evalRew r.toCompositeRow = Sum.inl (t.eval r.1)

theorem GenPred.castRew_holdsRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (r : GenRow T K n) : φ.castRew.holdsRew r.toCompositeRow ↔ φ.holds r.1

theorem ProjCol.castRew_evalRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (p : ProjCol T κ) (r : GenRow T K n) : p.castRew.evalRew r.toCompositeRow = (p.eval r.1).toComposite

theorem AggQuery.map_toCompositeRow_of_reg {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (d : AnnotatedDatabase T K) : Multiset.map GenRow.toCompositeRow (q.evaluate d) = Multiset.map (fun (t : Tuple (T ⊕ K) (n + 1)) (k : Fin (n + 1)) => Sum.inl (t k)) (q.evaluateAnnotated d).toComposite

On an all-regular query the token-aware embedding is the embedding of the classical and HAVING-site correctness statements.

theorem ColKind.rewKindsOf_of_lt {n : ℕ} (κ : Fin n → ColKind) {j : Fin (n + 1)} (h : ↑j < n) : rewKindsOf κ j = κ ⟨↑j, h⟩

A data column of a rewritten kind vector, positionally.

theorem ColKind.rewKindsOf_of_not_lt {n : ℕ} (κ : Fin n → ColKind) {j : Fin (n + 1)} (h : ¬↑j < n) : rewKindsOf κ j = prov

The trailing column of a rewritten kind vector.

Copying a column of unknown kind

def ProjCol.copy {T' : Type} {N : ℕ} {κ' : Fin N → ColKind} (i : Fin N) : ProjCol T' κ'

Copy the i-th column verbatim, whatever its kind: a regular or provenance column is read as a value term, a token column is a verbatim token copy. This is the projection column a join reassembly needs, since the operand's kind vector is not statically known there.

Equations

• ProjCol.copy i = match h : κ' i with | ColKind.reg => ProjCol.term (TermG.index i h) | ColKind.agg => ProjCol.token i h | ColKind.prov => ProjCol.provTerm (TermG.provIndex i h)

@[simp]

theorem ProjCol.copy_kind {T' : Type} {N : ℕ} {κ' : Fin N → ColKind} (i : Fin N) : (copy i).kind = κ' i

@[simp]

theorem GenValue.kindOf_toComposite {T : Type} [ValueType T] {K : Type} (v : GenValue T K) : v.toComposite.kindOf = v.kindOf

The kind of a transported value is the kind of the value.

theorem GenRow.toCompositeRow_conform {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} {κ : Fin n → ColKind} (r : GenRow T K n) (hr : ∀ (k : Fin n), (r.1 k).kindOf = (κ k).base) (j : Fin (n + 1)) : (r.toCompositeRow j).kindOf = (ColKind.rewKindsOf κ j).base

Kind conformance of the token-aware embedding: a row conforming to κ embeds to one conforming to ColKind.rewKindsOf κ.

theorem ProjCol.copy_evalRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {N : ℕ} {κ' : Fin N → ColKind} (i : Fin N) (u : Tuple (GenValue (T ⊕ K) K) N) (hu : (u i).kindOf = (κ' i).base) : (copy i).evalRew u = u i

A copied column evaluates to the column, on a conformant row.

HAVING predicates as gate terms

The HAVING site rewriting of Provenance.AggQueryHavingRewriting takes one aggregate comparison. An arbitrary Boolean combination of atoms is just as expressible: the predicate provenance predsem is ∧ ↦ ⊗, ∨ ↦ ⊕ and ¬ pushed to the atoms by De Morgan duality with operator complementation, and the rewritten world's terms have mul, add and the two gates – provsql_having for an aggregate atom, the indicator gate for a regular one. GenPred.gateTerm is that translation; it is faithful for an arbitrary predicate (GenPred.gateTerm_evalRew), the gates being the primitives the correctness is relative to.

Regular atoms do change the fate of the group guard. An aggregate atom's predicate provenance ranges over non-empty worlds only, so it supersedes the guard; a regular atom's χ does not entail the group's existence (GenPred.entailsExistence), and mixing one in can leave the whole predicate non-entailing – count(*) > 5 ∨ city = 'Paris' fires in worlds where the group is empty. The site rewriting therefore keeps the guard as a factor in that case (GenPred.siteProvTerm), reproducing what the general evaluator does with the pending group factor.

def GenPred.aggOnly {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → Bool

A predicate all of whose atoms are aggregate comparisons.

Equations

• (GenPred.cmp op t₁ t₂).aggOnly = false
• (GenPred.aggCmp k h op t).aggOnly = true
• (φ.and ψ).aggOnly = (φ.aggOnly && ψ.aggOnly)
• (φ.or ψ).aggOnly = (φ.aggOnly && ψ.aggOnly)
• φ.not.aggOnly = φ.aggOnly

theorem GenPred.aggOnly_entailsExistence {T : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) : φ.aggOnly = true → ∀ (neg : Bool), φ.entailsExistence neg = true

An aggregate-only predicate entails its groups' existence, whatever the polarity: every atom does, and both connectives preserve that.

theorem GenPred.hasAggAtom_comparedCols_nonempty {T : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) : φ.hasAggAtom = true → φ.comparedCols.Nonempty

A predicate with an aggregate atom compares at least one token column.

def GenPred.gateTerm {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → Bool → TermG (T ⊕ K) (ColKind.rewKindsOf κ)

The predicate provenance as a rewritten term: the predsem algebra – aggregate atoms to provsql_having gates, regular atoms to indicator gates, ∧ ↦ ⊗, ∨ ↦ ⊕, ¬ pushed down with operator complementation.

Equations

• (GenPred.cmp op t₁ t₂).gateTerm x✝ = TermG.chiGate (if x✝ = true then op.negate else op) t₁.castRew t₂.castRew
• (GenPred.aggCmp k h op t).gateTerm x✝ = TermG.cmpAgg (Fin.castAdd 1 k) ⋯ (if x✝ = true then op.negate else op) t.castRew
• (φ.and ψ).gateTerm x✝ = if x✝ = true then (φ.gateTerm x✝).add (ψ.gateTerm x✝) else (φ.gateTerm x✝).mul (ψ.gateTerm x✝)
• (φ.or ψ).gateTerm x✝ = if x✝ = true then (φ.gateTerm x✝).mul (ψ.gateTerm x✝) else (φ.gateTerm x✝).add (ψ.gateTerm x✝)
• φ.not.gateTerm x✝ = φ.gateTerm !x✝

theorem GenPred.gateTerm_evalRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (neg : Bool) (r : GenRow T K n) : (φ.gateTerm neg).evalRew r.toCompositeRow = Sum.inr (φ.predsem neg r.1)

The gate term computes the predicate provenance, for an arbitrary predicate: relative to the two gate primitives, which is exactly the sense in which ProvSQL's own rewriting is correct.

theorem GenPred.aggOnly_hasAggAtom {T : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) : φ.aggOnly = true → φ.hasAggAtom = true

An aggregate-only predicate has an aggregate atom.

theorem GenPred.comparedCols_agg {T : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) {k : Fin n} : k ∈ φ.comparedCols → κ k = ColKind.agg

Compared columns are token columns – by construction of the aggregate atom.

theorem gammaRow_conform {T K : Type} {n₁ n₂ : ℕ} (g : Tuple T n₁) (h : Fin n₂ → AggValue T K) (k : Fin (n₁ + n₂)) : (Fin.append (fun (i : Fin n₁) => Sum.inl (g i)) (fun (j : Fin n₂) => Sum.inr (h j)) k).kindOf = (ColKind.gammaKinds n₁ n₂ k).base

Kind conformance of a grouping row.

theorem GenRow.toCompositeRow_gammaRow_conform {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n₁ n₂ : ℕ} (g : Tuple T n₁) (h : Fin n₂ → AggValue T K) (a : GenAnn K) (i : Fin (n₁ + n₂ + 1)) : (toCompositeRow (Fin.append (fun (k : Fin n₁) => Sum.inl (g k)) fun (j : Fin n₂) => Sum.inr (h j), a) i).kindOf = (ColKind.gammaRewKinds n₁ n₂ i).base

Kind conformance of the embedding of a grouping row.

theorem gammaRow_agg_col {T : Type} [ValueType T] {K : Type} {m n₁ n₂ : ℕ} (g : Tuple T n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (U : List (AnnotatedTuple T K m)) {k : Fin (n₁ + n₂)} (hk : ColKind.gammaKinds n₁ n₂ k = ColKind.agg) : ∃ (a : AggValue T K), Fin.append (fun (i : Fin n₁) => Sum.inl (g i)) (fun (j : Fin n₂) => Sum.inr (AggValue.ofGroup (fs j) (ts j) U)) k = Sum.inr a ∧ List.map Prod.snd a.occs = List.map Prod.snd U

A token column of a grouping row carries the group's annotation list.

theorem GenAnn.finalize_supersede {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (b : K) (l₀ : List K) (C : Multiset (List K)) (hne : C ≠ 0) (hall : ∀ l' ∈ C, l' = l₀) : { base := b, pending := Multiset.filter (fun (l : List K) => ¬(C ≠ 0 ∧ ∀ l' ∈ C, l' = l)) {l₀} }.finalize = b

Superseding the group guard: when the compared occurrence lists are non-empty and all equal to the single pending group's list, the selection's filter removes that group factor, so the row finalizes to its concrete part.

The general HAVING site

def GenPred.siteProvTerm {T : Type} [ValueType T] {K : Type} {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.gammaKinds n₁ n₂)) : TermG (T ⊕ K) (ColKind.gammaRewKinds n₁ n₂)

The provenance column of a rewritten HAVING site: the predicate's gate term, times the group-existence guard δ(⊕ U) – which the rewritten grouping has left in the provenance column – unless the predicate already entails the group's existence, in which case the gate term supersedes it. This is ProvSQL's having_entails_group_existence test: the supersede of the δ gate is licensed exactly when every world the predicate accepts has the group non-empty.

Equations

• φ.siteProvTerm = if φ.entailsExistence false = true then φ.gateTerm false else (φ.gateTerm false).mul (TermG.provIndex (Fin.last (n₁ + n₂)) ⋯)

def AggQuery.havingPredCols {T : Type} [ValueType T] {K : Type} {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.gammaKinds n₁ n₂)) : Tuple (ProjCol (T ⊕ K) (ColKind.gammaRewKinds n₁ n₂)) (n₁ + n₂ + 1)

The output columns of a general HAVING site: the group keys and the aggregate tokens copied verbatim, and the predicate's provenance term in the provenance column.

Equations

• AggQuery.havingPredCols φ j = if hj : ↑j < n₁ + n₂ then ProjCol.copy (Fin.castAdd 1 ⟨↑j, hj⟩) else ProjCol.provTerm φ.siteProvTerm

theorem AggQuery.havingPredCols_kind {T : Type} [ValueType T] {K : Type} {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.gammaKinds n₁ n₂)) (j : Fin (n₁ + n₂ + 1)) : (havingPredCols φ j).kind = ColKind.gammaRewKinds n₁ n₂ j

The site's output columns have exactly the rewritten Gamma kinds.

def AggQuery.havingPredRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (φ : GenPred T (ColKind.gammaKinds n₁ n₂)) (qg : AggQuery T m (ColKind.allReg m)) (hq : qg.classical) : AggQuery (T ⊕ K) (n₁ + n₂ + 1) (ColKind.gammaRewKinds n₁ n₂)

The rewritten HAVING site, for an arbitrary predicate: the token-building grouping of AggQuery.gammaRew, with a projection keeping the group keys and the aggregate tokens and replacing the group-existence guard by the predicate's provenance term – the gate term alone when the predicate entails the group's existence, the gate term times the guard otherwise.

Equations

• AggQuery.havingPredRew is ts fs φ qg hq = AggQuery.Retag ⋯ (AggQuery.Proj (AggQuery.havingPredCols φ) (AggQuery.gammaRew is ts fs qg hq))

theorem AggQuery.havingPredRew_valid {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (φ : GenPred T (ColKind.gammaKinds n₁ n₂)) (hφ : φ.hasAggAtom = true) (qg : AggQuery T m (ColKind.allReg m)) (hq : qg.classical) (d : AnnotatedDatabase T K) : Multiset.map GenRow.toCompositeRow ((Sel φ (Gamma is ts fs qg)).evaluate d) = (havingPredRew is ts fs φ qg hq).evaluateRew d.toComposite

Correctness of the general HAVING site rewriting, relative to the gate primitives, for an arbitrary predicate with an aggregate atom – regular atoms mixed in included. The gate term computes the predicate provenance; the group guard is superseded exactly when the predicate entails the group's existence, and kept as a factor otherwise, matching the general evaluator's treatment of the pending group factor.

Duplicate elimination in the rewritten world

theorem fold_addFn_inr {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {α : Type} (f : α → K) (M : Multiset α) : Multiset.fold addFn 0 (Multiset.map (fun (x : α) => Sum.inr (f x)) M) = Sum.inr (Multiset.map f M).sum

Folding embedded annotations with the value-type addition is the annotation sum.

theorem GenRow.toCompositeRow_ofAnnotated {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (p : AnnotatedTuple T K n) : (ofAnnotated p).toCompositeRow = Fin.append (fun (k : Fin n) => Sum.inl (Sum.inl (p.1 k))) fun (x : Fin 1) => Sum.inl (Sum.inr p.2)

The embedding of a row rebuilt from an annotated tuple.

theorem GenRow.plainTuple_toCompositeRow {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) (k : Fin n) : plainTuple r.toCompositeRow (Fin.castAdd 1 k) = Sum.inl (plainTuple r.1 k)

The data reading of an embedded row is the embedded data reading.

theorem TermG.evalRew_provLast_toCompositeRow {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (r : GenRow T K n) : (provIndex (Fin.last n) ⋯).evalRew r.toCompositeRow = Sum.inr r.2.finalize

The provenance column of an embedded row is its finalized annotation.

def AggQuery.dedupRew {T K : Type} {n : ℕ} (q' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))

The rewritten duplicate elimination: ProvSQL's ε rule – group by the data columns and ⊕-sum the provenance column – applied to an arbitrary rewritten subquery, as AggQuery.rewriting does for the classical fragment.

Equations

• q'.dedupRew = AggQuery.Retag ⋯ (AggQuery.ProvSum (fun (k : Fin n) => Fin.castAdd 1 k) ⋯ (TermG.provIndex (Fin.last n) ⋯) q')

theorem AggQuery.dedupRew_valid {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {q : AggQuery T n (ColKind.allReg n)} {q' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))} (d : AnnotatedDatabase T K) (ih : Multiset.map GenRow.toCompositeRow (q.evaluate d) = q'.evaluateRew d.toComposite) : Multiset.map GenRow.toCompositeRow (q.Dedup.evaluate d) = q'.dedupRew.evaluateRew d.toComposite

Correctness of the rewritten duplicate elimination, for an arbitrary rewritten subquery.

Products of token-bearing blocks

def AggQuery.prodRewCols {T K : Type} {n₁ n₂ : ℕ} (κ₁ : Fin n₁ → ColKind) (κ₂ : Fin n₂ → ColKind) : Tuple (ProjCol (T ⊕ K) (Fin.append (ColKind.rewKindsOf κ₁) (ColKind.rewKindsOf κ₂))) (n₁ + n₂ + 1)

The reassembly columns of a rewritten product: the two operands' data columns copied verbatim (whatever their kinds), and the product of the two provenance columns.

Equations

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

theorem AggQuery.prodRewCols_kind {T K : Type} {n₁ n₂ : ℕ} (κ₁ : Fin n₁ → ColKind) (κ₂ : Fin n₂ → ColKind) (j : Fin (n₁ + n₂ + 1)) : (prodRewCols κ₁ κ₂ j).kind = ColKind.rewKindsOf (Fin.append κ₁ κ₂) j

The reassembly columns have the rewritten kinds of the product.

def AggQuery.prodRew {T K : Type} {n₁ n₂ : ℕ} {κ₁ : Fin n₁ → ColKind} {κ₂ : Fin n₂ → ColKind} (q₁' : AggQuery (T ⊕ K) (n₁ + 1) (ColKind.rewKindsOf κ₁)) (q₂' : AggQuery (T ⊕ K) (n₂ + 1) (ColKind.rewKindsOf κ₂)) : AggQuery (T ⊕ K) (n₁ + n₂ + 1) (ColKind.rewKindsOf (Fin.append κ₁ κ₂))

The rewritten product, over operands of arbitrary kinds: the two rewritten blocks joined, the data columns reassembled by kind-preserving copies, and the provenance columns multiplied.

Equations

• q₁'.prodRew q₂' = AggQuery.Retag ⋯ (AggQuery.Proj (AggQuery.prodRewCols κ₁ κ₂) (q₁'.Prod q₂'))

theorem AggQuery.prodRew_valid {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n₁ n₂ : ℕ} {κ₁ : Fin n₁ → ColKind} {κ₂ : Fin n₂ → ColKind} {q₁ : AggQuery T n₁ κ₁} {q₂ : AggQuery T n₂ κ₂} {q₁' : AggQuery (T ⊕ K) (n₁ + 1) (ColKind.rewKindsOf κ₁)} {q₂' : AggQuery (T ⊕ K) (n₂ + 1) (ColKind.rewKindsOf κ₂)} (d : AnnotatedDatabase T K) (ih₁ : Multiset.map GenRow.toCompositeRow (q₁.evaluate d) = q₁'.evaluateRew d.toComposite) (ih₂ : Multiset.map GenRow.toCompositeRow (q₂.evaluate d) = q₂'.evaluateRew d.toComposite) : Multiset.map GenRow.toCompositeRow ((q₁.Prod q₂).evaluate d) = (q₁'.prodRew q₂').evaluateRew d.toComposite

Correctness of the rewritten product, for arbitrary operand kinds: conformance of the operands' rows makes the kind-dispatched column copies faithful.

Difference in the rewritten world

The general evaluator keeps every row of the left operand, rewriting its annotation to α ⊖ Σβ – the monus against the ⊕-sum of the matching rows on the right. ProvSQL's rewriting encodes that missing left outer join as a union of two branches: rows whose data part is absent from the right operand keep their annotation, rows whose data part is present are joined against the per-key sums and subtract them. The rewritten world's TermG.sub supplies the monus directly, so both branches are plain projections of joins, and the two semijoin identities of Provenance.QueryRewriting reduce them to filters of the left operand.

theorem inl_append {T K : Type} {n m : ℕ} (t : Tuple (T ⊕ K) n) (s : Tuple (T ⊕ K) m) : (Fin.append (fun (k : Fin n) => Sum.inl (t k)) fun (k : Fin m) => Sum.inl (s k)) = fun (k : Fin (n + m)) => Sum.inl (Fin.append t s k)

The inl embedding commutes with appending rows.

theorem GenRow.toCompositeRow_ofAnnotated_inl {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] {n : ℕ} (p : AnnotatedTuple T K n) : (ofAnnotated p).toCompositeRow = fun (k : Fin (n + Nat.succ 0)) => Sum.inl (p.toComposite k)

The embedding of a rebuilt annotated row is the inl-image of its composite encoding.

def AggQuery.diffKeyProj {T K : Type} {n : ℕ} (q : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) : AggQuery (T ⊕ K) n (ColKind.allReg n)

The data columns of a rewritten block, as an all-regular query: the provenance column dropped.

Equations

• q.diffKeyProj = AggQuery.Retag ⋯ (AggQuery.Proj (fun (j : Fin n) => ProjCol.term (TermG.index (Fin.castAdd 1 j) ⋯)) q)

def AggQuery.diffColsU {T K : Type} {n : ℕ} : Tuple (ProjCol (T ⊕ K) (Fin.append (ColKind.rewKindsOf (ColKind.allReg n)) (ColKind.allReg n))) (n + 1)

The output columns of the unmatched branch: the left block copied verbatim, provenance column included.

Equations

• AggQuery.diffColsU j = if hj : ↑j < n then ProjCol.term (TermG.index (Fin.castAdd n (Fin.castAdd 1 ⟨↑j, hj⟩)) ⋯) else ProjCol.provTerm (TermG.provIndex (Fin.castAdd n (Fin.last n)) ⋯)

def AggQuery.diffColsM {T K : Type} {n : ℕ} : Tuple (ProjCol (T ⊕ K) (Fin.append (ColKind.rewKindsOf (ColKind.allReg n)) (ColKind.rewKindsOf (ColKind.allReg n)))) (n + 1)

The output columns of the matched branch: the left block's data columns, and the monus of the two provenance columns.

Equations

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

theorem AggQuery.diffColsU_kind {T K : Type} {n : ℕ} (j : Fin (n + 1)) : (diffColsU j).kind = ColKind.rewKindsOf (ColKind.allReg n) j

theorem AggQuery.diffColsM_kind {T K : Type} {n : ℕ} (j : Fin (n + 1)) : (diffColsM j).kind = ColKind.rewKindsOf (ColKind.allReg n) j

def AggQuery.diffBranchU {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} (q₁' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) (qs : AggQuery (T ⊕ K) n (ColKind.allReg n)) : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))

The unmatched branch: left rows whose data part is among the surviving keys, keeping their annotation.

Equations

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

def AggQuery.diffBranchM {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} (q₁' qs : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))

The matched branch: left rows joined against the per-key ⊕-sums, subtracting them.

Equations

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

def AggQuery.diffRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} (q₁' q₂' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))

The rewritten difference.

Equations

• q₁'.diffRew q₂' = (q₁'.diffBranchU (q₁'.diffKeyProj.Diff q₂'.diffKeyProj).Dedup).Sum (q₁'.diffBranchM q₂'.dedupRew)

theorem inlTuple_injective {T K : Type} {n : ℕ} : Function.Injective fun (u : Tuple T n) (k : Fin n) => Sum.inl (u k)

The data embedding of tuples is injective.

theorem AggQuery.diffKeyProj_evaluateRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (q' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) (D : Database (T ⊕ K)) (A : AnnotatedRelation T K n) (h : q'.evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin (n + 1)) => Sum.inl (p.toComposite k)) A) : q'.diffKeyProj.evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin n) => Sum.inl (Sum.inl (p.1 k))) A

The data projection of a rewritten block.

theorem AggQuery.diffSurvivors_evaluateRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (q₁' q₂' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) (D : Database (T ⊕ K)) (A₁ A₂ : AnnotatedRelation T K n) (h₁ : q₁'.evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin (n + 1)) => Sum.inl (p.toComposite k)) A₁) (h₂ : q₂'.evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin (n + 1)) => Sum.inl (p.toComposite k)) A₂) : (q₁'.diffKeyProj.Diff q₂'.diffKeyProj).Dedup.evaluateRew D = Multiset.map (fun (u : Tuple T n) (k : Fin n) => Sum.inl (Sum.inl (u k))) (Multiset.filter (fun (u : Tuple T n) => u ∉ Multiset.map Prod.fst A₂) (Multiset.map Prod.fst A₁)).dedup

The surviving keys: the deduplicated data tuples of the left operand absent from the right one.

theorem AggQuery.diffBranchU_evaluateRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (q₁' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) (qs : AggQuery (T ⊕ K) n (ColKind.allReg n)) (D : Database (T ⊕ K)) (A₁ : AnnotatedRelation T K n) (S : Multiset (Tuple T n)) (hS : S.Nodup) (h₁ : q₁'.evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin (n + 1)) => Sum.inl (p.toComposite k)) A₁) (hs : qs.evaluateRew D = Multiset.map (fun (u : Tuple T n) (k : Fin n) => Sum.inl (Sum.inl (u k))) S) : (q₁'.diffBranchU qs).evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin (n + 1)) => Sum.inl (p.toComposite k)) (Multiset.filter (fun (p : AnnotatedTuple T K n) => p.1 ∈ S) A₁)

The unmatched branch: by the semijoin identity, the left rows whose data part is a surviving key, with their annotation.

theorem AggQuery.diffBranchM_evaluateRew {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} (q₁' qs : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))) (D : Database (T ⊕ K)) (A₁ : AnnotatedRelation T K n) (S : Multiset (Tuple T n)) (hS : S.Nodup) (V : Tuple T n → K) (h₁ : q₁'.evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin (n + 1)) => Sum.inl (p.toComposite k)) A₁) (hs : qs.evaluateRew D = Multiset.map (fun (u : Tuple T n) (k : Fin (n + 1)) => Sum.inl (AnnotatedTuple.toComposite (u, V u) k)) S) : (q₁'.diffBranchM qs).evaluateRew D = Multiset.map (fun (p : AnnotatedTuple T K n) (k : Fin (n + 1)) => Sum.inl (AnnotatedTuple.toComposite (p.1, p.2 - V p.1) k)) (Multiset.filter (fun (p : AnnotatedTuple T K n) => p.1 ∈ S) A₁)

The matched branch: by the keyed-projection semijoin, the left rows whose data part carries a per-key sum, with that sum subtracted.

theorem AggQuery.diffRew_valid {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {q₁ q₂ : AggQuery T n (ColKind.allReg n)} {q₁' q₂' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))} (d : AnnotatedDatabase T K) (ih₁ : Multiset.map GenRow.toCompositeRow (q₁.evaluate d) = q₁'.evaluateRew d.toComposite) (ih₂ : Multiset.map GenRow.toCompositeRow (q₂.evaluate d) = q₂'.evaluateRew d.toComposite) : Multiset.map GenRow.toCompositeRow ((q₁.Diff q₂).evaluate d) = (q₁'.diffRew q₂').evaluateRew d.toComposite

Correctness of the rewritten difference, for arbitrary rewritten operands: the two branches partition the left operand by whether its data part occurs on the right, and on the unmatched part the subtracted sum is 𝟘.

The classical rewriting at the uniform kind vector

def AggQuery.rewritingOf {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf κ)

The classical rewriting, retagged to ColKind.rewKindsOf κ. AggQuery.rewriting targets ColKind.rewKinds n – the per-index if k < n form – which is only pointwise equal to the uniform Fin.append κ prov the congruences below consume. Retagging once here (semantically the identity) lets a congruence sit directly above the classical base rule instead of threading an explicit retag step.

Equations

• q.rewritingOf hq = AggQuery.Retag ⋯ (q.rewriting hq)

The closure

inductive AggQuery.RewritesTo {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} {κ' : Fin (n + 1) → ColKind} : AggQuery T n κ → AggQuery (T ⊕ K) (n + 1) κ' → Prop

The compositional closure of the rewriting rules: the three base rewritings – classical blocks, fused HAVING sites and bare groupings – composed under union, selection, projection, deduplication, product and difference, with the kind-retagging of AggQuery.Retag available to adapt a subderivation's output kinds. The HAVING-site rule havingPred keeps the group keys and the aggregate tokens as output columns and admits any predicate with an aggregate atom.

• classical {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.classical) : q.RewritesTo (q.rewritingOf hq)
• gamma {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (qg : AggQuery T m (ColKind.allReg m)) (hq : qg.classical) : (Gamma is ts fs qg).RewritesTo (gammaRew is ts fs qg hq)
• havingPred {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (φ : GenPred T (ColKind.gammaKinds n₁ n₂)) (hφ : φ.hasAggAtom = true) (qg : AggQuery T m (ColKind.allReg m)) (hq : qg.classical) : (Sel φ (Gamma is ts fs qg)).RewritesTo (havingPredRew is ts fs φ qg hq)
• retag {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} {κ' κ'' : Fin (n + 1) → ColKind} {q : AggQuery T n κ} {q' : AggQuery (T ⊕ K) (n + 1) κ'} (h : ∀ (k : Fin (n + 1)), (κ' k).base = (κ'' k).base) : q.RewritesTo q' → q.RewritesTo (Retag h q')
• sum {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} {κ' : Fin (n + 1) → ColKind} {q₁ q₂ : AggQuery T n κ} {q₁' q₂' : AggQuery (T ⊕ K) (n + 1) κ'} : q₁.RewritesTo q₁' → q₂.RewritesTo q₂' → (q₁.Sum q₂).RewritesTo (q₁'.Sum q₂')
• dedup {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {q : AggQuery T n (ColKind.allReg n)} {q' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))} : q.RewritesTo q' → q.Dedup.RewritesTo q'.dedupRew
• diff {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {q₁ q₂ : AggQuery T n (ColKind.allReg n)} {q₁' q₂' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf (ColKind.allReg n))} : q₁.RewritesTo q₁' → q₂.RewritesTo q₂' → (q₁.Diff q₂).RewritesTo (q₁'.diffRew q₂')
• sel {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} {q : AggQuery T n κ} {q' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf κ)} (φ : GenPred T κ) (hφ : φ.hasAggAtom = false) : q.RewritesTo q' → (Sel φ q).RewritesTo (Sel φ.castRew q')
• proj {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n m : ℕ} {κ : Fin n → ColKind} {q : AggQuery T n κ} {q' : AggQuery (T ⊕ K) (n + 1) (ColKind.rewKindsOf κ)} (ps : Tuple (ProjCol T κ) m) : q.RewritesTo q' → (Proj ps q).RewritesTo (Retag ⋯ (Proj (fun (j : Fin (m + 1)) => if hj : ↑j < m then (ps ⟨↑j, hj⟩).castRew else ProjCol.provTerm (TermG.provIndex (Fin.last n) ⋯)) q'))
• prod {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [HasAltLinearOrder K] {n₁ n₂ : ℕ} {κ₁ : Fin n₁ → ColKind} {κ₂ : Fin n₂ → ColKind} {q₁ : AggQuery T n₁ κ₁} {q₂ : AggQuery T n₂ κ₂} {q₁' : AggQuery (T ⊕ K) (n₁ + 1) (ColKind.rewKindsOf κ₁)} {q₂' : AggQuery (T ⊕ K) (n₂ + 1) (ColKind.rewKindsOf κ₂)} : q₁.RewritesTo q₁' → q₂.RewritesTo q₂' → (q₁.Prod q₂).RewritesTo (q₁'.prodRew q₂')

theorem AggQuery.rewritesTo_valid {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} {κ' : Fin (n + 1) → ColKind} {q : AggQuery T n κ} {q' : AggQuery (T ⊕ K) (n + 1) κ'} (h : q.RewritesTo q') (d : AnnotatedDatabase T K) : Multiset.map GenRow.toCompositeRow (q.evaluate d) = q'.evaluateRew d.toComposite

Whole-query correctness of the compositional rewriting: along the closure, the general evaluator's rows, embedded token-aware into the composite domain, are exactly the rewritten world's evaluation.

theorem AggQuery.rewritesTo_valid_reg {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} {κ' : Fin (n + 1) → ColKind} {q : AggQuery T n κ} {q' : AggQuery (T ⊕ K) (n + 1) κ'} (h : q.RewritesTo q') (hκ : ∀ (k : Fin n), κ k = ColKind.reg) (d : AnnotatedDatabase T K) : Multiset.map (fun (t : Tuple (T ⊕ K) (n + 1)) (k : Fin (n + 1)) => Sum.inl (t k)) (q.evaluateAnnotated d).toComposite = q'.evaluateRew d.toComposite

On an all-regular source the correctness specializes to the shape of the classical and HAVING-site statements: the annotated semantics, folded into composite tuples and embedded by inl.

Home · Documentation · Publications · Contributors · Source · Cite