The symbolic operators: projection, selection, join

A symbolic relation holds, for every descriptor of a parameter row, the encodings of the rows a query computes at the parameter rows of that type – and junk under the descriptors of no parameter row. What each operator below is asked is to map the slice of its input under the descriptor of a parameter row (Sym.slice) to the slice of its output: the encodings of the input's rows to the encodings of the output's. The rows may carry further columns after their cells (P of them), which a recursive term carries through its rounds untouched.

def Sym.descP {T : Type} {k n P : ℕ} (r : Tuple T ((k + n) * (7 + k) + P)) : Tuple T (k * (7 + k))

The descriptor of a symbolic row: its first k cells.

Equations

• Sym.descP r = Sym.ofCells fun (i : Fin k) (j : Fin (7 + k)) => r (Sym.cc P (Fin.castAdd n i) j)

noncomputable def Sym.slice {T : Type} [ValueType T] {k n P : ℕ} (Q : Multiset (Tuple T ((k + n) * (7 + k) + P))) (d : Tuple T (k * (7 + k))) : Multiset (Tuple T ((k + n) * (7 + k) + P))

The slice of a symbolic relation under a descriptor.

Equations

• Sym.slice Q d = Multiset.filter (fun (r : Tuple T ((k + n) * (7 + k) + P)) => Sym.descP r = d) Q

noncomputable def Sym.encAll {T : Type} [ValueType T] {k n : ℕ} (C : Finset T) (par : Fin k → T) {P : ℕ} (R : Multiset (Tuple T n × Tuple T P)) : Multiset (Tuple T ((k + n) * (7 + k) + P))

The encodings of rows carrying further columns.

Equations

• Sym.encAll C par R = Multiset.map (fun (x : Tuple T n × Tuple T P) => Sym.rowEncP C par x.1 x.2) R

def Sym.SliceIs {T : Type} [ValueType T] {k n : ℕ} (C : Finset T) (par : Fin k → T) {P : ℕ} (Q : Multiset (Tuple T ((k + n) * (7 + k) + P))) (R : Multiset (Tuple T n × Tuple T P)) : Prop

What a symbolic relation is asked: under the descriptor of the parameter row par, it holds the encodings of R.

Equations

• Sym.SliceIs C par Q R = (Sym.slice Q (Sym.descEnc C par) = Sym.encAll C par R)

Maps keeping the descriptor

Projection

theorem Sym.sliceIs_symProj {T : Type} [ValueType T] {k c n : ℕ} {C : Finset T} (par : Fin k → T) (P : ℕ) {m : ℕ} (srcs : Fin m → CS T k c n) (γ : Fin c → T) (hamb : ∀ (j : Fin c), CG C (γ j)) (hc : ∀ (j : Fin m) (a : T), srcs j = CS.const a → CG C a) {Q : Multiset (Tuple T ((k + n) * (7 + k) + P))} {R : Multiset (Tuple T n × Tuple T P)} (hQ : SliceIs C par Q R) : SliceIs C par (Multiset.map (fun (r : Tuple T ((k + n) * (7 + k) + P)) (x : Fin ((k + m) * (7 + k) + P)) => (symProjSA P srcs x).eval r γ) Q) (Multiset.map (fun (x : Tuple T n × Tuple T P) => (fun (j : Fin m) => CS.val par γ x.1 (srcs j), x.2)) R)

The symbolic projection's slice: the encodings of the projected rows.

Selection

Join

def Sym.descEqSP {T : Type} {k c n₁ n₂ : ℕ} (P₁ P₂ : ℕ) : SP T c ((k + n₁) * (7 + k) + P₁ + ((k + n₂) * (7 + k) + P₂))

The two descriptors of a pair of symbolic rows agree, the left one carrying P₁ further columns and the right one P₂.

Equations

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

def Sym.joinCellSA {T : Type} {k c n₁ n₂ : ℕ} (P₁ P₂ : ℕ) (y : Fin ((k + (n₁ + n₂)) * (7 + k))) : SA T c ((k + n₁) * (7 + k) + P₁ + ((k + n₂) * (7 + k) + P₂))

The cells of a joined row: the descriptor and the cells of the left row, then the cells of the right row, then the further columns of the left row (L) or of the right row (R).

Equations

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

def Sym.joinLSA {T : Type} {k c n₁ n₂ : ℕ} (P₁ P₂ : ℕ) : Fin ((k + (n₁ + n₂)) * (7 + k) + P₁) → SA T c ((k + n₁) * (7 + k) + P₁ + ((k + n₂) * (7 + k) + P₂))

The join keeping the left row's further columns.

Equations

• Sym.joinLSA P₁ P₂ i = Fin.addCases (Sym.joinCellSA P₁ P₂) (fun (z : Fin P₁) => Sym.SA.col (Fin.castAdd ((k + n₂) * (7 + k) + P₂) (Fin.natAdd ((k + n₁) * (7 + k)) z))) i

def Sym.joinRSA {T : Type} {k c n₁ n₂ : ℕ} (P₁ P₂ : ℕ) : Fin ((k + (n₁ + n₂)) * (7 + k) + P₂) → SA T c ((k + n₁) * (7 + k) + P₁ + ((k + n₂) * (7 + k) + P₂))

The join keeping the right row's further columns.

Equations

• Sym.joinRSA P₁ P₂ i = Fin.addCases (Sym.joinCellSA P₁ P₂) (fun (z : Fin P₂) => Sym.SA.col (Fin.natAdd ((k + n₁) * (7 + k) + P₁) (Fin.natAdd ((k + n₂) * (7 + k)) z))) i

The descriptors, and the leaves

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

The cells of a leaf's row, paired with a descriptor: the descriptor's cells, then the row's values as concrete cells.

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite