The plain basis: which operators a query cannot do without

The basis classification grades the operators of the algebra by what a query without them cannot compute. Each row is one invariant: every query that avoids a class of operators satisfies a property of its plain semantics, and one query using the class breaks it – so no generating set can leave the class out.

This file carries the vocabulary the classification is stated in and the invariants. The scope is the non-recursive queries: Mu and MuSet are partial operators whose value is the one their rounds settle at, and the locality row they belong to is a different argument.

Explode and Retag are transparent here: both read their argument's plain semantics unchanged (AggQueryIn.evaluatePlain), so a plain-semantics statement cannot see them, and they are in no class.

inductive OpKind : Type

The operator classes the basis classification distinguishes. The cross product and the apply are separate: a product is an apply whose right side reads no outer column, so a generating set may contain one without the other.

• empty : OpKind

  The empty relation ∅.

• proj : OpKind

  Generalized projection Π.

• sel : OpKind

  Selection σ.

• prod : OpKind

  Cross product ×.

• apply : OpKind

  The apply, SQL's LATERAL.

• union : OpKind

  Union ⊎.

• dedup : OpKind

  Duplicate elimination ε.

• diff : OpKind

  Difference −.

• gamma : OpKind

  Aggregation γ, grouped and scalar together.

• win : OpKind

  A window function.

• muBag : OpKind

  The bag recursion μ^⊎, SQL's WITH RECURSIVE … UNION ALL.

• muSet : OpKind

  The set recursion μ^∪, SQL's WITH RECURSIVE … UNION.

@[instance_reducible]

instance instDecidableEqOpKind : DecidableEq OpKind

Equations

• instDecidableEqOpKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprOpKind : Repr OpKind

Equations

• instReprOpKind = { reprPrec := instReprOpKind.repr }

def instReprOpKind.repr : OpKind → ℕ → Std.Format

Equations

• instReprOpKind.repr OpKind.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.empty")).group prec✝
• instReprOpKind.repr OpKind.proj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.proj")).group prec✝
• instReprOpKind.repr OpKind.sel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.sel")).group prec✝
• instReprOpKind.repr OpKind.prod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.prod")).group prec✝
• instReprOpKind.repr OpKind.apply prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.apply")).group prec✝
• instReprOpKind.repr OpKind.union prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.union")).group prec✝
• instReprOpKind.repr OpKind.dedup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.dedup")).group prec✝
• instReprOpKind.repr OpKind.diff prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.diff")).group prec✝
• instReprOpKind.repr OpKind.gamma prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.gamma")).group prec✝
• instReprOpKind.repr OpKind.win prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.win")).group prec✝
• instReprOpKind.repr OpKind.muBag prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.muBag")).group prec✝
• instReprOpKind.repr OpKind.muSet prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OpKind.muSet")).group prec✝

def AggQueryIn.usesOnly {T : Type} (S : Set OpKind) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

The classes a query uses are among S. A relation leaf is in no class, every operator is in its own, and Explode and Retag are in none, being transparent to the plain semantics.

Two operators are False: this predicate carries the scope of the classification as well, and the token-building grouping and the provenance sum are outside it. They belong to the rewritten world – they are what ProvSQL's plans build, not what a source query is written with – so a classification of the source language has nothing to say about them.

The two recursions are classes like the others (muBag, muSet), so a class set may or may not hold them. A class set holding neither – plainOps, and every basis of Provenance.BasisAssembly – therefore excludes every recursive query, so the six rows of the recursion-free classification hold as stated.

Equations

• AggQueryIn.usesOnly S (AggQueryIn.Rel x✝ a) = True
• AggQueryIn.usesOnly S (AggQueryIn.Hole x✝¹ s x✝) = True
• AggQueryIn.usesOnly S (AggQueryIn.Param pv x✝) = (OpKind.empty ∈ S ∧ OpKind.proj ∈ S ∧ OpKind.gamma ∈ S)
• AggQueryIn.usesOnly S AggQueryIn.Empty = (OpKind.empty ∈ S)
• AggQueryIn.usesOnly S (AggQueryIn.Proj ps q) = ((OpKind.proj ∈ S ∧ ∀ (j : Fin x✝¹), (ps j).sourceCol = true) ∧ AggQueryIn.usesOnly S q)
• AggQueryIn.usesOnly S (AggQueryIn.Sel φ q hφ) = (OpKind.sel ∈ S ∧ AggQueryIn.usesOnly S q)
• AggQueryIn.usesOnly S (q₁.Prod q₂) = (OpKind.prod ∈ S ∧ AggQueryIn.usesOnly S q₁ ∧ AggQueryIn.usesOnly S q₂)
• AggQueryIn.usesOnly S (q₁.Apply q₂) = (OpKind.apply ∈ S ∧ AggQueryIn.usesOnly S q₁ ∧ AggQueryIn.usesOnly S q₂)
• AggQueryIn.usesOnly S (q₁.Sum q₂) = (OpKind.union ∈ S ∧ AggQueryIn.usesOnly S q₁ ∧ AggQueryIn.usesOnly S q₂)
• AggQueryIn.usesOnly S q.Dedup = (OpKind.dedup ∈ S ∧ AggQueryIn.usesOnly S q)
• AggQueryIn.usesOnly S (q₁.Diff q₂) = (OpKind.diff ∈ S ∧ AggQueryIn.usesOnly S q₁ ∧ AggQueryIn.usesOnly S q₂)
• AggQueryIn.usesOnly S (AggQueryIn.Explode k a q) = AggQueryIn.usesOnly S q
• AggQueryIn.usesOnly S (AggQueryIn.Retag h q) = AggQueryIn.usesOnly S q
• AggQueryIn.usesOnly S (AggQueryIn.Mu s q₀ q₁) = (OpKind.muBag ∈ S ∧ AggQueryIn.usesOnly S q₀ ∧ AggQueryIn.usesOnly S q₁)
• AggQueryIn.usesOnly S (AggQueryIn.MuSet s q₀ q₁) = (OpKind.muSet ∈ S ∧ AggQueryIn.usesOnly S q₀ ∧ AggQueryIn.usesOnly S q₁)
• AggQueryIn.usesOnly S (AggQueryIn.Gamma is ts fs q keep ord) = (OpKind.gamma ∈ S ∧ AggQueryIn.usesOnly S q)
• AggQueryIn.usesOnly S (AggQueryIn.GammaScalar ts fs q ord) = (OpKind.gamma ∈ S ∧ AggQueryIn.usesOnly S q)
• AggQueryIn.usesOnly S (AggQueryIn.GammaNest is his p f q) = ((OpKind.gamma ∈ S ∧ p.sourceCol = true) ∧ AggQueryIn.usesOnly S q)
• AggQueryIn.usesOnly S (AggQueryIn.GammaTok is his ts fs a a_1 keep) = False
• AggQueryIn.usesOnly S (AggQueryIn.ProvSum is his t a) = False
• AggQueryIn.usesOnly S (AggQueryIn.Win P O o w t f q a dist keep) = (OpKind.win ∈ S ∧ AggQueryIn.usesOnly S q)
• AggQueryIn.usesOnly S (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = (OpKind.win ∈ S ∧ AggQueryIn.usesOnly S q_1)

Monotonicity of the classification

def AggQueryIn.PlainEquiv {T : Type} [ValueType T] {c n : ℕ} {κ κ' : Fin n → ColKind} {l l' : List (String × ℕ)} (q : AggQueryIn T c n κ l) (q' : AggQueryIn T c n κ' l') : Prop

Expressibility: two queries of the same arity are equivalent when their plain semantics agree on every instance.

Equations

• q.PlainEquiv q' = ∀ (D : Database T) (γ : Fin c → T), q.evaluatePlain D γ = q'.evaluatePlain D γ

def Database.allEmpty {T : Type} (D : Database T) : Prop

An instance all of whose relations are empty. A name the instance does not hold reads as the empty relation too, so this is the instance over which nothing is there.

Equations

• D.allEmpty = ∀ (k : ℕ) (s : String) (r : Relation T k), Database.find k s D = some r → r = 0

Schemas, and what a relation reference may name

A reference to a relation the instance does not hold reads as the empty relation here, Database.find returning an Option that every evaluator's Rel clause sends to ∅. That is a convention about ill-formed queries, not semantics: a query is written against a schema, and the question what R means on an instance without R should not arise. These definitions say when it does not, so that a statement about plain evaluation can ask for a well-formed query and a conforming instance instead of reading an absent name as empty.

(The same hypotheses are what a reading that made evaluation partial would need: the condition is static, so it belongs in the hypotheses and not in the evaluator's result type.)

structure Schema : Type

A schema: the arity of each relation name it declares, finitely many names being declared.

• decl : String → Option ℕ

  The arity of a name, or none where the schema does not declare it.

• finite : {s : String | self.decl s ≠ none}.Finite

  A schema declares finitely many names.

@[instance_reducible]

instance instCoeFunSchemaForallStringOptionNat : CoeFun Schema fun (x : Schema) => String → Option ℕ

Equations

• instCoeFunSchemaForallStringOptionNat = { coe := Schema.decl }

def Schema.empty : Schema

The schema declaring nothing.

Equations

• Schema.empty = { decl := fun (x : String) => none, finite := Schema.empty._proof_1 }

theorem Schema.update_finite (sch : Schema) (s : String) (k : ℕ) : {s' : String | (if s' = s then some k else sch.decl s') ≠ none}.Finite

Declaring one name, as a recursion's rounds do for the name they bind.

def Schema.update (sch : Schema) (s : String) (k : ℕ) : Schema

Equations

• sch.update s k = { decl := fun (s' : String) => if s' = s then some k else sch.decl s', finite := ⋯ }

def Schema.ofFn (f : String → Option ℕ) (N : Finset String) (h : ∀ (s : String), f s ≠ none → s ∈ N) : Schema

A schema declaring the names of a list, each with an arity.

Equations

• Schema.ofFn f N h = { decl := f, finite := ⋯ }

def AggQueryIn.noMention {T : Type} (s : String) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

The name s does not occur in the query.

Equations

• AggQueryIn.noMention s (AggQueryIn.Rel x✝ s') = (s' ≠ s)
• AggQueryIn.noMention s (AggQueryIn.Hole x✝¹ s_1 x✝) = True
• AggQueryIn.noMention s (AggQueryIn.Param pv x✝) = True
• AggQueryIn.noMention s AggQueryIn.Empty = True
• AggQueryIn.noMention s (AggQueryIn.Proj ps q) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.Sel φ q hφ) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (q₁.Prod q₂) = (AggQueryIn.noMention s q₁ ∧ AggQueryIn.noMention s q₂)
• AggQueryIn.noMention s (q₁.Apply q₂) = (AggQueryIn.noMention s q₁ ∧ AggQueryIn.noMention s q₂)
• AggQueryIn.noMention s (q₁.Sum q₂) = (AggQueryIn.noMention s q₁ ∧ AggQueryIn.noMention s q₂)
• AggQueryIn.noMention s q.Dedup = AggQueryIn.noMention s q
• AggQueryIn.noMention s (q₁.Diff q₂) = (AggQueryIn.noMention s q₁ ∧ AggQueryIn.noMention s q₂)
• AggQueryIn.noMention s (AggQueryIn.Explode k a q) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.Mu s_1 q₀ q₁) = (AggQueryIn.noMention s q₀ ∧ AggQueryIn.noMention s q₁)
• AggQueryIn.noMention s (AggQueryIn.MuSet s_1 q₀ q₁) = (AggQueryIn.noMention s q₀ ∧ AggQueryIn.noMention s q₁)
• AggQueryIn.noMention s (AggQueryIn.Gamma is ts fs q keep ord) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.GammaScalar ts fs q ord) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.GammaNest is his p f q) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.ProvSum is his t q) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.Retag h q) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.GammaTok is his ts fs a q keep) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.Win P O o w t f q a dist keep) = AggQueryIn.noMention s q
• AggQueryIn.noMention s (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = AggQueryIn.noMention s q_1

def AggQueryIn.overSchema {T : Type} (sch : Schema) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

A well-formed query: every relation reference names a relation the schema declares, at the arity the schema gives it. A recursion binds a name the schema does not declare, its base is over the schema, and its term is over the schema extended by that name – which its hole reads – and names it nowhere else (AggQueryIn.noMention): the hole is the one reference to the round, as the typing of the term asks, and a free reference to the bound name would be a second one.

Equations

• AggQueryIn.overSchema sch (AggQueryIn.Rel x✝ a) = (sch.decl a = some x✝)
• AggQueryIn.overSchema sch (AggQueryIn.Hole x✝¹ s x✝) = (sch.decl s = some x✝¹)
• AggQueryIn.overSchema sch (AggQueryIn.Param pv x✝) = True
• AggQueryIn.overSchema sch AggQueryIn.Empty = True
• AggQueryIn.overSchema sch (AggQueryIn.Proj ps q) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (AggQueryIn.Sel φ q hφ) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (q₁.Prod q₂) = (AggQueryIn.overSchema sch q₁ ∧ AggQueryIn.overSchema sch q₂)
• AggQueryIn.overSchema sch (q₁.Apply q₂) = (AggQueryIn.overSchema sch q₁ ∧ AggQueryIn.overSchema sch q₂)
• AggQueryIn.overSchema sch (q₁.Sum q₂) = (AggQueryIn.overSchema sch q₁ ∧ AggQueryIn.overSchema sch q₂)
• AggQueryIn.overSchema sch q.Dedup = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (q₁.Diff q₂) = (AggQueryIn.overSchema sch q₁ ∧ AggQueryIn.overSchema sch q₂)
• AggQueryIn.overSchema sch (AggQueryIn.Explode k a q) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (AggQueryIn.Retag h q) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (AggQueryIn.Mu s q₀ q₁) = (sch.decl s = none ∧ AggQueryIn.overSchema sch q₀ ∧ AggQueryIn.noMention s q₁ ∧ AggQueryIn.overSchema (sch.update s x✝¹) q₁)
• AggQueryIn.overSchema sch (AggQueryIn.MuSet s q₀ q₁) = (sch.decl s = none ∧ AggQueryIn.overSchema sch q₀ ∧ AggQueryIn.noMention s q₁ ∧ AggQueryIn.overSchema (sch.update s x✝) q₁)
• AggQueryIn.overSchema sch (AggQueryIn.Gamma is ts fs q keep ord) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (AggQueryIn.GammaScalar ts fs q ord) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (AggQueryIn.GammaNest is his p f q) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (AggQueryIn.GammaTok is his ts fs a a_1 keep) = AggQueryIn.overSchema sch a_1
• AggQueryIn.overSchema sch (AggQueryIn.ProvSum is his t a) = AggQueryIn.overSchema sch a
• AggQueryIn.overSchema sch (AggQueryIn.Win P O o w t f q a dist keep) = AggQueryIn.overSchema sch q
• AggQueryIn.overSchema sch (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = AggQueryIn.overSchema sch q_1

def Database.Conforms {T : Type} (sch : Schema) (D : Database T) : Prop

A conforming instance: it binds every name the schema declares, at the declared arity.

Equations

• Database.Conforms sch D = ∀ (s : String) (k : ℕ), sch.decl s = some k → ∃ (r : Relation T k), Database.find k s D = some r

def AggQueryIn.PlainEquivOn {T : Type} [ValueType T] (sch : Schema) {c n : ℕ} {κ κ' : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) (q' : AggQueryIn T c n κ') : Prop

Expressibility over a schema: the two queries agree on every instance of that schema, which is what the generation statement asks – a query is not evaluated on an instance of another schema. Agreement on every instance is stronger, and gives this one.

Equations

• AggQueryIn.PlainEquivOn sch q q' = ∀ (D : Database T), Database.Conforms sch D → ∀ (γ : Fin c → T), q.evaluatePlain D γ = q'.evaluatePlain D γ

theorem AggQueryIn.usesEmpty_of_overSchema_empty {T : Type} {S : Set OpKind} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : overSchema Schema.empty q → usesOnly S q → OpKind.empty ∈ S

Over the empty schema nothing can be written without ∅. Every leaf of a query is a relation reference or the empty relation, and the empty schema declares no name – so the empty relation is the only leaf there, and a generating set that omits it generates nothing. This is what the genericity reading of the ∅ row asks: the language is to be defined for every schema, the empty one included. It is not that the unit relation needs ∅: with any name in the schema, γ_∅[](R) is the unit, whatever R holds.

The signature: which functions and which aggregates

The signature 𝒜(Ω, Θ) is a parameter of the language and not of the semantics: Ω says which functions a term may apply to values, Θ which aggregate functions are available. The classification's rows for win and for μ^⊎ are the two that depend on it – they hold in the minimal signature 𝒜(∅, {count}), where a term is a column or a constant and the only aggregate is a count – so the predicates below are what those rows are stated against. The other rows hold for every Ω and every Θ containing a count, and the generation half is stated over every signature, aggregates being arbitrary function parameters of the syntax: that is why AggQueryIn.exists_basisOps_plainEquiv asks only for a counting aggregate and nothing else.

Ω = ∅ cannot be arranged by instantiating a parameter – the vocabulary +, -, *, CASE and COALESCE is built into TermIn – so it is a predicate on terms (noFun). Θ is a set the aggregates are asked to belong to.

def TermIn.noFun {T : Type} {c k : ℕ} : TermIn T c k → Bool

A term that applies no function to values: a column, an outer column, or a constant. Ω = ∅ of the minimal signature.

Equations

• (TermIn.const a).noFun = true
• (TermIn.outer a).noFun = true
• (#a).noFun = true
• (a.add a_1).noFun = false
• (a.sub a_1).noFun = false
• (a.mul a_1).noFun = false
• (TermIn.caseWhen a a_1 a_2 a_3 a_4).noFun = false
• (a.coalesce a_1).noFun = false

def TermGIn.noFun {T : Type} {c k : ℕ} {κ : Fin k → ColKind} : TermGIn T c κ → Bool

The same over the kind-indexed terms. A gate term – a comparison read as a value (cmpAgg, chiGate) – is a function on values too, and belongs to the rewritten world besides.

Equations

• (TermGIn.const a).noFun = true
• (TermGIn.outer a).noFun = true
• (TermGIn.index k_1 a).noFun = true
• (TermGIn.provIndex k_1 a).noFun = true
• (TermGIn.cmpAgg k_1 a a_1 a_2).noFun = false
• (TermGIn.chiGate a a_1 a_2).noFun = false
• (a.add a_1).noFun = false
• (a.sub a_1).noFun = false
• (a.mul a_1).noFun = false
• (TermGIn.caseWhen a a_1 a_2 a_3 a_4).noFun = false
• (a.coalesce a_1).noFun = false

def BoolTerm.noFun {T : Type} {k : ℕ} (b : BoolTerm T k) : Bool

A classical term reads no function either.

Equations

• b.noFun = (TermIn.noFun b.args.1 && TermIn.noFun b.args.2)

def Selection.noFun {T : Type} {k : ℕ} : Selection T k → Bool

And a classical selection: the comparisons are the signature's predicates, which the minimal signature keeps; what it asks is that their arguments be columns and constants.

Equations

• (Selection.BT b).noFun = b.noFun
• φ.Not.noFun = φ.noFun
• (φ.And ψ).noFun = (φ.noFun && ψ.noFun)
• (φ.Or ψ).noFun = (φ.noFun && ψ.noFun)
• Selection.True.noFun = true

def Selection.noFunOpt {T : Type} {k : ℕ} : Option (Selection T k) → Bool

A clause, or none.

Equations

• Selection.noFunOpt none = true
• Selection.noFunOpt (some φ) = φ.noFun

def GenPredIn.noFun {T : Type} {c k : ℕ} {κ : Fin k → ColKind} : GenPredIn T c κ → Bool

A predicate of the general syntax: its comparisons are the signature's own, so what is asked is of their terms.

Equations

• (GenPredIn.cmp a t₁ t₂).noFun = (t₁.noFun && t₂.noFun)
• (GenPredIn.aggCmp k_1 a a_1 t).noFun = t.noFun
• (GenPredIn.aggRange k_1 a a_1 t₁ a_2 t₂).noFun = (t₁.noFun && t₂.noFun)
• (φ.and ψ).noFun = (φ.noFun && ψ.noFun)
• (φ.or ψ).noFun = (φ.noFun && ψ.noFun)
• φ.not.noFun = φ.noFun

def ProjColIn.noFun {T : Type} {c k : ℕ} {κ : Fin k → ColKind} : ProjColIn T c κ → Bool

An output column: a term of the signature, a token column carried through, or a term over an aggregate column. The rewritten world's column, which applies an arbitrary function, is in no signature.

Equations

• (ProjColIn.term t).noFun = t.noFun
• (ProjColIn.token k_1 a).noFun = true
• (ProjColIn.aggTerm k_1 a a_1).noFun = false
• (ProjColIn.aggTermOf k_1 a t).noFun = t.noFun
• (ProjColIn.provTerm t).noFun = t.noFun

def AggQueryIn.inSig {T : Type} [ValueType T] (Θ : Set (SeqAggFunc T)) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

The query is in the signature 𝒜(Ω, Θ), for Ω read as noFun – no function on values – and Θ the aggregates it may use. A second-level aggregation reads its group as a bag, so its outer aggregate is asked to be a symmetric member of Θ read that way (SeqAggFunc.onBag).

Three operators are False because they apply a function to values, which Ω does not hold: the two of the rewritten world fold the domain's + into their provenance column (ProvSum, GammaTok), and a multi-frame window combines its leaves by an arbitrary function – which is why SQL's distribution functions take their arithmetic as a parameter here. A frame with an offset bound moves the current row's value by + or - (FrameCond.noOff), so it is not in the signature either. So a value of the result of a query in the signature is a value of the instance, a constant of the query, or an aggregate of one of Θ, which is what the row of μ^⊎ reads.

Equations

• One or more equations did not get rendered due to their size.
• AggQueryIn.inSig Θ (AggQueryIn.Rel x✝ s') = True
• AggQueryIn.inSig Θ (AggQueryIn.Hole x✝¹ s x✝) = True
• AggQueryIn.inSig Θ (AggQueryIn.Param pv x✝) = True
• AggQueryIn.inSig Θ AggQueryIn.Empty = True
• AggQueryIn.inSig Θ (AggQueryIn.Proj ps q) = ((∀ (j : Fin x✝¹), (ps j).noFun = true) ∧ AggQueryIn.inSig Θ q)
• AggQueryIn.inSig Θ (AggQueryIn.Sel φ q hφ) = (φ.noFun = true ∧ AggQueryIn.inSig Θ q)
• AggQueryIn.inSig Θ (q₁.Prod q₂) = (AggQueryIn.inSig Θ q₁ ∧ AggQueryIn.inSig Θ q₂)
• AggQueryIn.inSig Θ (q₁.Apply q₂) = (AggQueryIn.inSig Θ q₁ ∧ AggQueryIn.inSig Θ q₂)
• AggQueryIn.inSig Θ (q₁.Sum q₂) = (AggQueryIn.inSig Θ q₁ ∧ AggQueryIn.inSig Θ q₂)
• AggQueryIn.inSig Θ q.Dedup = AggQueryIn.inSig Θ q
• AggQueryIn.inSig Θ (q₁.Diff q₂) = (AggQueryIn.inSig Θ q₁ ∧ AggQueryIn.inSig Θ q₂)
• AggQueryIn.inSig Θ (AggQueryIn.Explode k a q) = AggQueryIn.inSig Θ q
• AggQueryIn.inSig Θ (AggQueryIn.Mu s q₀ q₁) = (AggQueryIn.inSig Θ q₀ ∧ AggQueryIn.inSig Θ q₁)
• AggQueryIn.inSig Θ (AggQueryIn.MuSet s q₀ q₁) = (AggQueryIn.inSig Θ q₀ ∧ AggQueryIn.inSig Θ q₁)
• AggQueryIn.inSig Θ (AggQueryIn.GammaScalar ts fs q ord) = ((∀ (j : Fin x✝), (ts j).noFun = true) ∧ (∀ (j : Fin x✝), fs j ∈ Θ) ∧ AggQueryIn.inSig Θ q)
• AggQueryIn.inSig Θ (AggQueryIn.GammaNest is his p f q) = (p.noFun = true ∧ (∃ (g : SeqAggFunc T) (hg : g.Symmetric), g ∈ Θ ∧ f = g.onBag ⋯) ∧ AggQueryIn.inSig Θ q)
• AggQueryIn.inSig Θ (AggQueryIn.ProvSum is his t q) = False
• AggQueryIn.inSig Θ (AggQueryIn.Retag h q) = AggQueryIn.inSig Θ q
• AggQueryIn.inSig Θ (AggQueryIn.GammaTok is his ts fs a q keep) = False
• AggQueryIn.inSig Θ (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = False

def AggQueryIn.inMinimalSig {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (cnt : SeqAggFunc T) (q : AggQueryIn T c n κ l) : Prop

The minimal signature 𝒜(∅, {count}): no function on values, and one counting aggregate. The aggregate is a parameter with SeqAggFunc.Counts as its specification, as everywhere else in this file – count is a function of the value domain and not a fixed one.

Equations

• AggQueryIn.inMinimalSig cnt q = AggQueryIn.inSig {cnt} q

Counting rows: two facts the invariants run on

Union: the one operator that duplicates a row

Without ⊎, an instance whose relations hold at most one row has an answer of at most one row: a projection and a window map it row by row, a selection, duplicate elimination and a difference only remove, a product and an apply read one row of each side, and an aggregation emits one row per group – one group, here, or none.

def Database.Thin {T : Type} (D : Database T) : Prop

An instance no relation of which holds more than one row.

Equations

• D.Thin = ∀ (k : ℕ) (s : String) (r : Relation T k), Database.find k s D = some r → Multiset.card r ≤ 1

theorem AggQueryIn.card_le_one_of_thin {T : Type} [ValueType T] {S : Set OpKind} (hu : OpKind.union ∉ S) (hmb : OpKind.muBag ∉ S) (hms : OpKind.muSet ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : usesOnly S q → ∀ (D : Database T), D.Thin → ∀ (γ : Fin c → T), Multiset.card (q.evaluatePlain D γ) ≤ 1

Without ⊎, a thin instance has an answer of at most one row.

What a query reads of the instance

The set recursion's case of the invariant runs over the rounds, each read in the instance extended by the previous one, so two facts about what a query reads of an instance are needed first: that it reads it only through Database.find, and that a query naming nothing of the recursion is blind to the extension. The second is what bounds a count inside a recursion by a polynomial in the original instance – SQL forbids the recursive reference under an aggregation, which is what makes every count inside the body one over a query without it.

def AggQueryIn.leaves {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → List (ℕ × String)

The relations a query reads off the instance, each with the arity it reads it at: its leaves, less the one a body reads its own recursive name at – the name at the recursion's arity, which is bound. A leaf naming that name at another arity reads the instance and stays free.

Equations

• (AggQueryIn.Rel x✝ s).leaves = [(x✝, s)]
• (AggQueryIn.Hole x✝¹ s x✝).leaves = [(x✝¹, s)]
• (AggQueryIn.Param pv x✝).leaves = []
• AggQueryIn.Empty.leaves = []
• (AggQueryIn.Proj ps q).leaves = q.leaves
• (AggQueryIn.Sel φ q hφ).leaves = q.leaves
• (q₁.Prod q₂).leaves = q₁.leaves ++ q₂.leaves
• (q₁.Apply q₂).leaves = q₁.leaves ++ q₂.leaves
• (q₁.Sum q₂).leaves = q₁.leaves ++ q₂.leaves
• q.Dedup.leaves = q.leaves
• (q₁.Diff q₂).leaves = q₁.leaves ++ q₂.leaves
• (AggQueryIn.Explode k a q).leaves = q.leaves
• (AggQueryIn.Retag h q).leaves = q.leaves
• (AggQueryIn.Mu s q₀ q₁).leaves = q₀.leaves ++ List.filter (fun (p : ℕ × String) => decide (p ≠ (x✝¹, s))) q₁.leaves
• (AggQueryIn.MuSet s q₀ q₁).leaves = q₀.leaves ++ List.filter (fun (p : ℕ × String) => decide (p ≠ (x✝, s))) q₁.leaves
• (AggQueryIn.Gamma is ts fs q keep ord).leaves = q.leaves
• (AggQueryIn.GammaScalar ts fs q ord).leaves = q.leaves
• (AggQueryIn.GammaNest is his p f q).leaves = q.leaves
• (AggQueryIn.ProvSum is his t q).leaves = q.leaves
• (AggQueryIn.GammaTok is his ts fs a q keep).leaves = q.leaves
• (AggQueryIn.Win P O o w t f q a dist keep).leaves = q.leaves
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).leaves = q_1.leaves

@[reducible, inline]

abbrev Database.AgreeOff {T : Type} (s : String) (l : List (String × ℕ)) (D D' : Database T) : Prop

Two instances agreeing away from a name, the holes of a term excepted: what a hole reads is the round it stands for, which both instances hold alike.

Equations

• Database.AgreeOff s l D D' = ∀ (k : ℕ) (t : String), t ≠ s ∨ (t, k) ∈ l → Database.find k t D = Database.find k t D'

theorem AggQueryIn.evaluatePlain_assign_of_noMention {T : Type} [ValueType T] {s : String} {m : ℕ} (X : Relation T m) {c n : ℕ} {κ : Fin n → ColKind} (q : AggQueryIn T c n κ) (hq : noMention s q) (D : Database T) (γ : Fin c → T) : q.evaluatePlain (Database.assign s X D) γ = q.evaluatePlain D γ

And so it is blind to the recursion's own relation.

What SQL asks of a recursive term

WITH RECURSIVE restricts the recursive term: the self-reference may not appear under an aggregate or a window function, under DISTINCT, or in an EXCEPT (PostgreSQL refuses each of them, and the standard does too). AggQueryIn.recGuarded is that restriction, and the invariant needs it: a count inside a recursion whose input reads the recursive relation would grow with the rounds, and the values the rounds take would not close on a set the instance fixes. Under the restriction every count inside the body is over a query the recursion does not feed, so AggQueryIn.evaluatePlain_assign_of_noMention reads it off the instance the recursion started from.

The restriction SQL also carries – the self-reference occurring exactly once, and not in a subquery – is about termination and not about this, so it is not asked here.

def AggQueryIn.recGuarded {T : Type} (s : String) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

The recursive relation s occurs under no aggregation, window, duplicate elimination or difference.

Equations

• AggQueryIn.recGuarded s (AggQueryIn.Rel x✝ s') = True
• AggQueryIn.recGuarded s (AggQueryIn.Hole x✝¹ s_1 x✝) = True
• AggQueryIn.recGuarded s (AggQueryIn.Param pv x✝) = True
• AggQueryIn.recGuarded s AggQueryIn.Empty = True
• AggQueryIn.recGuarded s (AggQueryIn.Proj ps q) = AggQueryIn.recGuarded s q
• AggQueryIn.recGuarded s (AggQueryIn.Sel φ q hφ) = AggQueryIn.recGuarded s q
• AggQueryIn.recGuarded s (q₁.Prod q₂) = (AggQueryIn.recGuarded s q₁ ∧ AggQueryIn.recGuarded s q₂)
• AggQueryIn.recGuarded s (q₁.Apply q₂) = (AggQueryIn.recGuarded s q₁ ∧ AggQueryIn.recGuarded s q₂)
• AggQueryIn.recGuarded s (q₁.Sum q₂) = (AggQueryIn.recGuarded s q₁ ∧ AggQueryIn.recGuarded s q₂)
• AggQueryIn.recGuarded s q.Dedup = AggQueryIn.noMention s q
• AggQueryIn.recGuarded s (q₁.Diff q₂) = (AggQueryIn.noMention s q₁ ∧ AggQueryIn.noMention s q₂)
• AggQueryIn.recGuarded s (AggQueryIn.Explode k a q) = AggQueryIn.recGuarded s q
• AggQueryIn.recGuarded s (AggQueryIn.Mu s_1 q₀ q₁) = (AggQueryIn.recGuarded s q₀ ∧ AggQueryIn.recGuarded s q₁)
• AggQueryIn.recGuarded s (AggQueryIn.MuSet s_1 q₀ q₁) = (AggQueryIn.recGuarded s q₀ ∧ AggQueryIn.recGuarded s q₁)
• AggQueryIn.recGuarded s (AggQueryIn.Gamma is ts fs q keep ord) = AggQueryIn.noMention s q
• AggQueryIn.recGuarded s (AggQueryIn.GammaScalar ts fs q ord) = AggQueryIn.noMention s q
• AggQueryIn.recGuarded s (AggQueryIn.GammaNest is his p f q) = AggQueryIn.noMention s q
• AggQueryIn.recGuarded s (AggQueryIn.ProvSum is his t q) = AggQueryIn.noMention s q
• AggQueryIn.recGuarded s (AggQueryIn.Retag h q) = AggQueryIn.recGuarded s q
• AggQueryIn.recGuarded s (AggQueryIn.GammaTok is his ts fs a q keep) = AggQueryIn.noMention s q
• AggQueryIn.recGuarded s (AggQueryIn.Win P O o w t f q a dist keep) = AggQueryIn.noMention s q
• AggQueryIn.recGuarded s (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = AggQueryIn.noMention s q_1

How a recursive term may read the recursive relation

The plain syntax restricts a recursion: in μR.(q₀, q₁) the base q₀ does not read R, and in the body q₁ the name R occurs once, and only under a projection, a selection on regular columns, either side of a product, the left side of an apply, or a union. That is narrower than the Lean's syntax, which lets a recursion be written with the name anywhere, and narrower than AggQueryIn.recGuarded – which only keeps R out of an aggregation, a window, a duplicate elimination and a difference. The results about bases of the whole algebra (Provenance.RecursionBasisTheorem) are stated against this restriction, so it is what such a result asks of a query.

What it gives for free is AggQueryIn.recGuarded: the operators a recursive term may read R under are none of the four the weaker restriction keeps it out of, so everything proved there applies. What it does not give is one storey of recursion – the other side of a product, and an apply's right side, are arbitrary queries that do not read R, and either may be a recursion of its own. So a body is not recursion-free, and the value analysis has to reach those sub-recursions through the outer induction (AggQueryIn.exists_polyBound_rec).

Explode and Retag are on the list here though they are not SQL operators: they are the kind discipline's two operators, identities on plain relations, so they move no value and read no column.

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

Every recursion of the query is hygienic: neither its base nor its term names the bound relation freely. The typing of the holes says the rest – that the term reads the relation once and only where it may – and a query over a schema is hygienic (AggQueryIn.hygienic_of_overSchema), the schema not declaring a bound name; what the predicate carries is the semantic condition the evaluator's binding of the name needs.

Equations

• (AggQueryIn.Rel x✝ s').hygienic = True
• (AggQueryIn.Hole x✝¹ s x✝).hygienic = True
• (AggQueryIn.Param pv x✝).hygienic = True
• AggQueryIn.Empty.hygienic = True
• (AggQueryIn.Proj ps q).hygienic = q.hygienic
• (AggQueryIn.Sel φ q hφ).hygienic = q.hygienic
• (q₁.Prod q₂).hygienic = (q₁.hygienic ∧ q₂.hygienic)
• (q₁.Apply q₂).hygienic = (q₁.hygienic ∧ q₂.hygienic)
• (q₁.Sum q₂).hygienic = (q₁.hygienic ∧ q₂.hygienic)
• q.Dedup.hygienic = q.hygienic
• (q₁.Diff q₂).hygienic = (q₁.hygienic ∧ q₂.hygienic)
• (AggQueryIn.Explode k a q).hygienic = q.hygienic
• (AggQueryIn.Mu s q₀ q₁).hygienic = (AggQueryIn.noMention s q₀ ∧ AggQueryIn.noMention s q₁ ∧ q₀.hygienic ∧ q₁.hygienic)
• (AggQueryIn.MuSet s q₀ q₁).hygienic = (AggQueryIn.noMention s q₀ ∧ AggQueryIn.noMention s q₁ ∧ q₀.hygienic ∧ q₁.hygienic)
• (AggQueryIn.Gamma is ts fs q keep ord).hygienic = q.hygienic
• (AggQueryIn.GammaScalar ts fs q ord).hygienic = q.hygienic
• (AggQueryIn.GammaNest is his p f q).hygienic = q.hygienic
• (AggQueryIn.ProvSum is his t q).hygienic = q.hygienic
• (AggQueryIn.Retag h q).hygienic = q.hygienic
• (AggQueryIn.GammaTok is his ts fs a q keep).hygienic = q.hygienic
• (AggQueryIn.Win P O o w t f q a dist keep).hygienic = q.hygienic
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).hygienic = q_1.hygienic

The constants a query may put in its result

def TermIn.constsIn {T : Type} {c k : ℕ} (V : Finset T) : TermIn T c k → Prop

The constants of a term lie in V.

Equations

• TermIn.constsIn V (TermIn.const a) = (a ∈ V)
• TermIn.constsIn V (TermIn.outer a) = True
• TermIn.constsIn V #a = True
• TermIn.constsIn V (a.add a_1) = (TermIn.constsIn V a ∧ TermIn.constsIn V a_1)
• TermIn.constsIn V (a.sub a_1) = (TermIn.constsIn V a ∧ TermIn.constsIn V a_1)
• TermIn.constsIn V (a.mul a_1) = (TermIn.constsIn V a ∧ TermIn.constsIn V a_1)
• TermIn.constsIn V (TermIn.caseWhen a a_1 a_2 a_3 a_4) = (TermIn.constsIn V a_1 ∧ TermIn.constsIn V a_2 ∧ TermIn.constsIn V a_3 ∧ TermIn.constsIn V a_4)
• TermIn.constsIn V (a.coalesce a_1) = (TermIn.constsIn V a ∧ TermIn.constsIn V a_1)

def TermGIn.constsIn {T : Type} {c k : ℕ} {κ : Fin k → ColKind} (V : Finset T) : TermGIn T c κ → Prop

And of a kind-indexed term.

Equations

• TermGIn.constsIn V (TermGIn.const a) = (a ∈ V)
• TermGIn.constsIn V (TermGIn.outer a) = True
• TermGIn.constsIn V (TermGIn.index k_1 a) = True
• TermGIn.constsIn V (TermGIn.provIndex k_1 a) = True
• TermGIn.constsIn V (TermGIn.cmpAgg k_1 a a_1 a_2) = TermGIn.constsIn V a_2
• TermGIn.constsIn V (TermGIn.chiGate a a_1 a_2) = (TermGIn.constsIn V a_1 ∧ TermGIn.constsIn V a_2)
• TermGIn.constsIn V (a.add a_1) = (TermGIn.constsIn V a ∧ TermGIn.constsIn V a_1)
• TermGIn.constsIn V (a.sub a_1) = (TermGIn.constsIn V a ∧ TermGIn.constsIn V a_1)
• TermGIn.constsIn V (a.mul a_1) = (TermGIn.constsIn V a ∧ TermGIn.constsIn V a_1)
• TermGIn.constsIn V (TermGIn.caseWhen a a_1 a_2 a_3 a_4) = (TermGIn.constsIn V a_1 ∧ TermGIn.constsIn V a_2 ∧ TermGIn.constsIn V a_3 ∧ TermGIn.constsIn V a_4)
• TermGIn.constsIn V (a.coalesce a_1) = (TermGIn.constsIn V a ∧ TermGIn.constsIn V a_1)

def ProjColIn.constsIn {T : Type} {c k : ℕ} {κ : Fin k → ColKind} (V : Finset T) : ProjColIn T c κ → Prop

And of an output column.

Equations

• ProjColIn.constsIn V (ProjColIn.term t) = TermGIn.constsIn V t
• ProjColIn.constsIn V (ProjColIn.token k_1 a) = True
• ProjColIn.constsIn V (ProjColIn.aggTerm k_1 a a_1) = True
• ProjColIn.constsIn V (ProjColIn.aggTermOf k_1 a t) = TermIn.constsIn V t
• ProjColIn.constsIn V (ProjColIn.provTerm t) = TermGIn.constsIn V t

def AggQueryIn.constsIn {T : Type} (V : Finset T) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

The constants the query may put in its result lie in V. Only a projection's columns are asked: the terms an aggregate reads feed a count, whose value is a function of how many values it reads and not of which, so their constants do not reach the result.

Equations

• AggQueryIn.constsIn V (AggQueryIn.Rel x✝ s') = True
• AggQueryIn.constsIn V (AggQueryIn.Hole x✝¹ s x✝) = True
• AggQueryIn.constsIn V (AggQueryIn.Param pv x✝) = ∀ (k : Fin x✝¹) (a : T), pv k = Sum.inl a → a ∈ V
• AggQueryIn.constsIn V AggQueryIn.Empty = True
• AggQueryIn.constsIn V (AggQueryIn.Proj ps q) = ((∀ (j : Fin x✝¹), ProjColIn.constsIn V (ps j)) ∧ AggQueryIn.constsIn V q)
• AggQueryIn.constsIn V (AggQueryIn.Sel φ q hφ) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (q₁.Prod q₂) = (AggQueryIn.constsIn V q₁ ∧ AggQueryIn.constsIn V q₂)
• AggQueryIn.constsIn V (q₁.Apply q₂) = (AggQueryIn.constsIn V q₁ ∧ AggQueryIn.constsIn V q₂)
• AggQueryIn.constsIn V (q₁.Sum q₂) = (AggQueryIn.constsIn V q₁ ∧ AggQueryIn.constsIn V q₂)
• AggQueryIn.constsIn V q.Dedup = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (q₁.Diff q₂) = (AggQueryIn.constsIn V q₁ ∧ AggQueryIn.constsIn V q₂)
• AggQueryIn.constsIn V (AggQueryIn.Explode k a q) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.Mu s q₀ q₁) = (AggQueryIn.constsIn V q₀ ∧ AggQueryIn.constsIn V q₁)
• AggQueryIn.constsIn V (AggQueryIn.MuSet s q₀ q₁) = (AggQueryIn.constsIn V q₀ ∧ AggQueryIn.constsIn V q₁)
• AggQueryIn.constsIn V (AggQueryIn.Gamma is ts fs q keep ord) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.GammaScalar ts fs q ord) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.GammaNest is his p f q) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.ProvSum is his t q) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.Retag h q) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.GammaTok is his ts fs a q keep) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.Win P O o w t f q a dist keep) = AggQueryIn.constsIn V q
• AggQueryIn.constsIn V (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = AggQueryIn.constsIn V q_1

def TermIn.consts {T : Type} [ValueType T] {c k : ℕ} : TermIn T c k → Finset T

The constants a term names, as a set.

Equations

• (TermIn.const a).consts = {a}
• (TermIn.outer a).consts = ∅
• (#a).consts = ∅
• (a.add a_1).consts = a.consts ∪ a_1.consts
• (a.sub a_1).consts = a.consts ∪ a_1.consts
• (a.mul a_1).consts = a.consts ∪ a_1.consts
• (TermIn.caseWhen a a_1 a_2 a_3 a_4).consts = a_1.consts ∪ a_2.consts ∪ a_3.consts ∪ a_4.consts
• (a.coalesce a_1).consts = a.consts ∪ a_1.consts

def TermGIn.consts {T : Type} [ValueType T] {c k : ℕ} {κ : Fin k → ColKind} : TermGIn T c κ → Finset T

And a kind-indexed term's.

Equations

• (TermGIn.const a).consts = {a}
• (TermGIn.outer a).consts = ∅
• (TermGIn.index k_1 a).consts = ∅
• (TermGIn.provIndex k_1 a).consts = ∅
• (TermGIn.cmpAgg k_1 a a_1 a_2).consts = a_2.consts
• (TermGIn.chiGate a a_1 a_2).consts = a_1.consts ∪ a_2.consts
• (a.add a_1).consts = a.consts ∪ a_1.consts
• (a.sub a_1).consts = a.consts ∪ a_1.consts
• (a.mul a_1).consts = a.consts ∪ a_1.consts
• (TermGIn.caseWhen a a_1 a_2 a_3 a_4).consts = a_1.consts ∪ a_2.consts ∪ a_3.consts ∪ a_4.consts
• (a.coalesce a_1).consts = a.consts ∪ a_1.consts

def ProjColIn.consts {T : Type} [ValueType T] {c k : ℕ} {κ : Fin k → ColKind} : ProjColIn T c κ → Finset T

And an output column's.

Equations

• (ProjColIn.term t).consts = t.consts
• (ProjColIn.token k_1 a).consts = ∅
• (ProjColIn.aggTerm k_1 a a_1).consts = ∅
• (ProjColIn.aggTermOf k_1 a t).consts = t.consts
• (ProjColIn.provTerm t).consts = t.consts

def AggQueryIn.consts {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Finset T

The constants a query names in its projections, as a set: what the value of a row of a recursion-free, function-free query can draw on beside the instance and the context.

Equations

• (AggQueryIn.Rel x✝ s').consts = ∅
• (AggQueryIn.Hole x✝¹ s x✝).consts = ∅
• (AggQueryIn.Param pv x✝).consts = Finset.univ.biUnion fun (k : Fin x✝¹) => Sum.elim (fun (a : T) => {a}) (fun (x : Fin x✝²) => ∅) (pv k)
• AggQueryIn.Empty.consts = ∅
• (AggQueryIn.Proj ps q).consts = (Finset.univ.biUnion fun (j : Fin x✝¹) => (ps j).consts) ∪ q.consts
• (AggQueryIn.Sel φ q hφ).consts = q.consts
• (q₁.Prod q₂).consts = q₁.consts ∪ q₂.consts
• (q₁.Apply q₂).consts = q₁.consts ∪ q₂.consts
• (q₁.Sum q₂).consts = q₁.consts ∪ q₂.consts
• q.Dedup.consts = q.consts
• (q₁.Diff q₂).consts = q₁.consts ∪ q₂.consts
• (AggQueryIn.Explode k a q).consts = q.consts
• (AggQueryIn.Mu s q₀ q₁).consts = q₀.consts ∪ q₁.consts
• (AggQueryIn.MuSet s q₀ q₁).consts = q₀.consts ∪ q₁.consts
• (AggQueryIn.Gamma is ts fs q keep ord).consts = q.consts
• (AggQueryIn.GammaScalar ts fs q ord).consts = q.consts
• (AggQueryIn.GammaNest is his p f q).consts = q.consts
• (AggQueryIn.ProvSum is his t q).consts = q.consts
• (AggQueryIn.Retag h q).consts = q.consts
• (AggQueryIn.GammaTok is his ts fs a q keep).consts = q.consts
• (AggQueryIn.Win P O o w t f q a dist keep).consts = q.consts
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).consts = q_1.consts

Where a query is defined

A recursion means the value its rounds settle at and nothing where they do not, so a query with a recursion is a partial function of the instance. SettlesAt says the evaluation at one instance runs only recursions that settle: at Mu, the round function vanishes on the empty round and the rounds from the base reach an empty one; at MuSet, the iterations from 0 repeat; and the subqueries settle at the instances the evaluation reads them at – a body at every round, an apply's right side at every row of its left. This is AggQueryIn.recSettles taken instance by instance and in the plain semantics: that predicate asks every instance, which a nested recursion needs, but a result about a class of queries has to speak of the instances where a query is defined, since a recursion that is total is the exception (the body reads the recursive name under a product with an instance relation, and a cycle in that relation keeps the rounds going). A query with no recursion settles everywhere.

def AggQueryIn.SettlesAt {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Database T → (Fin c → T) → Prop

The recursions settle at an instance.

Equations

• One or more equations did not get rendered due to their size.
• (AggQueryIn.Rel x✝² a).SettlesAt x✝¹ x✝ = True
• (AggQueryIn.Hole x✝³ s x✝²).SettlesAt x✝¹ x✝ = True
• (AggQueryIn.Param pv x✝²).SettlesAt x✝¹ x✝ = True
• AggQueryIn.Empty.SettlesAt x✝¹ x✝ = True
• (AggQueryIn.Proj ps q).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.Sel φ q hφ).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (q₁.Prod q₂).SettlesAt x✝¹ x✝ = (q₁.SettlesAt x✝¹ x✝ ∧ q₂.SettlesAt x✝¹ x✝)
• (q₁.Apply q₂).SettlesAt x✝¹ x✝ = (q₁.SettlesAt x✝¹ x✝ ∧ ∀ (u : Tuple T n₁), Multiset.Mem (q₁.evaluatePlain x✝¹ x✝) u → q₂.SettlesAt x✝¹ (Fin.append u x✝))
• (q₁.Sum q₂).SettlesAt x✝¹ x✝ = (q₁.SettlesAt x✝¹ x✝ ∧ q₂.SettlesAt x✝¹ x✝)
• q.Dedup.SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (q₁.Diff q₂).SettlesAt x✝¹ x✝ = (q₁.SettlesAt x✝¹ x✝ ∧ q₂.SettlesAt x✝¹ x✝)
• (AggQueryIn.Explode k a q).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.Retag h q).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.Gamma is ts fs q keep ord).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.GammaScalar ts fs q ord).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.GammaNest is his p f q).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.GammaTok is his ts fs a q keep).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.ProvSum is his t q).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.Win P O o w t f q a dist keep).SettlesAt x✝¹ x✝ = q.SettlesAt x✝¹ x✝
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).SettlesAt x✝¹ x✝ = q_1.SettlesAt x✝¹ x✝

noncomputable def AggQueryIn.evaluatePlain? {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) (D : Database T) (γ : Fin c → T) : Option (Relation T n)

The partial semantics: the plain reading where the query is defined, and nothing where it is not. This is what a query of the whole algebra denotes; evaluatePlain is its total extension by a junk value where a recursion never settles.

Equations

• q.evaluatePlain? D γ = if q.SettlesAt D γ then some (q.evaluatePlain D γ) else none

def AggQueryIn.Extends {T : Type} [ValueType T] {c n : ℕ} {κ κ' : Fin n → ColKind} {l l' : List (String × ℕ)} (q' : AggQueryIn T c n κ' l') (q : AggQueryIn T c n κ l) : Prop

q' extends q as a partial function: wherever q is defined, q' is defined with the same value. This is what a rewriting of the whole algebra establishes; extends_iff_settles spells it out through the evaluator and the settling.

Equations

• q'.Extends q = ∀ (D : Database T) (γ : Fin c → T) (r : Relation T n), q.evaluatePlain? D γ = some r → q'.evaluatePlain? D γ = some r

What the two fixpoints are when their rounds vanish or do not

Selection and difference: the two operators that can lose a row

Without σ and −, a query is either empty on every instance of its schema, or non-empty on every instance of it whose relations are all non-empty: nothing else can turn rows away. The disjunction is uniform in the outer context, which is what the apply needs – without a selection the outer row enters its right side only through terms, and a term decides no row's presence.

The two recursions keep the invariant, under the one hypothesis that makes them mean anything (SettlesAt), but not by an induction on the disjunction alone: whether μ^∪R.(q₀, q₁) is empty depends on whether q₁ is empty at the instance binding R to the empty relation, which is not a full instance of the body's schema, so the body's disjunction says nothing about it. What the induction carries instead is the disjunction relative to a set E of names forced empty (AggQueryIn.NonzeroOn): q is non-empty on every instance that is full off E, or empty on every instance that is empty on E. At a set recursion, the first round reads the body with the recursive name in E, and the later rounds read it with the name out of E – which the body's condition at the larger set implies (NonzeroOn.mono), the condition being antitone in E. At a bag recursion the base is a summand of the answer, so the base decides; the rounds from an empty base vanish because the round function vanishes on the empty round, which is what SettlesAt asks there.

def Database.Full {T : Type} (sch : Schema) (D : Database T) : Prop

An instance of the schema no relation of which is empty.

Equations

• Database.Full sch D = ∀ (s : String) (k : ℕ), sch.decl s = some k → ∃ (r : Relation T k), Database.find k s D = some r ∧ r ≠ 0

def Database.FullOff {T : Type} (sch : Schema) (E : Set String) (D : Database T) : Prop

An instance full off a set of names: every relation the schema declares under a name outside E is bound and non-empty. Full is the case E = ∅.

Equations

• Database.FullOff sch E D = ∀ (s : String) (k : ℕ), sch.decl s = some k → s ∉ E → ∃ (r : Relation T k), Database.find k s D = some r ∧ r ≠ 0

def Database.EmptyOn {T : Type} (sch : Schema) (E : Set String) (D : Database T) : Prop

An instance empty on a set of names: whatever is bound under a name of E, at the arity the schema declares it, is the empty relation.

Equations

• Database.EmptyOn sch E D = ∀ (s : String) (k : ℕ) (r : Relation T k), sch.decl s = some k → s ∈ E → Database.find k s D = some r → r = 0

def AggQueryIn.NonzeroOn {T : Type} (E : Set String) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Prop

Where a query without σ and − is non-empty, read off its syntax relative to a set E of names forced empty: a relation name is non-empty unless it is in E; ∅ never; the one-input operators and the aggregations inherit, the scalar aggregation always; a product and an apply need both sides, a union one; a bag recursion is its base; a set recursion is its base or its body at the instance binding the recursive name to the empty relation. The two lemmas below say that this is right: q.NonzeroOn E makes q non-empty on every instance full off E, and its negation makes q empty on every instance empty on E. The selection, the difference and the two operators of the rewritten world get the value that keeps the lemmas uniform; they are never reached.

Equations

• AggQueryIn.NonzeroOn E (AggQueryIn.Rel x✝ a) = (a ∉ E)
• AggQueryIn.NonzeroOn E (AggQueryIn.Hole x✝¹ s x✝) = (s ∉ E)
• AggQueryIn.NonzeroOn E (AggQueryIn.Param pv x✝) = True
• AggQueryIn.NonzeroOn E AggQueryIn.Empty = False
• AggQueryIn.NonzeroOn E (AggQueryIn.Proj ps q) = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (AggQueryIn.Sel φ q hφ) = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (q₁.Prod q₂) = (AggQueryIn.NonzeroOn E q₁ ∧ AggQueryIn.NonzeroOn E q₂)
• AggQueryIn.NonzeroOn E (q₁.Apply q₂) = (AggQueryIn.NonzeroOn E q₁ ∧ AggQueryIn.NonzeroOn E q₂)
• AggQueryIn.NonzeroOn E (q₁.Sum q₂) = (AggQueryIn.NonzeroOn E q₁ ∨ AggQueryIn.NonzeroOn E q₂)
• AggQueryIn.NonzeroOn E q.Dedup = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (q₁.Diff q₂) = AggQueryIn.NonzeroOn E q₁
• AggQueryIn.NonzeroOn E (AggQueryIn.Explode k a q) = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (AggQueryIn.Retag h q) = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (AggQueryIn.Mu s q₀ q₁) = AggQueryIn.NonzeroOn E q₀
• AggQueryIn.NonzeroOn E (AggQueryIn.MuSet s q₀ q₁) = (AggQueryIn.NonzeroOn E q₀ ∨ AggQueryIn.NonzeroOn (insert s E) q₁)
• AggQueryIn.NonzeroOn E (AggQueryIn.Gamma is ts fs q keep ord) = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (AggQueryIn.GammaScalar ts fs q ord) = True
• AggQueryIn.NonzeroOn E (AggQueryIn.GammaNest is his p f q) = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (AggQueryIn.GammaTok is his ts fs a a_1 keep) = AggQueryIn.NonzeroOn E a_1
• AggQueryIn.NonzeroOn E (AggQueryIn.ProvSum is his t a) = AggQueryIn.NonzeroOn E a
• AggQueryIn.NonzeroOn E (AggQueryIn.Win P O o w t f q a dist keep) = AggQueryIn.NonzeroOn E q
• AggQueryIn.NonzeroOn E (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps) = AggQueryIn.NonzeroOn E q_1

theorem AggQueryIn.zero_or_ne_zero_of_noSelDiff {T : Type} [ValueType T] {S : Set OpKind} (hsel : OpKind.sel ∉ S) (hdiff : OpKind.diff ∉ S) {sch : Schema} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) (hq : usesOnly S q) (hw : overSchema sch q) : (∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → q.evaluatePlain D γ = 0) ∨ ∀ (D : Database T) (γ : Fin c → T), Database.Full sch D → q.SettlesAt D γ → q.evaluatePlain D γ ≠ 0

Without σ and −, a query is empty everywhere or non-empty on every full instance, wherever it is defined – the recursions included, NonzeroOn ∅ deciding which.

def schemaR : Schema

The schema of one unary relation, for the witnesses below.

Equations

• schemaR = Schema.ofFn (fun (s : String) => if s = "R" then some 1 else none) {"R"} schemaR._proof_2

def dOne : Database ℕ

An instance of it holding the row (1).

Equations

• dOne = [("R", ⟨1, {![1]}⟩)]

def dZero : Database ℕ

And one holding the row (0).

Equations

• dZero = [("R", ⟨1, {![0]}⟩)]

def selWitness : AggQuery ℕ 1 (ColKind.allReg 1)

σ_{#0 = 1}(R), the witness of the selection row.

Equations

• selWitness = AggQueryIn.Sel (GenPredIn.cmp CompOp.eq (TermGIn.index 0 selWitness._proof_3) (TermGIn.const 1)) (AggQueryIn.Rel 1 "R") selWitness._proof_1

Product and apply: the two operators that multiply

Without them an answer grows linearly in the instance: a projection, a selection, a window, duplicate elimination, a difference and an aggregation each give at most as many rows as they read, and a union adds two such bounds. The + 1 is there for the scalar aggregation, whose row is there even on the empty instance.

def Database.size {T : Type} (D : Database T) : ℕ

The number of rows an instance holds.

Equations

• D.size = (List.map (fun (e : String × (n : ℕ) × Relation T n) => Multiset.card e.2.snd) D).sum

def recBound (c n K : ℕ) : ℕ

The number of rounds a recursion of the minimal signature can run before the orbits of its rows repeat: the size of a row box (below), plus two.

Equations

• recBound c n K = (n + c + K) ^ n + 2

def AggQueryIn.sizeBound {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → ℕ

The bound a query gives on its answer's size, per row of the instance.

Equations

• (AggQueryIn.Rel x✝ a).sizeBound = 1
• (AggQueryIn.Hole x✝¹ s x✝).sizeBound = 1
• (AggQueryIn.Param pv x✝).sizeBound = 1
• AggQueryIn.Empty.sizeBound = 0
• (AggQueryIn.Proj ps q).sizeBound = q.sizeBound
• (AggQueryIn.Sel φ q hφ).sizeBound = q.sizeBound
• (q₁.Prod q₂).sizeBound = 0
• (q₁.Apply q₂).sizeBound = 0
• (q₁.Sum q₂).sizeBound = q₁.sizeBound + q₂.sizeBound
• q.Dedup.sizeBound = q.sizeBound
• (q₁.Diff q₂).sizeBound = q₁.sizeBound
• (AggQueryIn.Explode k a q).sizeBound = q.sizeBound
• (AggQueryIn.Retag h q).sizeBound = q.sizeBound
• (AggQueryIn.Mu s q₀ q₁).sizeBound = recBound x✝² x✝¹ q₁.consts.card * q₀.sizeBound
• (AggQueryIn.MuSet s q₀ q₁).sizeBound = recBound x✝¹ x✝ q₁.consts.card * (q₀.sizeBound + q₁.sizeBound)
• (AggQueryIn.Gamma is ts fs q keep ord).sizeBound = q.sizeBound
• (AggQueryIn.GammaScalar ts fs q ord).sizeBound = 1
• (AggQueryIn.GammaNest is his p f q).sizeBound = q.sizeBound
• (AggQueryIn.GammaTok is his ts fs a a_1 keep).sizeBound = a_1.sizeBound
• (AggQueryIn.ProvSum is his t a).sizeBound = a.sizeBound
• (AggQueryIn.Win P O o w t f q a dist keep).sizeBound = q.sizeBound
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).sizeBound = q_1.sizeBound

A recursive term without × and the apply reads the previous round row by row

What the product row needs of a recursion is a bound on the number of rounds a bag recursion can run before its rounds are empty, and on the rows a set recursion can accumulate. Without × and the apply, a recursive term in the minimal signature maps each row of the previous round to at most one row – a projection reads a row as columns, context values and constants, a selection keeps or drops it – and adds rows that read no round. So each row of the base follows an orbit under one function f on rows; and in the minimal signature that orbit stays inside the rows built from the row's own values, the context's and the query's constants, a set of a size the query fixes. An orbit longer than that repeats, and a repeating orbit never ends: so a bag recursion that settles does so within that many rounds, and a set recursion's rows are the first that many points of the orbits of its base rows. Both bounds fail with arithmetic (Π_{x+1} has an orbit as long as the instance wants), which is why the row is about the minimal signature.

def optIter {α : Type} (f : α → Option α) : ℕ → α → Option α

The iterates of a partial function: optIter f j a is f applied j times to a, or none once an application has failed.

Equations

• optIter f 0 = some
• optIter f j.succ = fun (a : α) => (optIter f j a).bind f

theorem optIter_exists_lt {α : Type} [DecidableEq α] {f : α → Option α} (S : Finset α) (hS : ∀ b ∈ S, ∀ (c : α), f b = some c → c ∈ S) {a : α} (ha : a ∈ S) (j : ℕ) : ∃ j' < S.card + 2, optIter f j' a = optIter f j a

Every point of such an orbit is one of its first k + 2 points.

theorem optIter_ne_none {α : Type} [DecidableEq α] {f : α → Option α} (S : Finset α) (hS : ∀ b ∈ S, ∀ (c : α), f b = some c → c ∈ S) {a : α} (ha : a ∈ S) (h : optIter f (S.card + 1) a ≠ none) (j : ℕ) : optIter f j a ≠ none

An orbit alive at point k + 1 never ends.

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

Every projection column of the query applies no function to values – the half of inSig the recursion bounds read, a term being a column, a context value or a constant.

Equations

• (AggQueryIn.Rel x✝ s').noFunCols = True
• (AggQueryIn.Hole x✝¹ s x✝).noFunCols = True
• (AggQueryIn.Param pv x✝).noFunCols = True
• AggQueryIn.Empty.noFunCols = True
• (AggQueryIn.Proj ps q).noFunCols = ((∀ (j : Fin x✝¹), (ps j).noFun = true) ∧ q.noFunCols)
• (AggQueryIn.Sel φ q hφ).noFunCols = q.noFunCols
• (q₁.Prod q₂).noFunCols = (q₁.noFunCols ∧ q₂.noFunCols)
• (q₁.Apply q₂).noFunCols = (q₁.noFunCols ∧ q₂.noFunCols)
• (q₁.Sum q₂).noFunCols = (q₁.noFunCols ∧ q₂.noFunCols)
• q.Dedup.noFunCols = q.noFunCols
• (q₁.Diff q₂).noFunCols = (q₁.noFunCols ∧ q₂.noFunCols)
• (AggQueryIn.Explode k a q).noFunCols = q.noFunCols
• (AggQueryIn.Mu s q₀ q₁).noFunCols = (q₀.noFunCols ∧ q₁.noFunCols)
• (AggQueryIn.MuSet s q₀ q₁).noFunCols = (q₀.noFunCols ∧ q₁.noFunCols)
• (AggQueryIn.Gamma is ts fs q keep ord).noFunCols = q.noFunCols
• (AggQueryIn.GammaScalar ts fs q ord).noFunCols = q.noFunCols
• (AggQueryIn.GammaNest is his p f q).noFunCols = q.noFunCols
• (AggQueryIn.ProvSum is his t q).noFunCols = q.noFunCols
• (AggQueryIn.Retag h q).noFunCols = q.noFunCols
• (AggQueryIn.GammaTok is his ts fs a q keep).noFunCols = q.noFunCols
• (AggQueryIn.Win P O o w t f q a dist keep).noFunCols = q.noFunCols
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).noFunCols = q_1.noFunCols

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

Every recursive term of the query applies no function to values. This is what the product row asks of a recursion: the bound on its rounds is a bound on the orbit of a row under a term that can only copy values, and it is the one place the signature enters the rows. A query of a signature satisfies it (recNoFun_of_inSig), and so does a recursion-free query (recNoFun_of_usesOnly).

Equations

• (AggQueryIn.Rel x✝ s').recNoFun = True
• (AggQueryIn.Hole x✝¹ s x✝).recNoFun = True
• (AggQueryIn.Param pv x✝).recNoFun = True
• AggQueryIn.Empty.recNoFun = True
• (AggQueryIn.Proj ps q).recNoFun = q.recNoFun
• (AggQueryIn.Sel φ q hφ).recNoFun = q.recNoFun
• (q₁.Prod q₂).recNoFun = (q₁.recNoFun ∧ q₂.recNoFun)
• (q₁.Apply q₂).recNoFun = (q₁.recNoFun ∧ q₂.recNoFun)
• (q₁.Sum q₂).recNoFun = (q₁.recNoFun ∧ q₂.recNoFun)
• q.Dedup.recNoFun = q.recNoFun
• (q₁.Diff q₂).recNoFun = (q₁.recNoFun ∧ q₂.recNoFun)
• (AggQueryIn.Explode k a q).recNoFun = q.recNoFun
• (AggQueryIn.Mu s q₀ q₁).recNoFun = (q₁.noFunCols ∧ q₀.recNoFun ∧ q₁.recNoFun)
• (AggQueryIn.MuSet s q₀ q₁).recNoFun = (q₁.noFunCols ∧ q₀.recNoFun ∧ q₁.recNoFun)
• (AggQueryIn.Gamma is ts fs q keep ord).recNoFun = q.recNoFun
• (AggQueryIn.GammaScalar ts fs q ord).recNoFun = q.recNoFun
• (AggQueryIn.GammaNest is his p f q).recNoFun = q.recNoFun
• (AggQueryIn.ProvSum is his t q).recNoFun = q.recNoFun
• (AggQueryIn.Retag h q).recNoFun = q.recNoFun
• (AggQueryIn.GammaTok is his ts fs a q keep).recNoFun = q.recNoFun
• (AggQueryIn.Win P O o w t f q a dist keep).recNoFun = q.recNoFun
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).recNoFun = q_1.recNoFun

def rowVals {T : Type} [ValueType T] {c n : ℕ} (u : Tuple T n) (γ : Fin c → T) (K : Finset T) : Finset T

The values a row of a recursive term may draw on: the row it comes from, the context, and the term's constants.

Equations

• rowVals u γ K = Finset.image u Finset.univ ∪ Finset.image γ Finset.univ ∪ K

theorem AggQueryIn.pointwise_of_body {T : Type} [ValueType T] {S : Set OpKind} (hp : OpKind.prod ∉ S) (ha : OpKind.apply ∉ S) {s : String} {m c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : l = [(s, m)] → usesOnly S q → noMention s q → q.noFunCols → ∀ (D : Database T) (γ : Fin c → T), ∃ (f : Tuple T m → Option (Tuple T n)) (C : Multiset (Tuple T n)), (∀ (X : Multiset (Tuple T m)), q.evaluatePlain (Database.assign s X D) γ = Multiset.filterMap f X + C) ∧ ∀ (v : Tuple T m) (w : Tuple T n), f v = some w → ∀ (i : Fin n), w i ∈ rowVals v γ q.consts

Without × and the apply, a recursive term of the minimal signature reads the recursive relation row by row: its rows are the rows f u of the rows u of the relation, f a partial function, and rows C that read nothing of it; and the values of f u are values of u, of the context, or constants of the term.

def rowBox {T : Type} [ValueType T] {c n : ℕ} (u : Tuple T n) (γ : Fin c → T) (K : Finset T) : Finset (Tuple T n)

The rows a recursive term's orbits stay in: the rows over the values of the row the orbit starts from, the context and the term's constants. Its size is what bounds the rounds.

Equations

• rowBox u γ K = Fintype.piFinset fun (x : Fin n) => rowVals u γ K

theorem AggQueryIn.card_le_sizeBound {T : Type} [ValueType T] {S : Set OpKind} (hp : OpKind.prod ∉ S) (ha : OpKind.apply ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : usesOnly S q → q.hygienic → q.recNoFun → ∀ (D : Database T) (γ : Fin c → T), q.SettlesAt D γ → Multiset.card (q.evaluatePlain D γ) ≤ q.sizeBound * (D.size + 1)

Without × and the apply, an answer of the minimal signature is linear in the instance, the recursions included wherever they are defined: a bag recursion's rows are the orbits of its base's rows, ended within a number of rounds the query fixes, and a set recursion's rows are the first points of the orbits of its base's and its constant rows.

def dRep (m : ℕ) : Database ℕ

An instance whose relation holds m copies of one row.

Equations

• dRep m = [("R", ⟨1, Multiset.replicate m ![0]⟩)]

def prodWitness : AggQuery ℕ (1 + 1) (Fin.append (ColKind.allReg 1) (ColKind.allReg 1))

R × R, the witness of the product row.

Equations

• prodWitness = (AggQueryIn.Rel 1 "R").Prod (AggQueryIn.Rel 1 "R")

Projection: the one operator that merges rows

Without Π, a row's multiplicity is bounded by the query alone over an instance that has no duplicate: a union adds two bounds and a product or an apply multiplies them, while nothing else raises a multiplicity – aggregation and duplicate elimination bring it to one, and a selection, a difference and a window leave it alone. A projection is what merges rows that differ in a dropped column, and its answer's multiplicity grows with the instance.

def Database.Nodup {T : Type} (D : Database T) : Prop

An instance no relation of which holds a duplicate.

Equations

• D.Nodup = ∀ (k : ℕ) (s : String) (r : Relation T k), Database.find k s D = some r → Multiset.Nodup r

def AggQueryIn.multBound {T : Type} {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → ℕ

The bound a query gives on the multiplicity of a row of its answer, over an instance that has no duplicate.

Equations

• (AggQueryIn.Rel x✝ a).multBound = 1
• (AggQueryIn.Hole x✝¹ s x✝).multBound = 1
• (AggQueryIn.Param pv x✝).multBound = 1
• AggQueryIn.Empty.multBound = 0
• (AggQueryIn.Proj ps q).multBound = 0
• (AggQueryIn.Sel φ q hφ).multBound = q.multBound
• (q₁.Prod q₂).multBound = q₁.multBound * q₂.multBound
• (q₁.Apply q₂).multBound = q₁.multBound * q₂.multBound
• (q₁.Sum q₂).multBound = q₁.multBound + q₂.multBound
• q.Dedup.multBound = 1
• (q₁.Diff q₂).multBound = q₁.multBound
• (AggQueryIn.Explode k a q).multBound = q.multBound
• (AggQueryIn.Retag h q).multBound = q.multBound
• (AggQueryIn.Mu s q₀ q₁).multBound = q₀.multBound
• (AggQueryIn.MuSet s q₀ q₁).multBound = 1
• (AggQueryIn.Gamma is ts fs q keep ord).multBound = 1
• (AggQueryIn.GammaScalar ts fs q ord).multBound = 1
• (AggQueryIn.GammaNest is his p f q).multBound = 1
• (AggQueryIn.GammaTok is his ts fs a a_1 keep).multBound = 1
• (AggQueryIn.ProvSum is his t a).multBound = 1
• (AggQueryIn.Win P O o w t f q a dist keep).multBound = q.multBound
• (AggQueryIn.WinExpr P O o ws ts fs g q_1 keeps).multBound = q_1.multBound

A recursive term without Π reads the previous round tuple by tuple

What the projection row needs of a recursion is that the rounds of a bag recursion cannot settle past the first: without Π, a recursive term keeps a tuple of the previous round as it is or drops it, and adds tuples that do not depend on the round at all. So a tuple of one round is a tuple of the next, a non-empty round is followed by a non-empty one, and a recursion whose rounds settle settles at once – its value is its base, whose multiplicities the base's own bound covers. The statement below is the affine form of that: the term's output, as a set, is the previous round read through a block of the output's columns, cut down by a condition on the output row, together with a set of rows that read no round. The block is tracked by its offset, which is what shows it to be the whole row where the arities agree.

theorem AggQueryIn.affine_of_body {T : Type} [ValueType T] {S : Set OpKind} (hpr : OpKind.proj ∉ S) {s : String} {m c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : l = [(s, m)] → usesOnly S q → noMention s q → ∀ (D : Database T) (γ : Fin c → T), ∃ (β : Tuple T n → Tuple T m) (a : Tuple T n → Prop) (k : Tuple T n → Prop) (off : ℕ), (∀ (u : Tuple T n), a u → ∀ (i : Fin m), ∃ (h : ↑i + off < n), β u i = u ⟨↑i + off, h⟩) ∧ ∀ (X : Relation T m) (u : Tuple T n), Multiset.Mem (q.evaluatePlain (Database.assign s X D) γ) u ↔ Multiset.Mem X (β u) ∧ a u ∨ k u

Without Π, a recursive term reads the recursive relation tuple by tuple: its rows are the rows u whose block β u is a row of the relation and which satisfy a condition a, together with rows k that read nothing of it. The block is a run of m consecutive columns at offset off, recorded wherever a holds.

theorem AggQueryIn.count_le_multBound {T : Type} [ValueType T] {S : Set OpKind} (hpr : OpKind.proj ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : usesOnly S q → q.hygienic → ∀ (D : Database T), D.Nodup → ∀ (γ : Fin c → T), q.SettlesAt D γ → ∀ (u : Tuple T n), Multiset.count u (q.evaluatePlain D γ) ≤ q.multBound

Without Π, multiplicities are bounded by the query, the recursions included wherever they are defined: a bag recursion settles at its base, and a set recursion's rounds are duplicate-free.

def dShared (m : ℕ) : Database ℕ

An instance whose relation holds m distinct rows sharing their first column.

Equations

• dShared m = [("S", ⟨2, Multiset.map (fun (i : ℕ) => ![0, i]) (Multiset.range m)⟩)]

def projWitness : AggQueryIn ℕ 0 (Nat.succ 0) fun (j : Fin (Nat.succ 0)) => (![ProjColIn.term (TermGIn.index 0 ⋯)] j).kind

Π_{#0}(S), the witness of the projection row.

Equations

• projWitness = AggQueryIn.Proj ![ProjColIn.term (TermGIn.index 0 projWitness._proof_2)] (AggQueryIn.Rel 2 "S")

Generation: where one operator's plain semantics is another's

The invariants above say which classes no generating set may drop. These are the other half of the classification: identities under which a basis holding one operator need not hold another, each an equivalence of plain semantics (AggQueryIn.PlainEquiv) and so blind to annotations – the annotated readings of the two sides of such an identity are a separate question, and evaluate_winByJoin in Provenance.WindowPartition is the one that has both.

What is here: ε from γ (dedup_plainEquiv_gamma), the difference from a product with a tag aggregate (diff_plainEquiv_notIn), a selection from two differences (sel_plainEquiv_selByDiff), and the product from an apply whose right side reads no outer column (apply_plainEquiv_prod). Together they leave {∅, Π, σ, ×, ⊎, γ} generating everything but the apply and the window.

Two further statements complete the generation half, and both are proved elsewhere. Decorrelation – every query is equivalent to one with no apply – is AggQueryIn.exists_applyFree_plainEquiv (Provenance.Decorrelate). And a window is an apply of a scalar aggregation that reads its group in the window's order, which is what a grouping's ORDER BY (Relation.groupSeqOrd) provides: plainEquiv_winByApply below.

theorem AggQueryIn.dedup_plainEquiv_gamma {T : Type} [ValueType T] {lab c n : ℕ} {rd : Fin c → Bool} (q : AggQueryIn T c n (ColKind.allReg n)) : q.Dedup.PlainEquiv (Gamma (fun (k : Fin n) => k) (fun (j : Fin 0) => j.elim0) (fun (j : Fin 0) => j.elim0) q)

ε from γ: duplicate elimination is the grouping by every column with no aggregate. The keys a grouping emits are the distinct rows of its input, and with no aggregate nothing is appended to them, so ε is in no basis that holds γ.

theorem AggQueryIn.apply_plainEquiv_prod {T : Type} [ValueType T] {c n₁ n₂ : ℕ} {κ₂ : Fin n₂ → ColKind} {l : List (String × ℕ)} (q₁ : AggQueryIn T c n₁ (ColKind.allReg n₁) l) (q₂ : AggQueryIn T c n₂ κ₂) : (q₁.Apply (substMap (fun (k : Fin c) => Sum.inr (Fin.natAdd n₁ k)) q₂)).PlainEquiv (q₁.Prod q₂)

A product is a decorrelated apply: an apply whose right side reads no column of the left – a query of the ambient context weakened into the apply's, which AggQueryIn.substMap does – is the product. So × is in no basis that holds the apply, while the converse fails: an apply's right side reads the left row, and no product does.

The difference from a product with a tag aggregate

In the plain semantics the difference is SQL's NOT IN: a copy of a tuple of q₁ survives when q₂ holds no copy of it, and every copy survives or none does. The construction tags each side's rows with a constant – 0 on the left, the domain's non-zero value on the right – unites them, groups by the whole tuple, and counts the tags carrying that value. The count is 0 exactly on the tuples q₂ does not hold, and a product with the keys matched keeps the copies of those tuples.

The aggregate is a count: the grouping's one aggregate counts, through a FILTER clause, the rows carrying the right side's tag. So what the construction asks of it is SeqAggFunc.Counts – SQL's count(e), the aggregate of the minimal signature – and nothing about a sum. The tag it keys on is the value domain's own non-zero value (ValueType.nonzero), so the construction asks nothing of the domain either.

def AggQueryIn.tagCols {T : Type} {c k : ℕ} (a : T) : Tuple (ProjColIn T c (ColKind.allReg k)) (k + 1)

The projection that tags a row with a constant: its own columns, and one more holding a. The column constructor is outside the case analysis, so every output column is regular by reduction.

Equations

• AggQueryIn.tagCols a j = ProjColIn.term (Fin.lastCases (TermGIn.const a) (fun (i : Fin k) => TermGIn.index i ⋯) j)

def AggQueryIn.tagUnion {T : Type} [ValueType T] {c k : ℕ} (q₁ q₂ : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c (k + 1) (ColKind.allReg (k + 1))

The two sides tagged and united: every row of q₁ with 0, every row of q₂ with the domain's non-zero value.

Equations

• q₁.tagUnion q₂ = (AggQueryIn.Proj (AggQueryIn.tagCols 0) q₁).Sum (AggQueryIn.Proj (AggQueryIn.tagCols ValueType.nonzero) q₂)

def AggQueryIn.rightTag {T : Type} [ValueType T] {k : ℕ} : Selection T (k + 1)

The clause that keeps the right side's rows: the ones whose tag column holds the non-zero value. It is an IS NOT DISTINCT FROM, so it is never unknown, and it reads a regular column as a FILTER clause must.

Equations

• AggQueryIn.rightTag = Selection.BT (BoolTerm.SYNEQ (#(Fin.last k)) (TermIn.const ValueType.nonzero))

def AggQueryIn.tagAgg {T : Type} [ValueType T] {c k : ℕ} (cnt : SeqAggFunc T) (q₁ q₂ : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c (k + 1) (Fin.append (fun (x : Fin k) => ColKind.reg) fun (x : Fin 1) => ColKind.agg)

One row per distinct tuple, carrying the count of the right side's copies of it.

Equations

• AggQueryIn.tagAgg cnt q₁ q₂ = AggQueryIn.Gamma (fun (i : Fin k) => i.castSucc) ![#(Fin.last k)] ![cnt] (q₁.tagUnion q₂) ![some AggQueryIn.rightTag]

@[reducible, inline]

abbrev notInKinds (k : ℕ) : Fin (k + (k + 1)) → ColKind

The kinds of the product the construction selects on.

Equations

• notInKinds k = Fin.append (ColKind.allReg k) (Fin.append (fun (x : Fin k) => ColKind.reg) fun (x : Fin 1) => ColKind.agg)

theorem notInKinds_left (k : ℕ) (i : Fin k) : notInKinds k (Fin.castAdd (k + 1) i) = ColKind.reg

theorem notInKinds_key (k : ℕ) (i : Fin k) : notInKinds k (Fin.natAdd k (Fin.castAdd 1 i)) = ColKind.reg

theorem notInKinds_agg (k : ℕ) : notInKinds k (Fin.natAdd k (Fin.natAdd k 0)) = ColKind.agg

def AggQueryIn.notInCond {T : Type} [ValueType T] {c k : ℕ} : GenPredIn T c (notInKinds k)

What the construction selects on: the two blocks of key columns agree, and the tag count is 0.

Equations

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

def AggQueryIn.notInDiff {T : Type} [ValueType T] {c k : ℕ} (cnt : SeqAggFunc T) (q₁ q₂ : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c k (ColKind.allReg k)

The difference read as a NOT IN: the copies of q₁ whose tuple the tag count reads 0 on.

Equations

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

theorem AggQueryIn.diff_plainEquiv_notIn {T : Type} [ValueType T] {c k : ℕ} (cnt : SeqAggFunc T) (hc : cnt.Counts) (q₁ q₂ : AggQueryIn T c k (ColKind.allReg k)) : (q₁.Diff q₂).PlainEquiv (notInDiff cnt q₁ q₂)

− from σ, ×, ⊎, Π and γ: the difference is SQL's NOT IN. Every copy of a tuple of q₁ survives when q₂ holds no copy of it and none survives otherwise, which is what the tag aggregate decides: it reads 0 exactly on the tuples q₂ does not hold, and the product keeps the copies of those.

The aggregate is a parameter, and what the construction asks of it is SeqAggFunc.Counts: it counts the rows a FILTER clause keeps, which are the copies carrying the right side's tag. So the only aggregate the identity needs is SQL's count.

A selection from the difference

The converse direction: where the comparisons are among the terms, a selection is a difference. Tag every row with the truth value of the predicate as a value – which is what a CASE expression over the comparisons gives – and tag every row with the constant that reads true. A row of the first is missing from the second exactly where the predicate fails, so removing that difference from the first leaves the rows the selection keeps.

The term is a parameter of the general statement, with hterm saying that it reads yes on the rows the predicate keeps and nothing else; GenPredIn.polTerm builds it from the predicate – which is what “Ω contains the comparisons” asks for – and sel_plainEquiv_selByDiff_polTerm is the identity with no hypothesis on the term left. An aggregate atom is excluded: its value is a provenance and not a truth value.

def AggQueryIn.tagTermCols {T : Type} {k : ℕ} (t : TermGIn T 0 (ColKind.allReg k)) : Tuple (ProjCol T (ColKind.allReg k)) (k + 1)

The projection that tags a row with the value of a term.

Equations

• AggQueryIn.tagTermCols t j = ProjColIn.term (Fin.lastCases t (fun (i : Fin k) => TermGIn.index i ⋯) j)

def AggQueryIn.dropTag {T : Type} {k : ℕ} : Tuple (ProjCol T (ColKind.allReg (k + 1))) k

The projection that drops a tag column.

Equations

• AggQueryIn.dropTag i = ProjColIn.term (TermGIn.index i.castSucc ⋯)

def AggQueryIn.selByDiff {T : Type} {k : ℕ} (yes : T) (t : TermGIn T 0 (ColKind.allReg k)) (q : AggQuery T k (ColKind.allReg k)) : AggQuery T k (ColKind.allReg k)

A selection written with a difference: the rows tagged yes, read as what is left of the tagged rows after removing those that the constant tagging does not hold.

Equations

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

def GenPredIn.polTerm {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} (yes : T) (pol : Bool) : GenPredIn T c κ → TermGIn T c κ

The predicate read as a term: a CASE expression over the same comparisons, reading yes exactly where the predicate is true (pol = true) or exactly where it is false (pol = false), and 0 elsewhere.

Both polarities are needed because the logic is Kleene's: a negation holds where its argument is false, which is not where its argument fails to hold, so a term reading only truth cannot carry a negation. Reading the two together, a negation is a change of polarity, and the comparisons change with it (CompOp.negate).

Equations

• GenPredIn.polTerm yes true (GenPredIn.cmp a t₁ t₂) = TermGIn.caseWhen a t₁ t₂ (TermGIn.const yes) (TermGIn.const 0)
• GenPredIn.polTerm yes false (GenPredIn.cmp a t₁ t₂) = TermGIn.caseWhen a.negate t₁ t₂ (TermGIn.const yes) (TermGIn.const 0)
• GenPredIn.polTerm yes pol (GenPredIn.aggCmp k a a_1 t) = TermGIn.const 0
• GenPredIn.polTerm yes pol (GenPredIn.aggRange k a a_1 t₁ a_2 t₂) = TermGIn.const 0
• GenPredIn.polTerm yes true (φ.and ψ) = TermGIn.caseWhen CompOp.syneq (GenPredIn.polTerm yes true φ) (TermGIn.const yes) (GenPredIn.polTerm yes true ψ) (TermGIn.const 0)
• GenPredIn.polTerm yes false (φ.and ψ) = TermGIn.caseWhen CompOp.syneq (GenPredIn.polTerm yes false φ) (TermGIn.const yes) (TermGIn.const yes) (GenPredIn.polTerm yes false ψ)
• GenPredIn.polTerm yes true (φ.or ψ) = TermGIn.caseWhen CompOp.syneq (GenPredIn.polTerm yes true φ) (TermGIn.const yes) (TermGIn.const yes) (GenPredIn.polTerm yes true ψ)
• GenPredIn.polTerm yes false (φ.or ψ) = TermGIn.caseWhen CompOp.syneq (GenPredIn.polTerm yes false φ) (TermGIn.const yes) (GenPredIn.polTerm yes false ψ) (TermGIn.const 0)
• GenPredIn.polTerm yes pol φ.not = GenPredIn.polTerm yes (!pol) φ

theorem AggQueryIn.sel_plainEquiv_selByDiff_polTerm {T : Type} [ValueType T] {k : ℕ} (yes : T) (hyes : yes ≠ 0) (φ : GenPred T (ColKind.allReg k)) (hφ : GenPredIn.hasAggAtom φ = false) (q : AggQuery T k (ColKind.allReg k)) : (Sel φ q ⋯).PlainEquiv (selByDiff yes (GenPredIn.polTerm yes true φ) q)

σ from −, with the term built from the predicate. Where the predicate's atoms are comparisons, the CASE expression over them reads yes exactly on the rows it keeps, so the selection is a difference and nothing is asked of Ω beyond the comparisons it already has.

A window from an apply

A window whose frame contains its current row exactly when it contains its peers is an apply – the query with, for each of its rows, a scalar aggregation over the rows that row's frame holds. The frame condition is read as a selection comparing the row's keys against the current row's, which the apply supplies as outer columns, and the aggregation reads its group in the window's own order, which is what the grouping's ORDER BY is for.

Two things are parameters. The frame condition ρ is an arbitrary relation on order values in the library's encoding, so the predicate reading it is given, with hρ saying that it reads it: in SQL it is a frame clause, and there the predicate is the clause. And the frame is asked to contain its current row (ValueFrame.ContainsSelf): EXCLUDE CURRENT ROW and EXCLUDE TIES have no such reading, the group a scalar aggregation reads being determined by the rows and not by the occurrence.

def weakenOuter (T : Type) (d : ℕ) : Fin 0 → T ⊕ Fin d

The empty context, as a substitution: it weakens a closed query or a closed term into one that reads outer columns and ignores them.

Equations

• weakenOuter T d k = k.elim0

def outerKeyCond {T : Type} [ValueType T] {c n' m' : ℕ} {κ : Fin n' → ColKind} (cols : Tuple (Fin n') m') (h : ∀ (k : Fin m'), κ (cols k) = ColKind.reg) (outs : Tuple (Fin c) m') : GenPredIn T c κ

The key comparison against the outer columns: the row's columns cols are compared with the row the apply is reading, which it supplies at the outer positions outs. As in a join the comparison is IS NOT DISTINCT FROM, the syntactic equality a window partitions by.

Equations

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

theorem winApplyKinds (n : ℕ) : (Fin.append (ColKind.allReg n) fun (x : Fin 1) => ColKind.agg) = Fin.snoc (ColKind.allReg n) ColKind.agg

The apply's columns are the query's and the aggregate, as a window's are.

def applyOuter (T : Type) (c n : ℕ) : Fin c → T ⊕ Fin (n + c)

The substitution the apply's right side reads its context through: the left row comes first, so the ambient column j sits at n + j.

Equations

• applyOuter T c n j = Sum.inr (Fin.natAdd n j)

def winByApplyOn {T : Type} [ValueType T] {n m p c : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ψ : GenPredIn T (n + c) (ColKind.allReg n)) (t : TermIn T c n) (f : SeqAggFunc T) (q qf : AggQueryIn T c n (ColKind.allReg n)) : AggQueryIn T c (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

A window written with an apply and a scalar aggregation: for each row of q, the term aggregated over the rows of qf that row's frame holds, read in the window's own order.

The two relations are the same one where the window's input is all regular. They part where it is not: a window reads what ColKind.readTuple leaves of each row, so the rows the frame holds are that reading of the input, while the rows the apply emits are the input's own.

Equations

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

def winByApply {T : Type} [ValueType T] {n m p c : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ψ : GenPredIn T (n + c) (ColKind.allReg n)) (t : TermIn T c n) (f : SeqAggFunc T) (q : AggQueryIn T c n (ColKind.allReg n)) : AggQueryIn T c (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

The same over an all-regular input, where the frame reads the input itself.

Equations

• winByApply P O o ψ t f q = winByApplyOn P O o ψ t f q q

def nullCols {T : Type} [ValueType T] {c k : ℕ} (κ : Fin k → ColKind) : Tuple (ProjColIn T c (ColKind.allReg k)) k

The nulling of the aggregate columns, as a projection: what a window reads of its input (ColKind.readTuple), written in the language over an input whose columns have been re-typed to regular.

Equations

• nullCols κ j = if (κ j).base = ColKind.agg then ProjColIn.term (TermGIn.const 0) else ProjColIn.term (TermGIn.index j ⋯)

def Selection.keepsOpt {T : Type} [ValueType T] {k : ℕ} : Option (Selection T k) → Tuple T k → Bool

What a window's FILTER clause keeps, clause or no clause: with none, every row of the frame.

Equations

• Selection.keepsOpt none = fun (x : Tuple T k) => true
• Selection.keepsOpt (some φ) = φ.keeps

A classical selection as a predicate over a context

def TermIn.toRegIn {T : Type} {c k : ℕ} : Term T k → TermGIn T c (ColKind.allReg k)

A classical term as a term over all-regular columns, in any context.

Equations

• (TermIn.const a).toRegIn = TermGIn.const a
• (TermIn.outer j).toRegIn = j.elim0
• (#i).toRegIn = TermGIn.index i ⋯
• (t₁.add t₂).toRegIn = t₁.toRegIn.add t₂.toRegIn
• (t₁.sub t₂).toRegIn = t₁.toRegIn.sub t₂.toRegIn
• (t₁.mul t₂).toRegIn = t₁.toRegIn.mul t₂.toRegIn
• (TermIn.caseWhen op t₁ t₂ t₃ t₄).toRegIn = TermGIn.caseWhen op t₁.toRegIn t₂.toRegIn t₃.toRegIn t₄.toRegIn
• (t₁.coalesce t₂).toRegIn = t₁.toRegIn.coalesce t₂.toRegIn

def Selection.toPredIn {T : Type} [ValueType T] {c k : ℕ} : Selection T k → GenPredIn T c (ColKind.allReg k)

A classical selection as a predicate over all-regular columns, in any context: the clause of a FILTER or of a frame, read where a query applied to the current row reads it.

Equations

• (Selection.BT (BoolTerm.EQ t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.eq (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• (Selection.BT (BoolTerm.NE t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.ne (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• (Selection.BT (BoolTerm.LE t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.le (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• (Selection.BT (BoolTerm.LT t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.lt (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• (Selection.BT (BoolTerm.GE t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.ge (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• (Selection.BT (BoolTerm.GT t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.gt (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• (Selection.BT (BoolTerm.SYNEQ t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.syneq (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• (Selection.BT (BoolTerm.SYNNE t₁ t₂)).toPredIn = GenPredIn.cmp CompOp.synne (TermIn.toRegIn t₁) (TermIn.toRegIn t₂)
• φ.Not.toPredIn = φ.toPredIn.not
• (φ₁.And φ₂).toPredIn = φ₁.toPredIn.and φ₂.toPredIn
• (φ₁.Or φ₂).toPredIn = φ₁.toPredIn.or φ₂.toPredIn
• Selection.True.toPredIn = GenPredIn.cmp CompOp.eq (TermGIn.const 0) (TermGIn.const 0)

A frame clause as a predicate

def OrderCol.lePred {T : Type} {c m : ℕ} (cl : OrderCol) (x y : TermGIn T c (ColKind.allReg m)) : GenPredIn T c (ColKind.allReg m)

One column of the clause, as a comparison: the direction decides which way round the two terms are read.

Equations

• cl.lePred x y = if cl.desc = true then GenPredIn.cmp CompOp.le y x else GenPredIn.cmp CompOp.le x y

def OrderCol.ltPred {T : Type} {c m : ℕ} (cl : OrderCol) (x y : TermGIn T c (ColKind.allReg m)) : GenPredIn T c (ColKind.allReg m)

The same strictly.

Equations

• cl.ltPred x y = if cl.desc = true then GenPredIn.cmp CompOp.lt y x else GenPredIn.cmp CompOp.lt x y

def OrderCol.lePredN {T : Type} {c m : ℕ} (cl : OrderCol) (ν : T) (x y : TermGIn T c (ColKind.allReg m)) : GenPredIn T c (ColKind.allReg m)

One column of the clause where the domain names its null: the comparison, guarded by the null tests the clause's placement asks for. IS NULL is spelled IS NOT DISTINCT FROM ν, which is why the null has to be a value the terms can name – ValueType has an isNull predicate and no null constant, so the guards cannot be written without one.

Equations

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

def OrderCol.ltPredN {T : Type} {c m : ℕ} (cl : OrderCol) (ν : T) (x y : TermGIn T c (ColKind.allReg m)) : GenPredIn T c (ColKind.allReg m)

And the strict one: the negation of the comparison the other way round, which is where the guards swap places.

Equations

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

def OrderSpec.lePredOnOf {T : Type} [ValueType T] {p c m : ℕ} (base : Fin p → GenPredIn T c (ColKind.allReg m)) (x y : Fin p → TermGIn T c (ColKind.allReg m)) : List (Fin p) → GenPredIn T c (ColKind.allReg m)

The clause's comparison as a predicate: lexicographically, the columns in the order the clause names them, each column compared by a predicate of its own – which is where the direction and the null placement are read.

Equations

• OrderSpec.lePredOnOf base x y [] = GenPredIn.cmp CompOp.syneq (TermGIn.const 0) (TermGIn.const 0)
• OrderSpec.lePredOnOf base x y (k :: ks) = ((GenPredIn.cmp CompOp.syneq (x k) (y k)).and (OrderSpec.lePredOnOf base x y ks)).or ((GenPredIn.cmp CompOp.synne (x k) (y k)).and (base k))

def OrderSpec.ltPredOnOf {T : Type} [ValueType T] {p c m : ℕ} (base : Fin p → GenPredIn T c (ColKind.allReg m)) (x y : Fin p → TermGIn T c (ColKind.allReg m)) : List (Fin p) → GenPredIn T c (ColKind.allReg m)

And the strict one: what the clause puts before the current row's peers.

Equations

• OrderSpec.ltPredOnOf base x y [] = GenPredIn.cmp CompOp.synne (TermGIn.const 0) (TermGIn.const 0)
• OrderSpec.ltPredOnOf base x y (k :: ks) = ((GenPredIn.cmp CompOp.syneq (x k) (y k)).and (OrderSpec.ltPredOnOf base x y ks)).or ((GenPredIn.cmp CompOp.synne (x k) (y k)).and (base k))

def OrderSpec.lePredOn {T : Type} [ValueType T] {p c m : ℕ} (o : OrderSpec p) (x y : Fin p → TermGIn T c (ColKind.allReg m)) (ks : List (Fin p)) : GenPredIn T c (ColKind.allReg m)

The clause's comparison where nothing is null: the column's own comparison, in its own direction.

Equations

• o.lePredOn x y ks = OrderSpec.lePredOnOf (fun (k : Fin p) => (o k).lePred (x k) (y k)) x y ks

def OrderSpec.ltPredOn {T : Type} [ValueType T] {p c m : ℕ} (o : OrderSpec p) (x y : Fin p → TermGIn T c (ColKind.allReg m)) (ks : List (Fin p)) : GenPredIn T c (ColKind.allReg m)

And the strict one.

Equations

• o.ltPredOn x y ks = OrderSpec.ltPredOnOf (fun (k : Fin p) => (o k).ltPred (x k) (y k)) x y ks

The frame condition of the clause-determined frames

def frameSelfTerms {T : Type} {c k q : ℕ} (O : Tuple (Fin k) q) : Fin q → TermGIn T (k + c) (ColKind.allReg k)

The row's own order columns, as terms of the derived window's selection.

Equations

• frameSelfTerms O j = TermGIn.index (O j) ⋯

def frameOuterTerms {T : Type} {c k q : ℕ} (O : Tuple (Fin k) q) : Fin q → TermGIn T (k + c) (ColKind.allReg k)

The current row's, which the apply supplies as outer columns.

Equations

• frameOuterTerms O j = TermGIn.outer (Fin.castAdd c (O j))

def clausePredOpt {T : Type} [ValueType T] {c k : ℕ} : Option (Selection T k) → GenPredIn T c (ColKind.allReg k)

A window's FILTER clause as a predicate, or the tautology where there is none.

Equations

• clausePredOpt none = GenPredIn.cmp CompOp.syneq (TermGIn.const 0) (TermGIn.const 0)
• clausePredOpt (some φ) = φ.toPredIn

The predicates built here apply no function to values

def truePred {T : Type} [ValueType T] {c k : ℕ} : GenPredIn T c (ColKind.allReg k)

The tautology as a predicate of the language: IS NOT DISTINCT FROM between two equal constants.

Equations

• truePred = GenPredIn.cmp CompOp.syneq (TermGIn.const 0) (TermGIn.const 0)

def falsePred {T : Type} [ValueType T] {c k : ℕ} : GenPredIn T c (ColKind.allReg k)

And its opposite, which the value domain's own non-zero value makes available: the base case of a disjunction over no condition.

Equations

• falsePred = GenPredIn.cmp CompOp.syneq (TermGIn.const 0) (TermGIn.const ValueType.nonzero)

The two RANGE frames, with no hypothesis on the domain

ValueType names the domain's null (ValueType.nullVal), so the two readings above are the two cases of one lemma: a domain naming no null has none, and a domain naming one has it as its only null, which is what the IS NOT DISTINCT FROM ν tests need. Nothing is left for a caller to supply.

Every frame condition is a predicate of the language

A frame is a condition on the order values (FrameCond), so the predicate that spells it out in a window's derived form (winByApplyOn) is not something a caller has to supply: it is read off the condition. The two strict cases are conditions of the language and not negations, and reading the clause backwards is what turns at or before into at or after (OrderSpec.le_reverse), so the four comparisons are the two lemmas above at o and at o.reverse. The EXCLUDE modifiers and the union of the frames of a multi-frame window are the Boolean cases, where the reading of a conjunction and of a disjunction are the conjunction and the disjunction of the readings – Kleene's logic agreeing with the two-valued one on truth, which is what a selection keeps a row by.

def OrderCol.shiftTerm {T : Type} {c m : ℕ} (cl : OrderCol) (pre : Bool) (a : T) (x : TermGIn T c (ColKind.allReg m)) : TermGIn T c (ColKind.allReg m)

The current row's value moved by an offset, as a term.

Equations

• cl.shiftTerm pre a x = if (pre != cl.desc) = true then x.sub (TermGIn.const a) else x.add (TermGIn.const a)

theorem FrameCond.exists_condPred {T : Type} [ValueType T] {n p c : ℕ} (O : Tuple (Fin n) p) (fc : FrameCond T p) : ∃ (ψ : GenPredIn T (n + c) (ColKind.allReg n)), (fc.noOff = true → ψ.noFun = true) ∧ ∀ (y u : Tuple T n) (γ : Fin c → T), ψ.holdsPlain y (Fin.append u γ) ↔ fc.holds (O.key y) (O.key u) = true

Every frame condition is a predicate of the query language.

theorem ValueFrame.exists_framePred {T : Type} [ValueType T] {n p c : ℕ} (O : Tuple (Fin n) p) (w : ValueFrame T p) (keep : Option (Selection T n)) : ∃ (ψ : GenPredIn T (n + c) (ColKind.allReg n)), (Selection.noFunOpt keep = true → w.cond.noOff = true → ψ.noFun = true) ∧ ∀ (y u : Tuple T n) (γ : Fin c → T), ψ.holdsPlain y (Fin.append u γ) ↔ w.ρ (O.key y) (O.key u) = true ∧ Selection.keepsOpt keep y = true

A frame and a FILTER clause are a predicate of the language: what a window's derived form (winByApplyOn) spells its frame out with, for every frame the syntax can name and every clause.

theorem evaluatePlain_winByApplyOf {T : Type} [ValueType T] {n m p lab c : ℕ} {rd : Fin c → Bool} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) {w : ValueFrame T p} {hsql : ValueFrame.IsSQL o w} (hc : w.ContainsSelf) (ψ : GenPredIn T (n + c) (ColKind.allReg n)) (t : TermIn T c n) (f : SeqAggFunc T) (dist : Bool) (keep : Option (Selection T n)) (hρ : ∀ (y u : Tuple T n) (γ : Fin c → T), ψ.holdsPlain y (Fin.append u γ) ↔ w.ρ (O.key y) (O.key u) = true ∧ Selection.keepsOpt keep y = true) (q : AggQueryIn T c n (ColKind.allReg n)) (D : Database T) (γ : Fin c → T) : (winByApply P O o ψ t (if dist = true then f.distinct else f) q).evaluatePlain D γ = (AggQueryIn.Win P O o w t f q ⋯ dist keep).evaluatePlain D γ

The all-regular case: there the frame reads the input itself.

theorem evaluatePlain_winByApply {T : Type} [ValueType T] {n m p lab c : ℕ} {rd : Fin c → Bool} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) {w : ValueFrame T p} {hsql : ValueFrame.IsSQL o w} (hc : w.ContainsSelf) (ψ : GenPredIn T (n + c) (ColKind.allReg n)) (hρ : ∀ (y u : Tuple T n) (γ : Fin c → T), ψ.holdsPlain y (Fin.append u γ) ↔ w.ρ (O.key y) (O.key u) = true) (t : TermIn T c n) (f : SeqAggFunc T) (q : AggQueryIn T c n (ColKind.allReg n)) (D : Database T) (γ : Fin c → T) : (winByApply P O o ψ t f q).evaluatePlain D γ = (AggQueryIn.Win P O o w t f q ⋯).evaluatePlain D γ

A window is an apply of a scalar aggregation, over plain relations: the rows the selection keeps are the current row's frame, the clause reads them in the order the window reads them, and the aggregate is then the window's value. This is the plain form, with neither DISTINCT nor a FILTER clause; evaluatePlain_winByApplyOf has both.

theorem plainEquiv_winByApply {T : Type} [ValueType T] {n m p lab c : ℕ} {rd : Fin c → Bool} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) {w : ValueFrame T p} {hsql : ValueFrame.IsSQL o w} (hc : w.ContainsSelf) (ψ : GenPredIn T (n + c) (ColKind.allReg n)) (hρ : ∀ (y u : Tuple T n) (γ : Fin c → T), ψ.holdsPlain y (Fin.append u γ) ↔ w.ρ (O.key y) (O.key u) = true) (t : TermIn T c n) (f : SeqAggFunc T) (q : AggQueryIn T c n (ColKind.allReg n)) : (AggQueryIn.Win P O o w t f q ⋯).PlainEquiv (winByApply P O o ψ t f q)

A window is expressible without one, as an equivalence of queries (AggQueryIn.PlainEquiv).

Aggregation: the one operator that makes a row from nothing

theorem AggQueryIn.evaluatePlain_eq_zero_of_allEmpty {T : Type} [ValueType T] {S : Set OpKind} (hγ : OpKind.gamma ∉ S) {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : usesOnly S q → ∀ (D : Database T), D.allEmpty → ∀ (γ : Fin c → T), q.evaluatePlain D γ = 0

Without γ, the empty instance has an empty answer. Every other operator maps the empty relation to an empty relation: a projection and a window map it row by row, a selection filters it, a product and an apply read one row of each side, a union adds, duplicate elimination and difference only remove. Aggregation is the exception, the scalar form emitting its row whatever its input.

Home · Documentation · Publications · Contributors · Source · Cite