⊎ from μ^⊎ in the minimal universe

⊎ is in every basis of the recursion-free algebra (union_mem_of_generatesOn), but with a bag recursion the union is a derived operator. The construction (checked on PostgreSQL 18): for R, S of arity k, two constants p₀ ≠ p₁, a k-tuple c̄, and Z_R, Z_S the two relations with the tag p₀ prepended,

• Q_R := μ^⊎Y.( {(p₀, c̄)}, Π_{p₁, r}(σ_{#0 ≐ #(k+1)}(Y × Z_R)) )
• T := μ^⊎Y.( Q_R, Π_{p₁, s}(σ_{#0 ≐ #(k+1)}(Y × Z_S)) )
• R ⊎ S = Π_{#1..#k}(σ_{#0 ≢ p₀}(T)).

The rounds of Q_R: {(p₀, c̄)}, then {(p₁, r) : r ∈ R} – each row derived from (p₀, c̄) alone, since only a row of phase p₀ passes the selection, so with r's own multiplicity – then ∅, the phase being p₁. The rounds of T: Q_R, then {(p₁, s) : s ∈ S}, again from (p₀, c̄) alone, then ∅. Both settle on every instance, in two rounds; the restriction on recursive terms is met (Y once, on the left of an apply, under a selection on regular columns and a projection; the bases closed, Q_R being a closed query with its own recursion); and the multiplicities of R and S add up through the final projection, as ⊎ wants. What a single recursion cannot do – its body reads one fixed relation every round – the base Q_R does: it supplies the rows of R with their multiplicities and one row of multiplicity 1 for the round that reads S to start from.

AggQueryIn.sumByMu is the construction, evaluatePlain_sumByMu its evaluation, and AggQueryIn.exists_sumFree the pass: every query of the minimal universe is equivalent, wherever it settles, to one with no ⊎, over {∅, Π, σ, apply, γ, μ^⊎} and whatever else it used – the product of each round being written as an apply, since a basis holds one of the two and the apply is the one a recursive term may sit under. The two bound names of each construction have to be fresh – declared by no relation of the schema and occurring nowhere in the query, bound names included – so the pass takes a supply of fresh names, an injective f : ℕ → String, and AggQueryIn.names lists what a name must avoid; exists_freshSupply provides the supply for a finitely-supported schema, String being infinite.

The names of a query, bound names included

def AggQueryIn.names {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Finset String

Every name a query mentions, the names its recursions bind included: what a fresh name has to avoid.

Equations

• (AggQueryIn.Rel x✝ s).names = {s}
• (AggQueryIn.Hole x✝¹ s x✝).names = {s}
• (AggQueryIn.Param pv x✝).names = ∅
• AggQueryIn.Empty.names = ∅
• (AggQueryIn.Proj ps q).names = q.names
• (AggQueryIn.Sel φ q hφ).names = q.names
• (q₁.Prod q₂).names = q₁.names ∪ q₂.names
• (q₁.Apply q₂).names = q₁.names ∪ q₂.names
• (q₁.Sum q₂).names = q₁.names ∪ q₂.names
• q.Dedup.names = q.names
• (q₁.Diff q₂).names = q₁.names ∪ q₂.names
• (AggQueryIn.Explode k a q).names = q.names
• (AggQueryIn.Retag h q).names = q.names
• (AggQueryIn.Mu s q₀ q₁).names = insert s (q₀.names ∪ q₁.names)
• (AggQueryIn.MuSet s q₀ q₁).names = insert s (q₀.names ∪ q₁.names)
• (AggQueryIn.Gamma is ts fs q keep ord).names = q.names
• (AggQueryIn.GammaScalar ts fs q ord).names = q.names
• (AggQueryIn.GammaNest is his p f q).names = q.names
• (AggQueryIn.ProvSum is his t q).names = q.names
• (AggQueryIn.GammaTok is his ts fs a q keep).names = q.names
• (AggQueryIn.Win P O o w t f q a dist keep).names = q.names
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).names = q_1.names

What a kind cast keeps

The restriction, the signature and the names, through a substitution

The construction

def AggQueryIn.unitC {T : Type} {c : ℕ} : AggQueryIn T c 0 (ColKind.allReg 0)

The unit relation in a context of c outer columns: one empty row, the scalar aggregation of the empty relation with no aggregate.

Equations

• AggQueryIn.unitC = AggQueryIn.castKind AggQueryIn.unitC._proof_1 (AggQueryIn.GammaScalar (fun (j : Fin 0) => j.elim0) (fun (j : Fin 0) => j.elim0) AggQueryIn.Empty)

def AggQueryIn.tagRow {T : Type} {k : ℕ} (t : T) (r : Tuple T k) : Tuple T (k + 1)

A row with a constant prepended.

Equations

• AggQueryIn.tagRow t r = Fin.cons t r

def AggQueryIn.withTagCols {T : Type} {c k : ℕ} (t : T) : Fin (k + 1) → ProjColIn T c (ColKind.allReg k)

The columns of a row with a constant prepended.

Equations

• AggQueryIn.withTagCols t = Fin.cons (ProjColIn.term (TermGIn.const t)) fun (i : Fin k) => ProjColIn.term (TermGIn.index i ⋯)

theorem AggQueryIn.withTagCols_kind {T : Type} {c k : ℕ} (t : T) : (fun (j : Fin (k + 1)) => (withTagCols t j).kind) = ColKind.allReg (k + 1)

def AggQueryIn.withTag {T : Type} {c k : ℕ} (t : T) (q : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c (k + 1) (ColKind.allReg (k + 1))

A relation with the tag t prepended to every row.

Equations

• AggQueryIn.withTag t q = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (AggQueryIn.withTagCols t) q)

def AggQueryIn.driver {T : Type} [ValueType T] {c k : ℕ} (p₀ : T) : AggQueryIn T c (k + 1) (ColKind.allReg (k + 1))

The driver row (p₀, 0̄), one row of multiplicity one.

Equations

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

theorem AggQueryIn.prodKind_left {k : ℕ} (j : Fin (k + 1)) : Fin.append (ColKind.allReg (k + 1)) (ColKind.allReg (k + 1)) (Fin.castAdd (k + 1) j) = ColKind.reg

The product's first column is regular.

theorem AggQueryIn.prodKind_right {k : ℕ} (j : Fin (k + 1)) : Fin.append (ColKind.allReg (k + 1)) (ColKind.allReg (k + 1)) (Fin.natAdd (k + 1) j) = ColKind.reg

def AggQueryIn.roundCols {T : Type} {c k : ℕ} (p₁ : T) : Fin (k + 1) → ProjColIn T c (Fin.append (ColKind.allReg (k + 1)) (ColKind.allReg (k + 1)))

The columns a round's rows are projected to: the tag p₁, then the columns of the right factor past its tag.

Equations

• AggQueryIn.roundCols p₁ = Fin.cons (ProjColIn.term (TermGIn.const p₁)) fun (i : Fin k) => ProjColIn.term (TermGIn.index (Fin.natAdd (k + 1) i.succ) ⋯)

def AggQueryIn.roundProj {T : Type} [ValueType T] {c k : ℕ} (p₁ : T) (γ : Fin c → T) : Tuple T (k + 1 + (k + 1)) → Tuple T (k + 1)

The row a round emits from a joined row, as one function (named so that Multiset.map_map composes it against the opaque Tuple).

Equations

• AggQueryIn.roundProj p₁ γ u j = (AggQueryIn.roundCols p₁ j).evalPlain u γ

theorem AggQueryIn.roundCols_kind {T : Type} {c k : ℕ} (p₁ : T) : (fun (j : Fin (k + 1)) => (roundCols p₁ j).kind) = ColKind.allReg (k + 1)

def AggQueryIn.sameTag {T : Type} {c k : ℕ} : GenPredIn T c (Fin.append (ColKind.allReg (k + 1)) (ColKind.allReg (k + 1)))

The selection keeping the pairs whose two tags agree.

Equations

• AggQueryIn.sameTag = GenPredIn.cmp CompOp.syneq (TermGIn.index (Fin.castAdd (k + 1) 0) ⋯) (TermGIn.index (Fin.natAdd (k + 1) 0) ⋯)

def AggQueryIn.phaseBody {T : Type} {c k : ℕ} (s : String) (p₁ : T) (Z : AggQueryIn T c (k + 1) (ColKind.allReg (k + 1))) : AggQueryIn T c (k + 1) (ColKind.allReg (k + 1)) [(s, k + 1)]

A round of the construction: the rows of the recursive relation of phase p₀ (the tag of Z) each read Z, and the rows read are re-tagged p₁. The product is written as an apply whose right side reads no column of the left – which is what a product is, and keeps the construction over the classes of a basis holding the apply and not ×.

Equations

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

def AggQueryIn.notTag {T : Type} {c k : ℕ} (p₀ : T) : GenPredIn T c (ColKind.allReg (k + 1))

The selection dropping the rows of phase p₀.

Equations

• AggQueryIn.notTag p₀ = (GenPredIn.cmp CompOp.syneq (TermGIn.index 0 ⋯) (TermGIn.const p₀)).not

def AggQueryIn.unwithTagCols {T : Type} {c k : ℕ} : Tuple (ProjColIn T c (ColKind.allReg (k + 1))) k

The columns past the tag.

Equations

• AggQueryIn.unwithTagCols i = ProjColIn.term (TermGIn.index i.succ ⋯)

def AggQueryIn.sumByMu {T : Type} [ValueType T] {c k : ℕ} (s₁ s₂ : String) (q₁ q₂ : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c k (ColKind.allReg k)

⊎ from two bag recursions (see the module heading): s₁ binds the recursion listing q₁'s rows behind the driver, s₂ the one adding q₂'s rows to it. The phases are 0 and ValueType.nonzero.

Equations

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

What the construction computes

theorem AggQueryIn.evaluatePlain_sumByMu {T : Type} [ValueType T] {c k : ℕ} (s₁ s₂ : String) (q₁ q₂ : AggQueryIn T c k (ColKind.allReg k)) (h₁ : noMention s₁ q₁) (h₂₂ : noMention s₂ q₂) (D : Database T) (γ : Fin c → T) : (sumByMu s₁ s₂ q₁ q₂).evaluatePlain D γ = q₁.evaluatePlain D γ + q₂.evaluatePlain D γ

The construction is the union: its value is q₁ ⊎ q₂ on every instance and context, the two bound names being fresh.

What the construction is made of

def AggQueryIn.sumMuOps : Set OpKind

The classes the construction uses: the empty relation and a scalar aggregation (the unit), projections, selections, applies and bag recursions.

Equations

• AggQueryIn.sumMuOps = {OpKind.empty, OpKind.proj, OpKind.sel, OpKind.apply, OpKind.gamma, OpKind.muBag}

The pass: every ⊎ replaced by the construction

A ⊎ inside a recursive body cannot be replaced by the construction as it stands: the restriction on recursive terms, which the syntax carries, lets the recursive relation be read under a projection, a selection, a product, the left side of an apply or a union, and under no recursion. What a body q₁ with a ⊎ on its recursive path is, though, is a sum q₁' + qC of the body with the non-recursive side of every such ⊎ dropped and a closed query qC (exists_sumFree_aux's second half): the operators the recursive relation may sit under all distribute over ⊎. At a bag recursion that settles, qC is empty – its rows would be in every round – so q₁' is the body; at a set recursion, qC moves into the base, which is where the construction then replaces the ⊎.

def AggQueryIn.emptyRel {T : Type} [ValueType T] {c : ℕ} (n : ℕ) : AggQueryIn T c n (ColKind.allReg n)

The empty relation of arity n, all regular.

Equations

• AggQueryIn.emptyRel n = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (fun (x : Fin n) => ProjColIn.term (TermGIn.const 0)) AggQueryIn.Empty)

def AggQueryIn.emptyOf {T : Type} [ValueType T] {c n : ℕ} (κ : Fin n → ColKind) : AggQueryIn T c n κ

An empty relation of any kinds: a selection that keeps nothing, over the one constant row of a parameter leaf. A hole of aggregate kinds needs it, emptyRel having regular columns only.

Equations

• AggQueryIn.emptyOf κ = AggQueryIn.Sel (GenPredIn.cmp CompOp.syneq (TermGIn.const 0) (TermGIn.const ValueType.nonzero)) (AggQueryIn.Param (fun (x : Fin n) => Sum.inl 0) κ) ⋯

The two recursions, given a split body

The fence, and what the pass carries

def AggQueryIn.sumsAllReg {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

Every ⊎ has all-regular operands. A recursion is all-regular (AggQueryIn.Mu is), so this is what the construction needs of a ⊎ it replaces; it is what the re-typing produces, every operator of its output being over all-regular children.

Equations

• (AggQueryIn.Rel x✝ s).sumsAllReg = True
• (AggQueryIn.Hole x✝¹ s x✝).sumsAllReg = True
• (AggQueryIn.Param pv x✝).sumsAllReg = True
• AggQueryIn.Empty.sumsAllReg = True
• (AggQueryIn.Proj ps q).sumsAllReg = q.sumsAllReg
• (AggQueryIn.Sel φ q hφ).sumsAllReg = q.sumsAllReg
• (q₁.Prod q₂).sumsAllReg = (q₁.sumsAllReg ∧ q₂.sumsAllReg)
• (q₁.Apply q₂).sumsAllReg = (q₁.sumsAllReg ∧ q₂.sumsAllReg)
• (q₁.Sum q₂).sumsAllReg = (x✝ = ColKind.allReg x✝¹ ∧ q₁.sumsAllReg ∧ q₂.sumsAllReg)
• q.Dedup.sumsAllReg = q.sumsAllReg
• (q₁.Diff q₂).sumsAllReg = (q₁.sumsAllReg ∧ q₂.sumsAllReg)
• (AggQueryIn.Explode k a q).sumsAllReg = q.sumsAllReg
• (AggQueryIn.Retag h q).sumsAllReg = q.sumsAllReg
• (AggQueryIn.Mu s q₀ q₁).sumsAllReg = (q₀.sumsAllReg ∧ q₁.sumsAllReg)
• (AggQueryIn.MuSet s q₀ q₁).sumsAllReg = (q₀.sumsAllReg ∧ q₁.sumsAllReg)
• (AggQueryIn.Gamma is ts fs q keep ord).sumsAllReg = q.sumsAllReg
• (AggQueryIn.GammaScalar ts fs q ord).sumsAllReg = q.sumsAllReg
• (AggQueryIn.GammaNest is his p f q).sumsAllReg = q.sumsAllReg
• (AggQueryIn.ProvSum is his t q).sumsAllReg = q.sumsAllReg
• (AggQueryIn.GammaTok is his ts fs a q keep).sumsAllReg = q.sumsAllReg
• (AggQueryIn.Win P O o w t f q a dist keep).sumsAllReg = q.sumsAllReg
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).sumsAllReg = q_1.sumsAllReg

structure AggQueryIn.SumFreeOf {T : Type} [ValueType T] (S : Set OpKind) (Θ : Set (SeqAggFunc T)) (f : ℕ → String) {c n : ℕ} {κ : Fin n → ColKind} {l l' : List (String × ℕ)} (q : AggQueryIn T c n κ l) (q' : AggQueryIn T c n κ l') : Prop

What the pass keeps of a query, besides its value: the classes of S (the construction's being among them), the restriction on recursive terms, the signature, derivable windows, well-formedness over a schema declaring none of the fresh names, the names (its own, or fresh ones), and the names it does not mention (fresh ones aside).

• usesOnly : AggQueryIn.usesOnly S q'
• hygienic : q'.hygienic
• inSig : AggQueryIn.inSig Θ q'
• wins : q.WinsDerivable → q'.WinsDerivable
• over (sch : Schema) : (∀ (i : ℕ), sch.decl (f i) = none) → overSchema sch q → overSchema sch q'
• names (x : String) : x ∈ q'.names → x ∈ q.names ∨ ∃ (i : ℕ), x = f i
• nom (s : String) : (∀ (i : ℕ), s ≠ f i) → noMention s q → noMention s q'

theorem AggQueryIn.exists_sumFree_aux {T : Type} [ValueType T] {S : Set OpKind} (hS : sumMuOps ⊆ S) {Θ : Set (SeqAggFunc T)} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : usesOnly (insert OpKind.union S) q → q.hygienic → inSig Θ q → q.sumsAllReg → ∀ (f : ℕ → String), Function.Injective f → (∀ (i : ℕ), f i ∉ q.names) → (l = [] → ∃ (q' : AggQueryIn T c n κ), SumFreeOf S Θ f q q' ∧ ∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → q'.SettlesAt D γ ∧ q.evaluatePlain D γ = q'.evaluatePlain D γ) ∧ ∀ (s : String) (m : ℕ), l = [(s, m)] → noMention s q → ∃ (q' : AggQueryIn T c n κ l) (qC : AggQueryIn T c n κ), noMention s qC ∧ SumFreeOf S Θ f q q' ∧ SumFreeOf S Θ f q qC ∧ ∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → q'.SettlesAt D γ ∧ qC.SettlesAt D γ ∧ q.evaluatePlain D γ = q'.evaluatePlain D γ + qC.evaluatePlain D γ

The pass, both halves at once. For every query of the fragment (the classes of S and ⊎, restricted recursions, the signature Θ, every ⊎ all-regular) and every injective supply of names the query does not use: a query with no ⊎, keeping what SumFreeOf lists and defined and equal wherever the query is; and, for a body reading the name s once, a body still reading it once and a closed query the body is the sum of.

theorem AggQueryIn.exists_sumFree {T : Type} [ValueType T] {S : Set OpKind} (hS : sumMuOps ⊆ S) {Θ : Set (SeqAggFunc T)} {c n : ℕ} {κ : Fin n → ColKind} (q : AggQueryIn T c n κ) (hq : usesOnly (insert OpKind.union S) q) (hr : q.hygienic) (hi : inSig Θ q) (hsa : q.sumsAllReg) (f : ℕ → String) (hf : Function.Injective f) (hfr : ∀ (i : ℕ), f i ∉ q.names) : ∃ (q' : AggQueryIn T c n κ), usesOnly S q' ∧ q'.hygienic ∧ inSig Θ q' ∧ (q.WinsDerivable → q'.WinsDerivable) ∧ (∀ (sch : Schema), (∀ (i : ℕ), sch.decl (f i) = none) → overSchema sch q → overSchema sch q') ∧ ∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → q'.SettlesAt D γ ∧ q.evaluatePlain D γ = q'.evaluatePlain D γ

⊎ is derivable from μ^⊎ in the minimal universe (⊎ is not needed in a basis of the whole algebra once μ^⊎ is available): every query over the classes of S and ⊎ – restricted recursions, the signature Θ, every ⊎ all-regular – is matched, on every instance where it is defined, by one over the classes of S alone, for any S holding the construction's classes (sumMuOps: ∅, Π, σ, apply, γ, μ^⊎). The names the construction binds come from an injective supply the query does not use, which exists_freshSupply provides.

Home · Documentation · Publications · Contributors · Source · Cite