⊎ from μ^⊎ with products

Provenance.SumByMu derives the union from two bag recursions whose rounds join the recursive relation with a closed relation, the join written as an apply so that the construction lives in a basis holding the apply. Here the same construction is written with the product, for the bases holding × and not the apply: AggQueryIn.sumByMuX. Its rounds read exactly what sumByMu's do (AggQueryIn.apply_plainEquiv_prod), so its value and its definedness are those of sumByMu.

The difference read as a NOT IN (AggQueryIn.notInDiff) is a product already; AggQueryIn.notInDiffX is it with its tagged union written by sumByMuX.

Bag recursions with equal bodies

The construction

def AggQueryIn.phaseBodyX {T : Type} {c k : ℕ} (s : String) (p₁ : T) (Z : AggQueryIn T c (k + 1) (ColKind.allReg (k + 1))) : AggQueryIn T c (k + 1) (ColKind.allReg (k + 1)) [(s, k + 1)]

A round of the construction, with a product: phaseBody with the apply replaced by the product it stands for.

Equations

• AggQueryIn.phaseBodyX s p₁ Z = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (AggQueryIn.roundCols p₁) (AggQueryIn.Sel AggQueryIn.sameTag ((AggQueryIn.Hole (k + 1) s).Prod Z) ⋯))

def AggQueryIn.sumByMuX {T : Type} [ValueType T] {c k : ℕ} (s₁ s₂ : String) (q₁ q₂ : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c k (ColKind.allReg k)

⊎ from two bag recursions with products: sumByMu with each round's apply written as the product it is.

Equations

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

What the construction is made of

def AggQueryIn.sumProdOps : Set OpKind

The classes the construction uses: sumMuOps with the product in place of the apply.

Equations

• AggQueryIn.sumProdOps = {OpKind.empty, OpKind.proj, OpKind.sel, OpKind.prod, OpKind.gamma, OpKind.muBag}

The difference, with products and the union from recursions

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

The tagged union of the NOT IN form, its union written by sumByMuX.

Equations

• AggQueryIn.tagUnionX s₁ s₂ q₁ q₂ = AggQueryIn.sumByMuX s₁ s₂ (AggQueryIn.Proj (AggQueryIn.tagCols 0) q₁) (AggQueryIn.Proj (AggQueryIn.tagCols ValueType.nonzero) q₂)

def AggQueryIn.tagAggX {T : Type} [ValueType T] {c k : ℕ} (s₁ s₂ : String) (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)

The grouping of the NOT IN form over tagUnionX.

Equations

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

def AggQueryIn.notInDiffX {T : Type} [ValueType T] {c k : ℕ} (s₁ s₂ : String) (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, over the classes of a basis holding × and not ⊎.

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite