The environment of the symbolic evaluation, built from a cut

The symbolic evaluation (Provenance.SymTab) reads its descriptors and the counters of its bounded recursions off an environment (Sym.SymEnv). This file builds both from a query computing the cut, as unary relations over the ambient context, and proves the environment sound wherever the cut holds the null (Sym.envOK_envOf).

The counters of a recursion of arity n are the rows of E^K, E the non-null values of the cut with the two constants 0 and ValueType.nonzero, and K = n (k + 3): there are at least as many as the rounds a restricted bag recursion over good values can run.

Unary relations of values

def Sym.nnQ {T : Type} {c : ℕ} (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c 1 (ColKind.allReg 1)

The non-null rows of a unary relation.

Equations

• Sym.nnQ CQ = AggQueryIn.Sel (GenPredIn.cmp CompOp.eq (TermGIn.index 0 Sym.nnQ._proof_2) (TermGIn.index 0 Sym.nnQ._proof_2)) CQ trivial

def Sym.constQ {T : Type} {c : ℕ} (a : T) : AggQueryIn T c 1 (ColKind.allReg 1)

The one row holding a constant.

Equations

• Sym.constQ a = AggQueryIn.Param (fun (x : Fin 1) => Sum.inl a) (ColKind.allReg 1)

The alphabet of the counters

def Sym.alphaQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c 1 (ColKind.allReg 1)

The values counters are written with: the non-null values of the cut, 0 and ValueType.nonzero, each once.

Equations

• Sym.alphaQ f CQ = (AggQueryIn.sumByMuX (f 0) (f 1) (Sym.nnQ CQ) (AggQueryIn.sumByMuX (f 2) (f 3) (Sym.constQ 0) (Sym.constQ ValueType.nonzero))).dedupG

def Sym.FreshFor {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (f : ℕ → String) (q : AggQueryIn T c n κ l) : Prop

The supply names a query does not mention.

Equations

• Sym.FreshFor f q = ∀ (i : ℕ), AggQueryIn.noMention (f i) q

Powers of a unary relation

def Sym.powU {T : Type} {c : ℕ} (EQ : AggQueryIn T c 1 (ColKind.allReg 1)) (K : ℕ) : AggQueryIn T c K (ColKind.allReg K)

The K-th power of a unary relation, by products.

Equations

• Sym.powU EQ 0 = AggQueryIn.unitC
• Sym.powU EQ K.succ = Sym.prodR (Sym.powU EQ K) EQ

The counters

def Sym.ctrW (k n : ℕ) : ℕ

The width of the counters of a recursion of arity n, for k parameter components.

Equations

• Sym.ctrW k n = (k + 3) * n

def Sym.ctrQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) (K : ℕ) : AggQueryIn T c K (ColKind.allReg K)

The counters: the rows of E^K.

Equations

• Sym.ctrQ f CQ K = Sym.powU (Sym.alphaQ f CQ) K

def Sym.lqQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) (K : ℕ) : AggQueryIn T c K (ColKind.allReg K)

The least counter.

Equations

• Sym.lqQ f cnt CQ K = Sym.leastQ (f 4) (f 5) cnt (Sym.ctrQ f CQ K)

def Sym.sqQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) (K : ℕ) : AggQueryIn T c (K + K) (ColKind.allReg (K + K))

The successor relation of the counters.

Equations

• Sym.sqQ f cnt CQ K = Sym.succQ (f 6) (f 7) cnt (Sym.ctrQ f CQ K)

noncomputable def Sym.valsU {T : Type} [ValueType T] (R : Multiset (Tuple T 1)) : Finset T

The values of a unary relation, as a finite set.

Equations

• Sym.valsU R = (Multiset.map (fun (y : Tuple T 1) => y 0) R).toFinset

The bound above a gap

The cells of the descriptors

def Sym.cellSA {T : Type} {c N k : ℕ} (v : Fin 7 → SA T c N) (th : Fin k → SA T c N) : Fin (7 + k) → SA T c N

A cell's columns as arguments: seven columns and the rank's.

Equations

• Sym.cellSA v th = Fin.addCases v th

def Sym.thRowQ {T : Type} [ValueType T] {c : ℕ} (k r : ℕ) : AggQueryIn T c k (ColKind.allReg k)

The row of a constant thermometer.

Equations

• Sym.thRowQ k r = AggQueryIn.Param (fun (j : Fin k) => Sum.inl (Sym.therm k r j)) (ColKind.allReg k)

def Sym.thQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (k a✝ : ℕ) : AggQueryIn T c k (ColKind.allReg k)

The ranks from 0 to r in unary.

Equations

• Sym.thQ f k 0 = Sym.thRowQ k 0
• Sym.thQ f k K.succ = AggQueryIn.sumByMuX (f (2 * K)) (f (2 * K + 1)) (Sym.thQ f k K) (Sym.thRowQ k (K + 1))

The five kinds of cells

def Sym.concP {T : Type} [ValueType T] {c : ℕ} (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (7 + k) (ColKind.allReg (7 + k))

A concrete cell for each value of the cut.

Equations

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

def Sym.thP {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (k : ℕ) : AggQueryIn T c k (ColKind.allReg k)

The unary ranks.

Equations

• Sym.thP f k = Sym.thQ (fun (i : ℕ) => f (i + 16)) k k

def Sym.succP {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (7 + k) (ColKind.allReg (7 + k))

A cell for each gap above a non-null value of the cut with a value above it.

Equations

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

def Sym.topP {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (7 + k) (ColKind.allReg (7 + k))

A cell for each gap above the greatest non-null value of the cut.

Equations

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

def Sym.botP {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (7 + k) (ColKind.allReg (7 + k))

The cells of the gap below the least non-null value of the cut.

Equations

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

def Sym.emptyQ {T : Type} [ValueType T] {c : ℕ} (s₁ s₂ : String) (cnt : SeqAggFunc T) (R : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c 0 (ColKind.allReg 0)

The empty row where the cut holds no non-null value, nothing elsewhere.

Equations

• Sym.emptyQ s₁ s₂ cnt R = AggQueryIn.notInDiffX s₁ s₂ cnt AggQueryIn.unitC (Sym.projQ (fun (j : Fin 0) => j.elim0) R)

def Sym.botEP {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (7 + k) (ColKind.allReg (7 + k))

The cells of the one gap of a cut with no non-null value.

Equations

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

The cells

def Sym.cellsQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (7 + k) (ColKind.allReg (7 + k))

The cells of the descriptors, each once.

Equations

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

def Sym.GapOK {T : Type} [ValueType T] (C : Finset T) : WithBot T → Prop

A gap's lower bound: none, or a non-null value of the cut.

Equations

• Sym.GapOK C none = True
• Sym.GapOK C (some t) = (t ∈ C ∧ ValueType.isNull t = false)

def Sym.CellShape {T : Type} [ValueType T] (C : Finset T) (k : ℕ) (x : Tuple T (7 + k)) : Prop

The cells: a value of the cut, or a gap with a rank at most k.

Equations

• Sym.CellShape C k x = ((∃ a ∈ C, x = Sym.enc C k (Sym.Code.conc a)) ∨ ∃ (l : WithBot T) (r : ℕ), Sym.GapOK C l ∧ r ≤ k ∧ x = Sym.enc C k (Sym.Code.fresh l r))

Powers of a relation, block by block

theorem Sym.blk_lt {m K i j : ℕ} (hi : i < K) (hj : j < m) : m * i + j < m * K

def Sym.blk {T : Type} (m K : ℕ) (v : Tuple T (m * K)) (i : Fin K) : Tuple T m

The block i of a row of K blocks of m columns.

Equations

• Sym.blk m K v i j = v ⟨m * ↑i + ↑j, ⋯⟩

def Sym.powX {T : Type} {c m : ℕ} (R : AggQueryIn T c m (ColKind.allReg m)) (K : ℕ) : AggQueryIn T c (m * K) (ColKind.allReg (m * K))

The K-th power of a relation, its rows laid out block after block.

Equations

• Sym.powX R 0 = AggQueryIn.unitC
• Sym.powX R K.succ = Sym.prodR (Sym.powX R K) R

The descriptors

def Sym.descQ {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : AggQueryIn T c (k * (7 + k)) (ColKind.allReg (k * (7 + k)))

The descriptors: k cells.

Equations

• Sym.descQ f cnt k CQ = Sym.projQ (fun (x : Fin (k * (7 + k))) => Sym.SA.col (Fin.cast ⋯ x)) (Sym.powX (Sym.cellsQ f cnt k CQ) k)

The environment

def Sym.envOf {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) (cnt : SeqAggFunc T) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) : SymEnv T k c

The environment of the symbolic evaluation, built from a cut.

Equations

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

theorem Sym.envOK_envOf {T : Type} [ValueType T] {c : ℕ} (f : ℕ → String) {cnt : SeqAggFunc T} (hc : cnt.Counts) (k : ℕ) (CQ : AggQueryIn T c 1 (ColKind.allReg 1)) (hfr : FreshFor f CQ) (D : Database T) (γ : Fin c → T) (hnull : ∀ (a : T), ValueType.isNull a = true → a ∈ valsU (CQ.evaluatePlain D γ)) : EnvOK (envOf f cnt k CQ) D γ

The environment built from a cut is sound wherever the cut holds the null.

Home · Documentation · Publications · Contributors · Source · Cite