The pass over the whole algebra

Which classes every basis of the whole algebra contains is required_mem_of_generatesOnRec. This module is the construction behind the generation half: one structural induction (exists_basisRec_aux) matching every query of the whole algebra in the minimal universe by a query over a target set of classes holding the construction's six (AggQueryIn.sumMuOps: ∅, Π, σ, the apply, γ, μ^⊎) and not ⊎, with win kept or derived and the set recursion kept or handed to a MuSetHandler. Its instance over basisRecOps = {∅, Π, σ, apply, γ, win, μ^⊎}, the basis of the whole algebra, is basisRecOps_generatesOnRec in Provenance.MuUnion, where the handler is proved. The apply is kept in place of × because the restriction on recursive terms admits an apply whose left side reads the recursive relation, and the decorrelation of such an apply puts ε of that left side inside the right side's decorrelation – the recursive relation read twice, under a duplicate elimination.

The pass is one structural induction (exists_basisRec_aux), every node re-typed to regular columns and rewritten by the local identities of Provenance.PlainBasis – a window kept over the doubled input (Provenance.WinKept) or, without the window class, written as an apply of a scalar aggregation (winByApply), duplicate elimination as a grouping, the difference as a NOT IN, a product as an apply, a union as two bag recursions (Provenance.SumByMu) – with a second half for recursive bodies, as the union's pass has. What the induction needs first is that the predicates the generation statement asks of its output pass through the two wrappers every case uses: the substitution an apply's right side is read through (AggQueryIn.substMap) and the re-typing of an operator's output (AggQueryIn.allRegOf).

The same through the re-typing of a query's columns

What re-typing a column keeps of the signature

A product in the other order

A recursive term may read the recursive relation on either side of a product, but only on the left of an apply, so a product whose right side reads it is written as the apply the other way round, its columns put back in place by a projection.

def swapIdx (n₁ n₂ : ℕ) : Fin (n₁ + n₂) → Fin (n₂ + n₁)

The column j of a product, in the product the other way round.

Equations

• swapIdx n₁ n₂ i = Fin.addCases (fun (i : Fin n₁) => Fin.natAdd n₂ i) (fun (i : Fin n₂) => Fin.castAdd n₁ i) i

def swapCols {T : Type} (c n₁ n₂ : ℕ) : Fin (n₁ + n₂) → ProjColIn T c (Fin.append (ColKind.allReg n₂) (ColKind.allReg n₁))

The columns of the swap, over the product the other way round.

Equations

• swapCols c n₁ n₂ j = ProjColIn.term (TermGIn.index (swapIdx n₁ n₂ j) ⋯)

theorem swapCols_kind {T : Type} (c n₁ n₂ : ℕ) : (fun (j : Fin (n₁ + n₂)) => (swapCols c n₁ n₂ j).kind) = ColKind.allReg (n₁ + n₂)

def AggQueryIn.prodSwap {T : Type} {c n₁ n₂ : ℕ} {l : List (String × ℕ)} (q₂ : AggQueryIn T c n₂ (ColKind.allReg n₂) l) (q₁ : AggQueryIn T c n₁ (ColKind.allReg n₁)) : AggQueryIn T c (n₁ + n₂) (ColKind.allReg (n₁ + n₂)) l

q₁ × q₂ as the apply of q₂ with q₁ lifted to its context, the columns put back in the product's order.

Equations

• q₂.prodSwap q₁ = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (swapCols c n₁ n₂) (q₂.Apply (AggQueryIn.substMap (fun (j : Fin c) => Sum.inr (Fin.natAdd n₂ j)) q₁)))

The window's derived form, through the predicates of the pass

The difference's derived form, its product written as an apply

def AggQueryIn.notInDiffA {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 NOT IN form with its product written as an apply, which is what a basis holding the apply and not × reads it as.

Equations

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

A product as an apply, in the order given and the other way round

def AggQueryIn.prodA {T : Type} {c n₁ n₂ : ℕ} {l : List (String × ℕ)} (q₁ : AggQueryIn T c n₁ (ColKind.allReg n₁) l) (q₂ : AggQueryIn T c n₂ (ColKind.allReg n₂)) : AggQueryIn T c (n₁ + n₂) (ColKind.allReg (n₁ + n₂)) l

q₁ × q₂ as the apply of q₁ with q₂ lifted to its context.

Equations

• q₁.prodA q₂ = AggQueryIn.castKind ⋯ (q₁.Apply (AggQueryIn.substMap (applyOuter T c n₁) q₂))

The classes, and what the pass carries

structure AggQueryIn.BasisRecOf {T : Type} [ValueType T] (S : Set OpKind) (Θ : Set (SeqAggFunc T)) (f : ℕ → String) {c n : ℕ} {κ : Fin n → ColKind} {l l' : List (String × ℕ)} (q : AggQueryIn T c n κ l) (q' : AggQueryIn T c n (ColKind.allReg n) l') : Prop

What the pass keeps of a query, besides its value: the generating classes, the restriction on recursive terms, the signature, well-formedness over a schema declaring none of the fresh names, the names (its own, or fresh ones), and the names it does not mention (fresh ones aside). Windows are gone from the output, so nothing is said of them.

• usesOnly : AggQueryIn.usesOnly S q'
• hygienic : q'.hygienic
• inSig : AggQueryIn.inSig Θ q'
• over (sch : Schema) : (∀ (i : ℕ), sch.decl (f i) = none) → overSchema sch q → overSchema sch q'
• names (x : String) : x ∈ q'.names → x ∈ q.names ∨ ∃ (i : ℕ), x = f i
• nom (s : String) : (∀ (i : ℕ), s ≠ f i) → noMention s q → noMention s q'

def AggQueryIn.tri (f : ℕ → String) (j : ℕ) : ℕ → String

A third of the supply: the names f (3 i + j).

Equations

• AggQueryIn.tri f j i = f (3 * i + j)

def AggQueryIn.MuSetHandler {T : Type} [ValueType T] (S : Set OpKind) (Θ : Set (SeqAggFunc T)) : Prop

What stands in for a set recursion where the target classes hold none: from the pass's rewriting of the base, the body and its closed part of μ^∪R.(q₀, q₁), a query over the target classes defined and equal to the recursion wherever the recursion is. The supply f is the recursion's own, its children having been rewritten with its first and second thirds; the bodies are over the schema the recursion is written over, with its name declared.

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite