Terms and predicates over symbolic rows

A term of the minimal signature is a column, a parameter, a value of the ambient context or a constant (Sym.CS, read off a term by Sym.termCS). On a symbolic row each is a cell: a column's cell, the parameter's cell of the descriptor, or the constant cell of a value of the context or of the query (Sym.CS.sa). Where the values involved are good – components of the parameter row, values of the cut, or the null – the cell read on the encoding of a row is the encoding of the term's value (Sym.CS.eval_sa), and a predicate translated cell by cell (Sym.transPred) has the three-valued truth of the original on the decoded row (Sym.eval3_transPred).

inductive Sym.CS (T : Type) (k c n : ℕ) : Type

Where a term's value comes from: a column of the row, a parameter component, a value of the ambient context, or a constant.

• col {T : Type} {k c n : ℕ} (i : Fin n) : CS T k c n
• par {T : Type} {k c n : ℕ} (i : Fin k) : CS T k c n
• amb {T : Type} {k c n : ℕ} (j : Fin c) : CS T k c n
• const {T : Type} {k c n : ℕ} (a : T) : CS T k c n

def Sym.CS.val {T : Type} {k c n : ℕ} (par : Fin k → T) (γ : Fin c → T) (v : Tuple T n) : CS T k c n → T

What it reads under a parameter row, a context and an output row.

Equations

• Sym.CS.val par γ v (Sym.CS.col i) = v i
• Sym.CS.val par γ v (Sym.CS.par i) = par i
• Sym.CS.val par γ v (Sym.CS.amb j) = γ j
• Sym.CS.val par γ v (Sym.CS.const a) = a

def Sym.concCols {T : Type} [ValueType T] {k c m : ℕ} (vcol : SA T c m) : Fin (7 + k) → SA T c m

The columns of a concrete cell, with its value column given.

Equations

• Sym.concCols vcol = Fin.append ![Sym.SA.const 0, vcol, Sym.SA.const 0, Sym.SA.const 0, Sym.SA.const 0, Sym.SA.const Sym.sLo, Sym.SA.const Sym.sHi] fun (x : Fin k) => Sym.SA.const 0

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

The column of cell i, column j, of a symbolic row with P more columns after its cells.

Equations

• Sym.cc P i j = Fin.castAdd P (Sym.ci i j)

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

The cell a source reads, on a symbolic row of k + n cells and P more columns.

Equations

• Sym.CS.sa P (Sym.CS.col i) = fun (j : Fin (7 + k)) => Sym.SA.col (Sym.cc P (Fin.natAdd k i) j)
• Sym.CS.sa P (Sym.CS.par i) = fun (j : Fin (7 + k)) => Sym.SA.col (Sym.cc P (Fin.castAdd n i) j)
• Sym.CS.sa P (Sym.CS.amb j) = Sym.concCols (Sym.SA.amb j)
• Sym.CS.sa P (Sym.CS.const a) = Sym.concCols (Sym.SA.const a)

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

The symbolic row of a parameter row and an output row, with P more columns.

Equations

• Sym.rowEncP C par v e = Fin.append (Sym.rowEnc C par v) e

theorem Sym.CS.eval_sa {T : Type} [ValueType T] {k c n : ℕ} {C : Finset T} (P : ℕ) (s : CS T k c n) (par : Fin k → T) (γ : Fin c → T) (v : Tuple T n) (e : Tuple T P) (hs : ∀ (a : Fin c), s = amb a → γ a ∈ C ∨ ValueType.isNull (γ a) = true) (hc : ∀ (a : T), s = const a → a ∈ C ∨ ValueType.isNull a = true) (i : Fin (7 + k)) : (sa P s i).eval (rowEncP C par v e) γ = enc C k (vcode C par (val par γ v s)) i

A source's cell, read on an encoded row, encodes the source's value, where the value is good.

Terms

def Sym.CG {T : Type} [ValueType T] (C : Finset T) (a : T) : Prop

A value of the cut, or the null.

Equations

• Sym.CG C a = (a ∈ C ∨ ValueType.isNull a = true)

def Sym.termCS {T : Type} [ValueType T] {k c n : ℕ} {κ : Fin n → ColKind} : TermGIn T (k + c) κ → CS T k c n

The source of a term: its column, parameter, context value or constant. A term with a function (outside the minimal signature) reads as the constant 0.

Equations

• Sym.termCS (TermGIn.const a) = Sym.CS.const a
• Sym.termCS (TermGIn.outer o) = Fin.addCases (fun (i : Fin k) => Sym.CS.par i) (fun (j : Fin c) => Sym.CS.amb j) o
• Sym.termCS (TermGIn.index i a) = Sym.CS.col i
• Sym.termCS (TermGIn.provIndex i a) = Sym.CS.col i
• Sym.termCS x✝ = Sym.CS.const 0

def Sym.projCS {T : Type} [ValueType T] {k c n : ℕ} {κ : Fin n → ColKind} : ProjColIn T (k + c) κ → CS T k c n

The source of a projection column. A column applying an arbitrary function (outside every signature) reads as the constant 0.

Equations

• Sym.projCS (ProjColIn.term t) = Sym.termCS t
• Sym.projCS (ProjColIn.token i a) = Sym.CS.col i
• Sym.projCS (ProjColIn.aggTerm k_1 a a_1) = Sym.CS.const 0
• Sym.projCS (ProjColIn.aggTermOf i a (TermIn.const a_1)) = Sym.CS.const a_1
• Sym.projCS (ProjColIn.aggTermOf i a (TermIn.outer a_1)) = Sym.CS.col i
• Sym.projCS (ProjColIn.aggTermOf i a t) = Sym.CS.const 0
• Sym.projCS (ProjColIn.provTerm t) = Sym.termCS t

Predicates

def Sym.transPred {T : Type} [ValueType T] {k c n : ℕ} (P : ℕ) {κ : Fin n → ColKind} : GenPredIn T (k + c) κ → SP T c ((k + n) * (7 + k) + P)

A predicate over a symbolic row, cell by cell.

Equations

• One or more equations did not get rendered due to their size.
• Sym.transPred P (GenPredIn.cmp op t₁ t₂) = Sym.cellCmp op (Sym.CS.sa P (Sym.termCS t₁)) (Sym.CS.sa P (Sym.termCS t₂))
• Sym.transPred P (GenPredIn.aggCmp i a op t) = Sym.cellCmp op (Sym.CS.sa P (Sym.CS.col i)) (Sym.CS.sa P (Sym.termCS t))
• Sym.transPred P (φ.and ψ) = (Sym.transPred P φ).and (Sym.transPred P ψ)
• Sym.transPred P (φ.or ψ) = (Sym.transPred P φ).or (Sym.transPred P ψ)
• Sym.transPred P φ.not = (Sym.transPred P φ).not

theorem Sym.eval3_transPred {T : Type} [ValueType T] {k c n : ℕ} {C : Finset T} (P : ℕ) {κ : Fin n → ColKind} (φ : GenPredIn T (k + c) κ) (hφ : φ.noFun = true) (hφc : ∀ a ∈ φ.consts, CG C a) (par : Fin k → T) (γ : Fin c → T) (v : Tuple T n) (e : Tuple T P) (hv : ∀ (i : Fin n), GoodVal par (v i)) (hamb : ∀ (j : Fin c), CG C (γ j)) : (transPred P φ).eval3 (rowEncP C par v e) γ = φ.evalPlain3 v (Fin.append par γ)

The translated predicate has the original's three-valued truth on the encoding of a row, where the values involved are good.

Classical selections

def Sym.termCST {T : Type} [ValueType T] {k n : ℕ} : TermIn T 0 n → CS T k 0 n

The source of a term of a classical selection.

Equations

• Sym.termCST (TermIn.const a) = Sym.CS.const a
• Sym.termCST #i = Sym.CS.col i
• Sym.termCST x✝ = Sym.CS.const 0

def Sym.transSel {T : Type} [ValueType T] {k n : ℕ} (P : ℕ) : Selection T n → SP T 0 ((k + n) * (7 + k) + P)

A classical selection over a symbolic row, cell by cell.

Equations

• Sym.transSel P (Selection.BT b) = Sym.cellCmp b.toCompOp (Sym.CS.sa P (Sym.termCST b.args.1)) (Sym.CS.sa P (Sym.termCST b.args.2))
• Sym.transSel P φ.Not = (Sym.transSel P φ).not
• Sym.transSel P (φ.And ψ) = (Sym.transSel P φ).and (Sym.transSel P ψ)
• Sym.transSel P (φ.Or ψ) = (Sym.transSel P φ).or (Sym.transSel P ψ)
• Sym.transSel P Selection.True = Sym.SP.tru

Projections onto symbolic rows

def Sym.projSA {T : Type} {c N M : ℕ} (f : Fin M → SA T c N) : Tuple (ProjColIn T c (ColKind.allReg N)) M

A projection by arguments: each output column one argument.

Equations

• Sym.projSA f x = ProjColIn.term (f x).toG

theorem Sym.projSA_kind {T : Type} {c N M : ℕ} (f : Fin M → SA T c N) : (fun (x : Fin M) => (projSA f x).kind) = ColKind.allReg M

def Sym.symProjSA {T : Type} [ValueType T] {k c n : ℕ} (P : ℕ) {m : ℕ} (srcs : Fin m → CS T k c n) : Fin ((k + m) * (7 + k) + P) → SA T c ((k + n) * (7 + k) + P)

The argument of an output column of a symbolic projection: the descriptor's cells copied, then the sources' cells, then the further columns copied.

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite