Codes as columns, and comparisons between them

A code (Provenance.SymCode) is stored in 7 + k columns, k the number of parameter components: a flag saying whether the code is fresh, the value (or the gap's lower bound, the least value of the cut for the gap below it), a flag for the gap below the least value, the gap's upper bound and a flag for the gap above the greatest, two columns placing the code against its value – before it, at it or after it, which is what an order on cells reads – and the rank written in unary over the two constants 0 and ValueType.nonzero taken in increasing order (Sym.therm).

A comparison between two cells is a predicate over their columns (Sym.cellCmp), written in a small syntax of comparisons over columns, constants and the ambient context (Sym.SP) that compiles both to the general predicates (Sym.SP.toGen) and to the classical selections of a FILTER clause (Sym.SP.toSel). Its three-valued truth on the encodings of two codes is exactly that of the comparison between the values they stand for (Sym.eval3_cellCmp), unknown included: a comparison with the null is unknown whatever the code it is compared with.

Comparisons over columns, constants and the context

inductive Sym.SA (T : Type) (c n : ℕ) : Type

An argument of a comparison: a constant, a column, or a value of the context.

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

def Sym.SA.eval {T : Type} {c n : ℕ} : SA T c n → Tuple T n → (Fin c → T) → T

What an argument reads on a row in a context.

Equations

• (Sym.SA.const a).eval x✝¹ x✝ = a
• (Sym.SA.col i).eval x✝¹ x✝ = x✝¹ i
• (Sym.SA.amb j).eval x✝¹ x✝ = x✝ j

inductive Sym.SP (T : Type) (c n : ℕ) : Type

A predicate of comparisons, the shape every translated comparison has.

• atom {T : Type} {c n : ℕ} (op : CompOp) (a b : SA T c n) : SP T c n
• and {T : Type} {c n : ℕ} (p q : SP T c n) : SP T c n
• or {T : Type} {c n : ℕ} (p q : SP T c n) : SP T c n
• not {T : Type} {c n : ℕ} (p : SP T c n) : SP T c n
• tru {T : Type} {c n : ℕ} : SP T c n
• fls {T : Type} {c n : ℕ} : SP T c n

def Sym.SP.eval3 {T : Type} [ValueType T] {c n : ℕ} : SP T c n → Tuple T n → (Fin c → T) → Kleene

Its three-valued truth.

Equations

• (Sym.SP.atom op a b).eval3 x✝¹ x✝ = op.eval3 (a.eval x✝¹ x✝) (b.eval x✝¹ x✝)
• (p.and q).eval3 x✝¹ x✝ = (p.eval3 x✝¹ x✝).and (q.eval3 x✝¹ x✝)
• (p.or q).eval3 x✝¹ x✝ = (p.eval3 x✝¹ x✝).or (q.eval3 x✝¹ x✝)
• p.not.eval3 x✝¹ x✝ = (p.eval3 x✝¹ x✝).not
• Sym.SP.tru.eval3 x✝¹ x✝ = Kleene.true
• Sym.SP.fls.eval3 x✝¹ x✝ = Kleene.false

def Sym.SA.toG {T : Type} {c n : ℕ} : SA T c n → TermGIn T c (ColKind.allReg n)

An argument as a term of the general syntax over regular columns.

Equations

• (Sym.SA.const a).toG = TermGIn.const a
• (Sym.SA.col i).toG = TermGIn.index i ⋯
• (Sym.SA.amb j).toG = TermGIn.outer j

def Sym.SP.toGen {T : Type} [ValueType T] {c n : ℕ} : SP T c n → GenPredIn T c (ColKind.allReg n)

The predicate in the general syntax.

Equations

• (Sym.SP.atom op a b).toGen = GenPredIn.cmp op a.toG b.toG
• (p.and q).toGen = p.toGen.and q.toGen
• (p.or q).toGen = p.toGen.or q.toGen
• p.not.toGen = p.toGen.not
• Sym.SP.tru.toGen = GenPredIn.cmp CompOp.syneq (TermGIn.const 0) (TermGIn.const 0)
• Sym.SP.fls.toGen = GenPredIn.cmp CompOp.syneq (TermGIn.const 0) (TermGIn.const ValueType.nonzero)

theorem Sym.SP.hasAggAtom_toGen {T : Type} [ValueType T] {c n : ℕ} (p : SP T c n) : p.toGen.hasAggAtom = false

A translated predicate reads no aggregate column.

def Sym.SA.toT {T : Type} {n : ℕ} : SA T 0 n → Term T n

An argument as a term of a classical selection, where there is no context.

Equations

• (Sym.SA.const a).toT = TermIn.const a
• (Sym.SA.col i).toT = #i
• (Sym.SA.amb j).toT = j.elim0

def Sym.boolOf {T : Type} {n : ℕ} (op : CompOp) (t₁ t₂ : Term T n) : BoolTerm T n

A comparison as a Boolean term.

Equations

• Sym.boolOf CompOp.eq t₁ t₂ = BoolTerm.EQ t₁ t₂
• Sym.boolOf CompOp.ne t₁ t₂ = BoolTerm.NE t₁ t₂
• Sym.boolOf CompOp.lt t₁ t₂ = BoolTerm.LT t₁ t₂
• Sym.boolOf CompOp.le t₁ t₂ = BoolTerm.LE t₁ t₂
• Sym.boolOf CompOp.gt t₁ t₂ = BoolTerm.GT t₁ t₂
• Sym.boolOf CompOp.ge t₁ t₂ = BoolTerm.GE t₁ t₂
• Sym.boolOf CompOp.syneq t₁ t₂ = BoolTerm.SYNEQ t₁ t₂
• Sym.boolOf CompOp.synne t₁ t₂ = BoolTerm.SYNNE t₁ t₂

def Sym.SP.toSel {T : Type} {n : ℕ} : SP T 0 n → Selection T n

The predicate as a classical selection.

Equations

• (Sym.SP.atom op a b).toSel = Selection.BT (Sym.boolOf op a.toT b.toT)
• (p.and q).toSel = p.toSel.And q.toSel
• (p.or q).toSel = p.toSel.Or q.toSel
• p.not.toSel = p.toSel.Not
• Sym.SP.tru.toSel = Selection.True
• Sym.SP.fls.toSel = Selection.True.Not

The columns of a code

def Sym.sLo {T : Type} [ValueType T] : T

The smaller of the two constants.

Equations

• Sym.sLo = if 0 < ValueType.nonzero then 0 else ValueType.nonzero

def Sym.sHi {T : Type} [ValueType T] : T

The larger of the two constants.

Equations

• Sym.sHi = if 0 < ValueType.nonzero then ValueType.nonzero else 0

def Sym.therm {T : Type} [ValueType T] (k r : ℕ) : Fin k → T

A rank in unary: k columns, the first r holding the larger of the two constants and the others the smaller, so that the ranks are ordered as their columns are, lexicographically.

Equations

• Sym.therm k r j = if ↑j < r then Sym.sHi else Sym.sLo

def Sym.wbFlag {T : Type} [ValueType T] : WithBot T → T

Whether the gap is below the least value.

Equations

• Sym.wbFlag none = ValueType.nonzero
• Sym.wbFlag (some val) = 0

def Sym.wtVal {T : Type} [ValueType T] : WithTop T → T

A gap's upper bound as a column (0 above the greatest value).

Equations

• Sym.wtVal none = 0
• Sym.wtVal (some a) = a

def Sym.wtFlag {T : Type} [ValueType T] : WithTop T → T

Whether the gap is above the greatest value.

Equations

• Sym.wtFlag none = ValueType.nonzero
• Sym.wtFlag (some a) = 0

def Sym.upOf {T : Type} [ValueType T] (C : Finset T) (l : WithBot T) : WithTop T

The gap's upper bound: the least non-null value of the cut above the lower bound.

Equations

• Sym.upOf C l = {t ∈ C | ValueType.isNull t = false ∧ l < ↑t}.min

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

A gap's lower bound as a column: the least value of the cut for the gap below it (0 if the cut holds no non-null value).

Equations

• Sym.lval C none = Sym.wtVal (Sym.upOf C ⊥)
• Sym.lval C (some val) = val

def Sym.posA {T : Type} [ValueType T] : Code T → T

Where a code sits against its value column, first column: before it (a gap below the least value), at it (a concrete value), after it (a gap above its lower bound) read as (sLo, sLo), (sLo, sHi), (sHi, sLo).

Equations

• Sym.posA (Sym.Code.conc a) = Sym.sLo
• Sym.posA (Sym.Code.fresh none r) = Sym.sLo
• Sym.posA (Sym.Code.fresh (some val) r) = Sym.sHi

def Sym.posB {T : Type} [ValueType T] : Code T → T

The second column.

Equations

• Sym.posB (Sym.Code.conc a) = Sym.sHi
• Sym.posB (Sym.Code.fresh l r) = Sym.sLo

def Sym.enc {T : Type} [ValueType T] (C : Finset T) (k : ℕ) : Code T → Tuple T (7 + k)

A code as 7 + k columns.

Equations

• One or more equations did not get rendered due to their size.
• Sym.enc C k (Sym.Code.conc a) = Fin.append ![0, a, 0, 0, 0, Sym.sLo, Sym.sHi] fun (x : Fin k) => 0

@[reducible, inline]

abbrev Sym.iF (k : ℕ) : Fin (7 + k)

The column of the fresh flag.

Equations

• Sym.iF k = Fin.castAdd k 0

@[reducible, inline]

abbrev Sym.iV (k : ℕ) : Fin (7 + k)

The column of the value or of the gap's lower bound.

Equations

• Sym.iV k = Fin.castAdd k 1

@[reducible, inline]

abbrev Sym.iB (k : ℕ) : Fin (7 + k)

The column of the below-the-least flag.

Equations

• Sym.iB k = Fin.castAdd k 2

@[reducible, inline]

abbrev Sym.iH (k : ℕ) : Fin (7 + k)

The column of the gap's upper bound.

Equations

• Sym.iH k = Fin.castAdd k 3

@[reducible, inline]

abbrev Sym.iHB (k : ℕ) : Fin (7 + k)

The column of the above-the-greatest flag.

Equations

• Sym.iHB k = Fin.castAdd k 4

@[reducible, inline]

abbrev Sym.iSA (k : ℕ) : Fin (7 + k)

The first column placing the code against its value.

Equations

• Sym.iSA k = Fin.castAdd k 5

@[reducible, inline]

abbrev Sym.iSB (k : ℕ) : Fin (7 + k)

The second.

Equations

• Sym.iSB k = Fin.castAdd k 6

@[reducible, inline]

abbrev Sym.iR {k : ℕ} (j : Fin k) : Fin (7 + k)

The j-th column of the rank.

Equations

• Sym.iR j = Fin.natAdd 7 j

Comparing two cells

def Sym.isZ {T : Type} [ValueType T] {c n : ℕ} (a : SA T c n) : SP T c n

The argument is 0.

Equations

• Sym.isZ a = Sym.SP.atom CompOp.syneq a (Sym.SA.const 0)

def Sym.isN {T : Type} [ValueType T] {c n : ℕ} (a : SA T c n) : SP T c n

The argument is ValueType.nonzero.

Equations

• Sym.isN a = Sym.SP.atom CompOp.syneq a (Sym.SA.const ValueType.nonzero)

def Sym.wrap {T : Type} {c n : ℕ} (a : SA T c n) (Q : SP T c n) : SP T c n

A comparison made strict in a concrete value: unknown where the value is null, Q elsewhere.

Equations

• Sym.wrap a Q = (Sym.SP.atom CompOp.eq a a).and (Q.or (Sym.SP.atom CompOp.eq a a).not)

def Sym.orAll {T : Type} {c n : ℕ} : List (SP T c n) → SP T c n

The disjunction of a list.

Equations

• Sym.orAll [] = Sym.SP.fls
• Sym.orAll (p :: ps) = p.or (Sym.orAll ps)

def Sym.andAll {T : Type} {c n : ℕ} : List (SP T c n) → SP T c n

The conjunction of a list.

Equations

• Sym.andAll [] = Sym.SP.tru
• Sym.andAll (p :: ps) = p.and (Sym.andAll ps)

def Sym.isLo {T : Type} [ValueType T] {c n : ℕ} (a : SA T c n) : SP T c n

The argument is the smaller constant.

Equations

• Sym.isLo a = Sym.SP.atom CompOp.syneq a (Sym.SA.const Sym.sLo)

def Sym.isHi {T : Type} [ValueType T] {c n : ℕ} (a : SA T c n) : SP T c n

The argument is the larger constant.

Equations

• Sym.isHi a = Sym.SP.atom CompOp.syneq a (Sym.SA.const Sym.sHi)

def Sym.thLt {T : Type} [ValueType T] {c n k : ℕ} (x y : Fin (7 + k) → SA T c n) : SP T c n

The first rank below the second.

Equations

• Sym.thLt x y = Sym.orAll (List.map (fun (j : Fin k) => (Sym.isLo (x (Sym.iR j))).and (Sym.isHi (y (Sym.iR j)))) (List.finRange k))

def Sym.thEq {T : Type} {c n k : ℕ} (x y : Fin (7 + k) → SA T c n) : SP T c n

The two ranks equal.

Equations

• Sym.thEq x y = Sym.andAll (List.map (fun (j : Fin k) => Sym.SP.atom CompOp.syneq (x (Sym.iR j)) (y (Sym.iR j))) (List.finRange k))

def Sym.ltCF {T : Type} [ValueType T] {c n k : ℕ} (a : SA T c n) (y : Fin (7 + k) → SA T c n) : SP T c n

A concrete value below a fresh cell.

Equations

• Sym.ltCF a y = (Sym.isZ (y (Sym.iB k))).and (Sym.SP.atom CompOp.le a (y (Sym.iV k)))

def Sym.ltFC {T : Type} [ValueType T] {c n k : ℕ} (x : Fin (7 + k) → SA T c n) (b : SA T c n) : SP T c n

A fresh cell below a concrete value.

Equations

• Sym.ltFC x b = ((Sym.isZ (x (Sym.iB k))).and (Sym.SP.atom CompOp.le b (x (Sym.iV k)))).not

def Sym.ltFF {T : Type} [ValueType T] {c n k : ℕ} (x y : Fin (7 + k) → SA T c n) : SP T c n

A fresh cell below another.

Equations

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

def Sym.eqFF {T : Type} {c n k : ℕ} (x y : Fin (7 + k) → SA T c n) : SP T c n

Two fresh cells equal.

Equations

• Sym.eqFF x y = (Sym.SP.atom CompOp.syneq (x (Sym.iB k)) (y (Sym.iB k))).and ((Sym.SP.atom CompOp.syneq (x (Sym.iV k)) (y (Sym.iV k))).and (Sym.thEq x y))

def Sym.branchCF {T : Type} [ValueType T] {c n k : ℕ} (op : CompOp) (a : SA T c n) (y : Fin (7 + k) → SA T c n) : SP T c n

A concrete value compared with a fresh cell.

Equations

• Sym.branchCF CompOp.eq a y = Sym.wrap a Sym.SP.fls
• Sym.branchCF CompOp.ne a y = Sym.wrap a Sym.SP.tru
• Sym.branchCF CompOp.lt a y = Sym.wrap a (Sym.ltCF a y)
• Sym.branchCF CompOp.le a y = Sym.wrap a (Sym.ltCF a y)
• Sym.branchCF CompOp.gt a y = Sym.wrap a (Sym.ltCF a y).not
• Sym.branchCF CompOp.ge a y = Sym.wrap a (Sym.ltCF a y).not
• Sym.branchCF CompOp.syneq a y = Sym.SP.fls
• Sym.branchCF CompOp.synne a y = Sym.SP.tru

def Sym.branchFC {T : Type} [ValueType T] {c n k : ℕ} (op : CompOp) (x : Fin (7 + k) → SA T c n) (b : SA T c n) : SP T c n

A fresh cell compared with a concrete value.

Equations

• Sym.branchFC CompOp.eq x b = Sym.wrap b Sym.SP.fls
• Sym.branchFC CompOp.ne x b = Sym.wrap b Sym.SP.tru
• Sym.branchFC CompOp.lt x b = Sym.wrap b (Sym.ltFC x b)
• Sym.branchFC CompOp.le x b = Sym.wrap b (Sym.ltFC x b)
• Sym.branchFC CompOp.gt x b = Sym.wrap b (Sym.ltFC x b).not
• Sym.branchFC CompOp.ge x b = Sym.wrap b (Sym.ltFC x b).not
• Sym.branchFC CompOp.syneq x b = Sym.SP.fls
• Sym.branchFC CompOp.synne x b = Sym.SP.tru

def Sym.branchFF {T : Type} [ValueType T] {c n k : ℕ} (op : CompOp) (x y : Fin (7 + k) → SA T c n) : SP T c n

Two fresh cells compared.

Equations

• Sym.branchFF CompOp.eq x y = Sym.eqFF x y
• Sym.branchFF CompOp.ne x y = (Sym.eqFF x y).not
• Sym.branchFF CompOp.lt x y = Sym.ltFF x y
• Sym.branchFF CompOp.le x y = (Sym.ltFF x y).or (Sym.eqFF x y)
• Sym.branchFF CompOp.gt x y = Sym.ltFF y x
• Sym.branchFF CompOp.ge x y = (Sym.ltFF y x).or (Sym.eqFF x y)
• Sym.branchFF CompOp.syneq x y = Sym.eqFF x y
• Sym.branchFF CompOp.synne x y = (Sym.eqFF x y).not

def Sym.cellCmp {T : Type} [ValueType T] {c n k : ℕ} (op : CompOp) (x y : Fin (7 + k) → SA T c n) : SP T c n

Two cells compared: by their values where both are concrete, and through the bounds and ranks of the codes elsewhere.

Equations

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

What a comparison of cells reads

The comparison of two cells is the comparison of their values

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

The codes a cell may hold where the symbolic evaluation is faithful: the code of a fresh component, a value of the cut, or the null.

Equations

• Sym.CodeOK C par x = ((∃ (i : Fin k), Sym.IsFresh C (par i) ∧ x = Sym.code C par i) ∨ ∃ (a : T), (a ∈ C ∨ ValueType.isNull a = true) ∧ x = Sym.Code.conc a)

theorem Sym.eval3_cellCmp {T : Type} [ValueType T] {C : Finset T} {c n k : ℕ} {par : Fin k → T} (op : CompOp) (x y : Fin (7 + k) → SA T c n) (u : Tuple T n) (γ : Fin c → T) {cx cy : Code T} (hcx : CodeOK C par cx) (hcy : CodeOK C par cy) (hx : ∀ (i : Fin (7 + k)), (x i).eval u γ = enc C k cx i) (hy : ∀ (i : Fin (7 + k)), (y i).eval u γ = enc C k cy i) : (cellCmp op x y).eval3 u γ = op.eval3 (dec C par cx) (dec C par cy)

The comparison of two cells is the comparison of the values they stand for, in all three truth values.

Home · Documentation · Publications · Contributors · Source · Cite