Symbolic rows

A symbolic relation for a query whose context starts with k parameter components holds rows of k + n cells, each cell 7 + k columns (Provenance.SymCells): the first k cells are the codes of the parameter row – its descriptor – and the other n the codes of an output row. A value of an output row is coded canonically (Sym.vcode): the code of the parameter component it equals where that component is fresh, itself elsewhere. Sym.rowEnc is the symbolic row of a parameter row and an output row, and what a symbolic evaluation is asked is that the rows it holds under the descriptor of a parameter row be the encodings of the output rows at that parameter row.

Cells of a row

def Sym.ci {k N : ℕ} (i : Fin N) (j : Fin (7 + k)) : Fin (N * (7 + k))

The column j of cell i.

Equations

• Sym.ci i j = finProdFinEquiv (i, j)

def Sym.cellOf {T : Type} {k N : ℕ} (r : Tuple T (N * (7 + k))) (i : Fin N) : Tuple T (7 + k)

The cell i of a row.

Equations

• Sym.cellOf r i j = r (Sym.ci i j)

def Sym.ofCells {T : Type} {k N : ℕ} (cs : Fin N → Tuple T (7 + k)) : Tuple T (N * (7 + k))

A row from its cells.

Equations

• Sym.ofCells cs x = cs (finProdFinEquiv.symm x).1 (finProdFinEquiv.symm x).2

The canonical code of a value

noncomputable def Sym.vcode {T : Type} [ValueType T] (C : Finset T) {k : ℕ} (par : Fin k → T) (b : T) : Code T

The code of a value of an output row: the code of the parameter component it is, where that component is fresh; the value itself elsewhere.

Equations

• Sym.vcode C par b = if h : ∃ (i : Fin k), Sym.IsFresh C (par i) ∧ par i = b then Sym.code C par h.choose else Sym.Code.conc b

def Sym.GoodVal {T : Type} [ValueType T] {C : Finset T} {k : ℕ} (par : Fin k → T) (b : T) : Prop

A value the symbolic evaluation can code: a component of the parameter row, a value of the cut, or the null.

Equations

• Sym.GoodVal par b = ((∃ (i : Fin k), par i = b) ∨ b ∈ C ∨ ValueType.isNull b = true)

Encodings are injective

def Sym.RankOK {T : Type} (k : ℕ) : Code T → Prop

The fresh codes a row holds have their ranks below k.

Equations

• Sym.RankOK k (Sym.Code.conc a) = True
• Sym.RankOK k (Sym.Code.fresh l r) = (r < k)

The symbolic row of a parameter row and an output row

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

The descriptor of a parameter row: the codes of its components.

Equations

• Sym.descEnc C par = Sym.ofCells fun (i : Fin k) => Sym.enc C k (Sym.code C par i)

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

The symbolic row of a parameter row and an output row.

Equations

• Sym.rowEnc C par v = Sym.ofCells (Fin.append (fun (i : Fin k) => Sym.enc C k (Sym.code C par i)) fun (j : Fin n) => Sym.enc C k (Sym.vcode C par (v j)))

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

The descriptor part of a symbolic row.

Equations

• Sym.descPart r = Sym.ofCells fun (i : Fin k) => Sym.cellOf r (Fin.castAdd n i)

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

The output part of a symbolic row.

Equations

• Sym.outPart r = Sym.ofCells fun (j : Fin n) => Sym.cellOf r (Fin.natAdd k j)

Home · Documentation · Publications · Contributors · Source · Cite