The difference in place of the selection

{∅, Π, −, apply, γ, win, μ^⊎} generates the whole algebra in the minimal universe: a selection is an apply of its input with a closed test that holds the empty tuple once where the predicate is true at the row and nothing elsewhere. The tests are built from the difference alone, except for the order: x < y is read by a window counting, over the relation {x, y} (a bag recursion of one round), the rows strictly before y, and that count is compared with 0 as a key, which Explode allows.

def basisRecDiffOps : Set OpKind

The classes of the basis with the difference in place of the selection: ∅, Π, −, the apply, γ, win, μ^⊎.

Equations

• basisRecDiffOps = {OpKind.empty, OpKind.proj, OpKind.diff, OpKind.apply, OpKind.gamma, OpKind.win, OpKind.muBag}

Truth values as relations of arity 0

@[reducible, inline]

abbrev DiffBasis.rows {T : Type} {k : ℕ} (X : Relation T k) : Multiset (Tuple T k)

A relation read as the bag of its rows.

Equations

• DiffBasis.rows X = X

def DiffBasis.val {T : Type} {C : ℕ} (γ : Fin C → T) (e : T ⊕ Fin C) : T

The value an expression names: a constant, or a position of the context.

Equations

• DiffBasis.val γ e = Sum.elim id γ e

def DiffBasis.boolRel {T : Type} (b : Bool) : Multiset (Tuple T 0)

The relation of arity 0 holding the empty tuple once where b holds, and nothing elsewhere.

Equations

• DiffBasis.boolRel b = if b = true then {fun (k : Fin 0) => k.elim0} else 0

def DiffBasis.param1 {T : Type} {C : ℕ} (e : T ⊕ Fin C) : AggQueryIn T C 1 (ColKind.allReg 1)

One row, of the value e names.

Equations

• DiffBasis.param1 e = AggQueryIn.Param (fun (x : Fin 1) => e) (ColKind.allReg 1)

def DiffBasis.proj0 {T : Type} {C k : ℕ} (q : AggQueryIn T C k (ColKind.allReg k)) : AggQueryIn T C 0 (ColKind.allReg 0)

Every row projected onto no column.

Equations

• DiffBasis.proj0 q = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (fun (j : Fin 0) => j.elim0) q)

@[reducible, inline]

abbrev DiffBasis.rel {T : Type} {k : ℕ} (X : Multiset (Tuple T k)) : Relation T k

A bag of rows read as a relation.

Equations

• DiffBasis.rel X = X

def DiffBasis.inter {T : Type} {C k : ℕ} (X Y : AggQueryIn T C k (ColKind.allReg k)) : AggQueryIn T C k (ColKind.allReg k)

The rows of X that are rows of Y, by two differences.

Equations

• DiffBasis.inter X Y = X.Diff (X.Diff Y)

def DiffBasis.notT {T : Type} {C : ℕ} (A : AggQueryIn T C 0 (ColKind.allReg 0)) : AggQueryIn T C 0 (ColKind.allReg 0)

Truth negated: the unit minus the test.

Equations

• DiffBasis.notT A = AggQueryIn.unitC.Diff A

def DiffBasis.andT {T : Type} {C : ℕ} (A B : AggQueryIn T C 0 (ColKind.allReg 0)) : AggQueryIn T C 0 (ColKind.allReg 0)

Both tests hold.

Equations

• DiffBasis.andT A B = DiffBasis.inter A B

def DiffBasis.orT {T : Type} {C : ℕ} (A B : AggQueryIn T C 0 (ColKind.allReg 0)) : AggQueryIn T C 0 (ColKind.allReg 0)

One of the two tests holds.

Equations

• DiffBasis.orT A B = DiffBasis.notT (DiffBasis.andT (DiffBasis.notT A) (DiffBasis.notT B))

Equality and nulls

def DiffBasis.eqT {T : Type} {C : ℕ} (a b : T ⊕ Fin C) : AggQueryIn T C 0 (ColKind.allReg 0)

The two values are equal.

Equations

• DiffBasis.eqT a b = DiffBasis.proj0 (DiffBasis.inter (DiffBasis.param1 a) (DiffBasis.param1 b))

def DiffBasis.nnT {T : Type} [ValueType T] {C : ℕ} (a : T ⊕ Fin C) : AggQueryIn T C 0 (ColKind.allReg 0)

The value is not null.

Equations

• DiffBasis.nnT a = match ValueType.nullVal with | none => AggQueryIn.unitC | some ν => DiffBasis.notT (DiffBasis.eqT a (Sum.inl ν))

The order

def DiffBasis.liftE {T : Type} {C : ℕ} (e : T ⊕ Fin C) : T ⊕ Fin (1 + C)

An expression read one position further in, past the row of an apply's left side.

Equations

• DiffBasis.liftE e = Sum.map id (Fin.natAdd 1) e

def DiffBasis.stepBody {T : Type} {C : ℕ} (s : String) (b : T ⊕ Fin C) : AggQueryIn T C 1 (ColKind.allReg 1) [(s, 1)]

The round of the recursion building {a, b}: the row of b, once per row of the recursive relation other than b.

Equations

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

def DiffBasis.r1 {T : Type} (a : T) : Tuple T 1

The row of a value.

Equations

• DiffBasis.r1 a x✝ = a

def DiffBasis.pairZ {T : Type} {C : ℕ} (s : String) (a b : T ⊕ Fin C) : AggQueryIn T C 1 (ColKind.allReg 1)

{a, b} – {a} where the two are equal – as a bag recursion of one round from a.

Equations

• DiffBasis.pairZ s a b = AggQueryIn.Mu s (DiffBasis.param1 a) (DiffBasis.stepBody s b)

@[reducible, inline]

abbrev DiffBasis.PairQ (T : Type) [ValueType T] : Type

A way to build {a, b} from two expressions, at every context.

Equations

• DiffBasis.PairQ T = ({C : ℕ} → T ⊕ Fin C → T ⊕ Fin C → AggQueryIn T C 1 (ColKind.allReg 1))

def DiffBasis.PairSpec {T : Type} [ValueType T] (pr : PairQ T) : Prop

What {a, b} is asked: defined everywhere, {a} where the two are equal and {a, b} otherwise.

Equations

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

def DiffBasis.prZ {T : Type} [ValueType T] (s : String) : PairQ T

{a, b} by a bag recursion of one round.

Equations

• DiffBasis.prZ s a b = DiffBasis.pairZ s a b

def DiffBasis.beforeW {T : Type} : ValueFrame T 1

The frame of the rows strictly before the current one, its peers and itself excluded.

Equations

• DiffBasis.beforeW = { cond := FrameCond.lt (OrderSpec.asc 1), self := false }

def DiffBasis.P0 : Tuple (Fin 1) 0

No partition.

Equations

• DiffBasis.P0 j = j.elim0

def DiffBasis.O0 : Tuple (Fin 1) 1

Ordered by the one column.

Equations

• DiffBasis.O0 x✝ = 0

def DiffBasis.ltO {T : Type} [ValueType T] (a b : T) : Bool

Whether a sorts strictly before b, ascending.

Equations

• DiffBasis.ltO a b = (OrderSpec.asc 1).lt (fun (x : Fin 1) => a) fun (x : Fin 1) => b

theorem DiffBasis.kinds_explode : Function.update (Fin.snoc (ColKind.allReg 1) ColKind.agg) (Fin.last 1) ColKind.reg = ColKind.allReg 2

def DiffBasis.winZ {T : Type} {C : ℕ} (cnt : SeqAggFunc T) (Z : AggQueryIn T C 1 (ColKind.allReg 1)) : AggQueryIn T C 2 (ColKind.allReg 2)

{a, b} with, on each row, the number of rows strictly before it, the count read as a key.

Equations

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

def DiffBasis.termOf {T : Type} {C k : ℕ} {κ : Fin k → ColKind} (e : T ⊕ Fin C) : TermGIn T C κ

The value an expression names, as a term.

Equations

• DiffBasis.termOf (Sum.inl a) = TermGIn.const a
• DiffBasis.termOf (Sum.inr j) = TermGIn.outer j

def DiffBasis.projB {T : Type} {C : ℕ} (b : T ⊕ Fin C) (W : AggQueryIn T C 2 (ColKind.allReg 2)) : AggQueryIn T C 2 (ColKind.allReg 2)

Each row's count, beside the value b.

Equations

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

def DiffBasis.ltT {T : Type} [ValueType T] {C : ℕ} (cnt : SeqAggFunc T) (pr : PairQ T) (a b : T ⊕ Fin C) : AggQueryIn T C 0 (ColKind.allReg 0)

a < b, nulls aside: the row of b in {a, b} has a row strictly before it.

Equations

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

theorem DiffBasis.evaluatePlain_ltT {T : Type} [ValueType T] {C : ℕ} {D : Database T} {γ : Fin C → T} {cnt : SeqAggFunc T} (hcnt : cnt.IsCount) {pr : PairQ T} (hpr : PairSpec fun {C : ℕ} => pr) (a b : T ⊕ Fin C) : (ltT cnt (fun {C : ℕ} => pr) a b).evaluatePlain D γ = boolRel (ltO (val γ a) (val γ b) && !ValueType.isNull (val γ a))

Comparisons, in Kleene's logic

def DiffBasis.opE {T : Type} [ValueType T] {C : ℕ} (cnt : SeqAggFunc T) (pr : PairQ T) (op : CompOp) (a b : T ⊕ Fin C) : AggQueryIn T C 0 (ColKind.allReg 0)

The comparison holds, read two-valued: the order through ltT, the equalities through eqT.

Equations

• DiffBasis.opE cnt pr CompOp.eq a b = DiffBasis.eqT a b
• DiffBasis.opE cnt pr CompOp.syneq a b = DiffBasis.eqT a b
• DiffBasis.opE cnt pr CompOp.ne a b = DiffBasis.notT (DiffBasis.eqT a b)
• DiffBasis.opE cnt pr CompOp.synne a b = DiffBasis.notT (DiffBasis.eqT a b)
• DiffBasis.opE cnt pr CompOp.lt a b = DiffBasis.ltT cnt (fun {C : ℕ} => pr) a b
• DiffBasis.opE cnt pr CompOp.gt a b = DiffBasis.ltT cnt (fun {C : ℕ} => pr) b a
• DiffBasis.opE cnt pr CompOp.le a b = DiffBasis.notT (DiffBasis.ltT cnt (fun {C : ℕ} => pr) b a)
• DiffBasis.opE cnt pr CompOp.ge a b = DiffBasis.notT (DiffBasis.ltT cnt (fun {C : ℕ} => pr) a b)

def DiffBasis.cmpTF {T : Type} [ValueType T] {C : ℕ} (cnt : SeqAggFunc T) (pr : PairQ T) (op : CompOp) (a b : T ⊕ Fin C) : AggQueryIn T C 0 (ColKind.allReg 0) × AggQueryIn T C 0 (ColKind.allReg 0)

A comparison's truth and falsity: for a null-strict one, both values non-null and the comparison, or its negation; for IS [NOT] DISTINCT FROM, equality, which is never unknown.

Equations

• One or more equations did not get rendered due to their size.
• DiffBasis.cmpTF cnt pr CompOp.syneq a b = (DiffBasis.eqT a b, DiffBasis.notT (DiffBasis.eqT a b))
• DiffBasis.cmpTF cnt pr CompOp.synne a b = (DiffBasis.notT (DiffBasis.eqT a b), DiffBasis.eqT a b)

Predicates

def DiffBasis.termE {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} : TermGIn T c κ → T ⊕ Fin (n + c)

A term of the minimal signature as an expression of the test's context, the row of the selection's input coming first.

Equations

• DiffBasis.termE (TermGIn.const a) = Sum.inl a
• DiffBasis.termE (TermGIn.outer j) = Sum.inr (Fin.natAdd n j)
• DiffBasis.termE (TermGIn.index k a) = Sum.inr (Fin.castAdd c k)
• DiffBasis.termE (TermGIn.provIndex k a) = Sum.inr (Fin.castAdd c k)
• DiffBasis.termE x✝ = Sum.inl 0

def DiffBasis.predTF {T : Type} [ValueType T] (cnt : SeqAggFunc T) (pr : PairQ T) {c n : ℕ} {κ : Fin n → ColKind} : GenPredIn T c κ → AggQueryIn T (n + c) 0 (ColKind.allReg 0) × AggQueryIn T (n + c) 0 (ColKind.allReg 0)

The test of a predicate, true and false: the first holds the empty tuple where the predicate is true at the row, the second where it is false.

Equations

• One or more equations did not get rendered due to their size.
• DiffBasis.predTF cnt pr (GenPredIn.cmp op t₁ t₂) = DiffBasis.cmpTF cnt (fun {C : ℕ} => pr) op (DiffBasis.termE t₁) (DiffBasis.termE t₂)
• DiffBasis.predTF cnt pr (GenPredIn.aggCmp k a op t) = DiffBasis.cmpTF cnt (fun {C : ℕ} => pr) op (Sum.inr (Fin.castAdd c k)) (DiffBasis.termE t)
• DiffBasis.predTF cnt pr φ.not = ((DiffBasis.predTF cnt (fun {C : ℕ} => pr) φ).2, (DiffBasis.predTF cnt (fun {C : ℕ} => pr) φ).1)

The tests are in the fragment

def DiffBasis.selTestOps : Set OpKind

The classes every test uses: ∅, Π, −, γ and win; the pair {a, b} adds its own.

Equations

• DiffBasis.selTestOps = {OpKind.empty, OpKind.proj, OpKind.diff, OpKind.gamma, OpKind.win}

structure DiffBasis.TestOK {T : Type} [ValueType T] (S : Set OpKind) (Θ : Set (SeqAggFunc T)) (Q : Schema → Prop) {C k : ℕ} {κ : Fin k → ColKind} (q : AggQueryIn T C k κ) : Prop

What a closed test is asked: its classes, its signature, a schema satisfying Q, no relation mentioned, and defined everywhere.

• uses : AggQueryIn.usesOnly S q
• sig : AggQueryIn.inSig Θ q
• over (sch : Schema) : Q sch → AggQueryIn.overSchema sch q
• noM (x : String) : AggQueryIn.noMention x q
• settles (D : Database T) (γ : Fin C → T) : q.SettlesAt D γ
• preg : q.paramsReg

def DiffBasis.PairOK {T : Type} [ValueType T] (S : Set OpKind) (Θ : Set (SeqAggFunc T)) (Q : Schema → Prop) (pr : PairQ T) : Prop

A pair construction whose pairs are in the fragment.

Equations

• DiffBasis.PairOK S Θ Q pr = ∀ {C : ℕ} (a b : T ⊕ Fin C), DiffBasis.TestOK S Θ Q (pr a b)

A selection as an apply

theorem DiffBasis.kinds_append0 {n : ℕ} (κ : Fin n → ColKind) : Fin.append κ (ColKind.allReg 0) = κ

def DiffBasis.selX {T : Type} [ValueType T] (cnt : SeqAggFunc T) (pr : PairQ T) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (φ : GenPredIn T c κ) (q : AggQueryIn T c n κ l) : AggQueryIn T c n κ l

A selection written with the apply: each row of the input meets the test of the predicate at that row, which holds the empty tuple once where the predicate is true and nothing elsewhere.

Equations

• DiffBasis.selX cnt pr φ q = AggQueryIn.castKind ⋯ (q.Apply (DiffBasis.predTF cnt (fun {C : ℕ} => pr) φ).1)

theorem DiffBasis.evaluatePlain_selX {T : Type} [ValueType T] {cnt : SeqAggFunc T} (hcnt : cnt.IsCount) {pr : PairQ T} (hpr : PairSpec fun {C : ℕ} => pr) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (φ : GenPredIn T c κ) (hφ : φ.noFun = true) (q : AggQueryIn T c n κ l) (D : Database T) (γ : Fin c → T) : (selX cnt (fun {C : ℕ} => pr) φ q).evaluatePlain D γ = Multiset.filter (fun (u : Tuple T n) => φ.holdsPlain u γ) (q.evaluatePlain D γ)

The pass

The basis with the difference

theorem basisRecDiffOps_generatesOnRec {T : Type} [ValueType T] (sch : Schema) (cnt : SeqAggFunc T) (hcnt : cnt.IsCount) : GeneratesOnRec T sch cnt basisRecDiffOps

{∅, Π, −, apply, γ, win, μ^⊎} generates the whole algebra in the minimal universe: every query of the algebra over a schema, in the signature with a count as its only aggregate, is matched by one over those seven classes, defined and equal wherever the query is. First the query is matched over {∅, Π, σ, apply, γ, win, μ^⊎} (basisRecOps_generatesOnRec), then each selection of the match becomes an apply of its test (DiffBasis.exists_selPass), the order being read by a window and its count compared as a key.

theorem basisRecDiffOps_isBasis : (∀ (sch : Schema), GeneratesOnRec ℕ sch SeqAggFunc.count basisRecDiffOps) ∧ ∀ S ⊂ basisRecDiffOps, ¬∀ (sch : Schema), GeneratesOnRec ℕ sch SeqAggFunc.count S

basisRecDiffOps is a basis of the whole algebra in the minimal universe over ℕ: it generates over every schema, and no proper subset does.

Home · Documentation · Publications · Contributors · Source · Cite