The symbolic grouping

A grouping over a symbolic relation groups by the descriptor and by the key cells, and counts through the value column of each cell: a cell's value column is null exactly when the value it stands for is (Sym.isNull_termV), and the counting aggregates of the minimal signature read nothing but how many values are not null (SeqAggFunc.ReadsCount). Under the descriptor of a parameter row the groups are the encodings of the groups the query forms at that row, one for one, the encoding being injective on good values; so the grouping of the symbolic relation computes, under each such descriptor, the encodings of the keys and the very counts of the grouping (Sym.gammaRows_slice).

The plain grouping, as a function of its input

noncomputable def Sym.gammaRows {T : Type} [ValueType T] {n₁ n₂ c' m' : ℕ} (is : Tuple (Fin m') n₁) (ts : Tuple (TermIn T c' m') n₂) (fs : Tuple (SeqAggFunc T) n₂) (keep : Fin n₂ → Option (Selection T m')) (ord : GroupOrder T m') (r : Multiset (Tuple T m')) (γ : Fin c' → T) : Multiset (Tuple T (n₁ + n₂))

The rows a grouping emits from its input.

Equations

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

The symbolic grouping's keys and terms

def Sym.gKeyIdx {k m n₁ : ℕ} (is : Tuple (Fin m) n₁) : Tuple (Fin ((k + m) * (7 + k))) (k * (7 + k) + n₁ * (7 + k))

The key columns of the symbolic grouping: the descriptor's, then the key cells'.

Equations

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

def Sym.termV {T : Type} [ValueType T] {k c m : ℕ} : TermIn T (k + c) m → TermIn T c ((k + m) * (7 + k))

A term of a grouping, read on a symbolic row: the value column of the cell it reads.

Equations

• Sym.termV (TermIn.const a) = TermIn.const a
• Sym.termV (TermIn.outer o) = Fin.addCases (fun (i : Fin k) => #(Sym.ci (Fin.castAdd m i) (Sym.iV k))) (fun (j : Fin c) => TermIn.outer j) o
• Sym.termV #i = #(Sym.ci (Fin.natAdd k i) (Sym.iV k))
• Sym.termV x✝ = TermIn.const 0

theorem Sym.isNull_termV {T : Type} [ValueType T] {k c m : ℕ} (C : Finset T) (t : TermIn T (k + c) m) (ht : t.noFun = true) (par : Fin k → T) (v : Tuple T m) (γ : Fin c → T) : ValueType.isNull ((termV t).eval (rowEnc C par v) γ) = ValueType.isNull (t.eval v (Fin.append par γ))

A term read on an encoded row is null exactly when the term is.

noncomputable def Sym.encK {T : Type} [ValueType T] {k n₁ : ℕ} (C : Finset T) (par : Fin k → T) (g : Tuple T n₁) : Tuple T (k * (7 + k) + n₁ * (7 + k))

The encoding of a key.

Equations

• Sym.encK C par g = Fin.append (Sym.descEnc C par) (Sym.ofCells fun (t : Fin n₁) => Sym.enc C k (Sym.vcode C par (g t)))

def Sym.keyDesc {T : Type} {k M : ℕ} (x : Tuple T (k * (7 + k) + M)) : Tuple T (k * (7 + k))

The descriptor of a key.

Equations

• Sym.keyDesc x i = x (Fin.castAdd M i)

theorem Sym.gammaRows_slice {T : Type} [ValueType T] {k c m n₁ n₂ : ℕ} {C : Finset T} (par : Fin k → T) (is : Tuple (Fin m) n₁) (ts : Tuple (TermIn T (k + c) m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (keep : Fin n₂ → Option (Selection T m)) (ord : GroupOrder T m) (hts : ∀ (j : Fin n₂), (ts j).noFun = true) (hfs : ∀ (j : Fin n₂), (fs j).ReadsCount) (hkeep : ∀ (j : Fin n₂) (φ : Selection T m), keep j = some φ → φ.noFun = true ∧ ∀ a ∈ φ.consts, CG C a) (Q : Multiset (Tuple T ((k + m) * (7 + k)))) (R : Multiset (Tuple T m)) (hR : ∀ v ∈ R, ∀ (i : Fin m), GoodVal par (v i)) (hQ : SliceIs C par Q (Multiset.map (fun (v : Tuple T m) => (v, Fin.elim0)) R)) (γ : Fin c → T) : Multiset.filter (fun (x : Tuple T (k * (7 + k) + n₁ * (7 + k) + n₂)) => (keyDesc fun (i : Fin (k * (7 + k) + n₁ * (7 + k))) => x (Fin.castAdd n₂ i)) = descEnc C par) (gammaRows (gKeyIdx is) (fun (j : Fin n₂) => termV (ts j)) fs (fun (j : Fin n₂) => Option.map (fun (φ : Selection T m) => (transSel 0 φ).toSel) (keep j)) GroupOrder.unord Q γ) = Multiset.map (fun (y : Tuple T (n₁ + n₂)) => Fin.append (encK C par fun (t : Fin n₁) => y (Fin.castAdd n₂ t)) fun (j : Fin n₂) => y (Fin.natAdd n₁ j)) (gammaRows is ts fs keep ord R (Fin.append par γ))

The symbolic grouping, under the descriptor of a parameter row, emits the encodings of the keys the grouping forms at that row, each with the counts the grouping computes there.

From the grouping's rows to symbolic rows

def Sym.gOutSA {T : Type} [ValueType T] {k c : ℕ} (n₁ n₂ : ℕ) : Fin ((k + (n₁ + n₂)) * (7 + k) + 0) → SA T c (k * (7 + k) + n₁ * (7 + k) + n₂)

The cells of a grouping's row: the descriptor and key cells as they are, each aggregate column as a concrete cell.

Equations

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

Second-level aggregation

noncomputable def Sym.nestRows {T : Type} [ValueType T] {n₁ c' m' : ℕ} {κ' : Fin m' → ColKind} (is : Tuple (Fin m') n₁) (p : ProjColIn T c' κ') (f : Multiset T → T) (r : Multiset (Tuple T m')) (γ : Fin c' → T) : Multiset (Tuple T (n₁ + 1))

The rows a second-level aggregation emits from its input.

Equations

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

def Sym.projV {T : Type} [ValueType T] {k c m : ℕ} {κ : Fin m → ColKind} (p : ProjColIn T (k + c) κ) : ProjColIn T c (ColKind.allReg ((k + m) * (7 + k) + 0))

The value column of a projection column's cell.

Equations

• Sym.projV p = ProjColIn.term (Sym.CS.sa 0 (Sym.projCS p) (Sym.iV k)).toG

Aggregation without grouping

The scalar aggregation emits one row on every input, the empty one included, so its symbolic counterpart emits one row under every descriptor: it groups by the descriptor the union of the input's rows, tagged ValueType.nonzero, and of one padding row per descriptor, tagged 0, and its aggregates read only the rows tagged ValueType.nonzero through a FILTER clause.

def Sym.sKeyIdx {k m : ℕ} : Tuple (Fin ((k + m) * (7 + k) + 1)) (k * (7 + k))

The descriptor columns of a tagged symbolic row.

Equations

• Sym.sKeyIdx y = Fin.castAdd 1 (Sym.ci (Fin.castAdd m (finProdFinEquiv.symm y).1) (finProdFinEquiv.symm y).2)

def Sym.tagSel {T : Type} [ValueType T] {N : ℕ} : Selection T (N + 1)

The clause keeping the input's rows: the tag is ValueType.nonzero.

Equations

• Sym.tagSel = Selection.BT (BoolTerm.SYNEQ (#(Fin.natAdd N 0)) (TermIn.const ValueType.nonzero))

def Sym.sOutSA {T : Type} [ValueType T] {k c : ℕ} (n₂ : ℕ) : Fin ((k + n₂) * (7 + k) + 0) → SA T c (k * (7 + k) + n₂)

The cells of a scalar aggregation's row: the descriptor's cells, then each aggregate column as a concrete cell.

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite