An apply written with products

An apply L ⊳ R reads its right side at each row of its left side. Its right side's table (Sym.tabQ) holds the encodings of the right side's rows under every descriptor; so the apply is the product of its left side with the descriptors, the table and enough copies of a pool of values, where a row's descriptor is its own (Sym.matchSP), the table's row is filed under that descriptor, and the copied values are the ones the table's cells code (Sym.decCell) – projected on the left row and the decoded values (Sym.applyX, Sym.evaluatePlain_applyX). No row of the left side is read twice: the left side appears once, as the last factor, so the construction applies as well inside a recursive term.

def Sym.uIdx (k n₂ : ℕ) (i : Fin k) : Fin (k * (7 + k) + (k + n₂) * (7 + k) + n₂ + k)

The columns of a row of the product: its left row.

Equations

• Sym.uIdx k n₂ i = Fin.natAdd (k * (7 + k) + (k + n₂) * (7 + k) + n₂) i

def Sym.dIdx (k n₂ : ℕ) (i : Fin k) (j : Fin (7 + k)) : Fin (k * (7 + k) + (k + n₂) * (7 + k) + n₂ + k)

The cell i of the row's descriptor.

Equations

• Sym.dIdx k n₂ i j = Fin.castAdd k (Fin.castAdd n₂ (Fin.castAdd ((k + n₂) * (7 + k)) (Sym.ci i j)))

def Sym.tIdx (k n₂ : ℕ) (z : Fin ((k + n₂) * (7 + k))) : Fin (k * (7 + k) + (k + n₂) * (7 + k) + n₂ + k)

A column of the row's table row.

Equations

• Sym.tIdx k n₂ z = Fin.castAdd k (Fin.castAdd n₂ (Fin.natAdd (k * (7 + k)) z))

def Sym.wIdx (k n₂ : ℕ) (j : Fin n₂) : Fin (k * (7 + k) + (k + n₂) * (7 + k) + n₂ + k)

The j-th decoded value.

Equations

• Sym.wIdx k n₂ j = Fin.castAdd k (Fin.natAdd (k * (7 + k) + (k + n₂) * (7 + k)) j)

def Sym.applyPred {T : Type} [ValueType T] {c : ℕ} (k n₂ : ℕ) : SP T c (k * (7 + k) + (k + n₂) * (7 + k) + n₂ + k)

The row's descriptor, the table row filed under it, and the values its cells code.

Equations

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

noncomputable def Sym.valsQ {T : Type} [ValueType T] {c k : ℕ} (f : ℕ → String) (env : SymEnv T k c) (VQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c 1 (ColKind.allReg 1)

The values a decoded value is taken from: a pool, and the cut.

Equations

• Sym.valsQ f env VQ = (Sym.u2 f VQ env.CQ).dedupG

noncomputable def Sym.applyX {T : Type} [ValueType T] {c k n₂ : ℕ} (cnt : SeqAggFunc T) (f : ℕ → String) {l : List (String × ℕ)} {κ₂ : Fin n₂ → ColKind} (L : AggQueryIn T c k (ColKind.allReg k) l) (R : AggQueryIn T (k + c) n₂ κ₂) (VQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (k + n₂) (ColKind.allReg (k + n₂)) l

An apply, with products: the left side L (read once), the right side R's table, and a pool VQ holding the left side's values.

Equations

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

The predicate on a row of the product

@[reducible, inline]

abbrev Sym.prow {T : Type} {k n₂ : ℕ} (d : Tuple T (k * (7 + k))) (t : Tuple T ((k + n₂) * (7 + k))) (w : Tuple T n₂) (u : Tuple T k) : Tuple T (k * (7 + k) + (k + n₂) * (7 + k) + n₂ + k)

The row of the product.

Equations

• Sym.prow d t w u = Fin.append (Fin.append (Fin.append d t) w) u

Rearranging a product

The apply, with products, computes the apply

theorem Sym.evaluatePlain_applyX {T : Type} [ValueType T] {c k n₂ : ℕ} (Θ : Set (SeqAggFunc T)) {cnt : SeqAggFunc T} (hc : cnt.Counts) (f : ℕ → String) {l : List (String × ℕ)} {κ₂ : Fin n₂ → ColKind} (L : AggQueryIn T c k (ColKind.allReg k) l) (R : AggQueryIn T (k + c) n₂ κ₂) (VQ : AggQueryIn T c 1 (ColKind.allReg 1)) (hU : AggQueryIn.usesOnly basisProdOps R) (hsrc : SymSrc Θ R) (hfR : ∀ (i : ℕ), AggQueryIn.noMention (f i) R) (hfV : AggQueryIn.noMention (part f 1 0) VQ) (D' : Database T) (γ : Fin c → T) (hset : ∀ (u : Tuple T k), Multiset.Mem (L.evaluatePlain D' γ) u → R.SettlesAt D' (Fin.append u γ)) (hval : ∀ (u : Tuple T k), Multiset.Mem (L.evaluatePlain D' γ) u → ∀ (i : Fin k), u i ∈ valsU (VQ.evaluatePlain D' γ)) : (applyX cnt f L R VQ).evaluatePlain D' γ = Multiset.bind (L.evaluatePlain D' γ) fun (u : Tuple T k) => Multiset.map (fun (v : Fin n₂ → T) => Fin.append u v) (R.evaluatePlain D' (Fin.append u γ))

The apply, with products, computes the apply, wherever the right side settles at the left side's rows and the pool holds their values.

Home · Documentation · Publications · Contributors · Source · Cite