The joint reading of a family, and homomorphisms

A selection comparing several aggregate values of one family reads them in one world of the family (classWorlds). Under a homomorphism the family's listing is reordered among tied occurrences – the evaluator lists a group by its rows and then by the annotations, and the annotations are not the same on the two sides – and a joint reading is blind to that only if every value of the family is reordered together.

This holds when every value of the family is built from one listing of the family's occurrences by a function of the occurrence's row: a LeafSpec says how a value reads an occurrence (what each of its leaves reads, whether it is in the leaf's group, whether the leaf's clause keeps it), and LeafSpec.build is the value it builds from a listing. Then a world of the family is read off the sequence of rows it selects (classWorlds_presented), the bag of those is blind to a tie-block permutation of the listing (subWorlds_tiePerm), and the joint worlds of the two sides correspond (classWorlds_hom).

structure LeafSpec (ρ T : Type) : Type

How an aggregate value reads an occurrence of its family, as a function of the occurrence's row ρ: the value each leaf reads, whether the occurrence is in each leaf's group, whether each leaf's clause keeps it – and the leaves' aggregates, conventions and combining function.

• arity : ℕ
• V : ρ → Fin self.arity → T
• Fr : ρ → Fin self.arity → Bool
• Kp : ρ → Fin self.arity → Bool
• aggs : Fin self.arity → SeqAggFunc T
• scalar : Fin self.arity → Bool
• g : (Fin self.arity → T) → T

def LeafSpec.build {ρ T β K : Type} (sp : LeafSpec ρ T) (L : List β) (ann : β → K) (str : β → ρ) (φ : FamId T) : AggExpr T K

The value built from a listing L of the family, an occurrence being read through its row str and annotated by ann.

Equations

• sp.build L ann str φ = { arity := sp.arity, occs := List.map (fun (b : β) => (sp.V (str b), ann b, sp.Fr (str b), sp.Kp (str b))) L, aggs := sp.aggs, scalar := sp.scalar, g := sp.g, fam := φ }

def LeafSpec.okL {ρ T : Type} (sp : LeafSpec ρ T) (s : List ρ) : Prop

Whether a selected sequence of rows is a world of the value.

Equations

• sp.okL s = ∀ (j : Fin sp.arity), sp.scalar j = false → ∃ r ∈ s, sp.Fr r j = true

def LeafSpec.valL {ρ T : Type} (sp : LeafSpec ρ T) (s : List ρ) : T

The value on a selected sequence of rows.

Equations

• sp.valL s = sp.g fun (j : Fin sp.arity) => sp.aggs j (List.map (fun (r : ρ) => sp.V r j) (List.filter (fun (r : ρ) => sp.Fr r j && sp.Kp r j) s))

def AggExpr.PresBy {ρ β T K : Type} (e : AggExpr T K) (L : List β) (ann : β → K) (str : β → ρ) (ok : List ρ → Prop) (val : List ρ → T) : Prop

An aggregate expression presented by a listing: its occurrences are the listing's, position for position, with the listing's annotations, and its world condition and its value are read off the rows a world selects, through ok and val. This is all a joint reading asks of a value of a family.

Equations

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

Two lists related position by position

theorem classWorlds_presented {T K : Type} [CommSemiringWithMonus K] [ValueType T] [DecidableEq K] {ρ β : Type} {n : ℕ} (u : Tuple (GenValue T K) n) (M : List (Fin n)) (L : List β) (ann : β → K) (str : β → ρ) (ok : Fin n → List ρ → Prop) (val : Fin n → List ρ → T) (hM : ∀ k ∈ M, ∃ (y : AggTok T K), u k = Sum.inr y ∧ y.flatExpr.PresBy L ann str (ok k) (val k)) (x₀ : AggTok T K) (hx₀ : x₀.isNested = false) (ok₀ : List ρ → Prop) (val₀ : List ρ → T) (hx₀b : x₀.flatExpr.PresBy L ann str ok₀ val₀) : classWorlds u M x₀ = Multiset.map (fun (w : K × K × List ρ) => (w.1, w.2.1, fun (k : Fin n) => if k ∈ M then some (val k w.2.2) else none)) (Multiset.filter (fun (w : K × K × List ρ) => ∀ k ∈ M, ok k w.2.2) (Multiset.map (fun (w : K × K × List β) => (w.1, w.2.1, List.map str w.2.2)) (subWorlds ann L)))

A family built from one listing reads its worlds off the listing. If every column of M holds a value presented by the listing L (each read through its own ok and val), and so does the value x₀ the family is listed by, then the family's worlds are the subfamilies of L, each read through the rows it selects.

theorem classWorlds_hom {T K : Type} [CommSemiringWithMonus K] [ValueType T] [DecidableEq K] {K' : Type} [CommSemiringWithMonus K'] [DecidableEq K'] (f : K →+* K') {ρ β β' : Type} {n : ℕ} (u : Tuple (GenValue T K) n) (u' : Tuple (GenValue T K') n) (M : List (Fin n)) (L : List β) (ann : β → K) (str : β → ρ) (L' : List β') (ann' : β' → K') (str' : β' → ρ) (e : β → β') {eqv : β' → β' → Prop} (heqv : ∀ {a b : β'}, eqv a b → str' a = str' b) (hperm : TiePerm eqv L' (List.map e L)) (hstr : ∀ (b : β), str' (e b) = str b) (hann : ∀ (b : β), ann' (e b) = f (ann b)) (ok : Fin n → List ρ → Prop) (val : Fin n → List ρ → T) (hM : ∀ k ∈ M, ∃ (y : AggTok T K), u k = Sum.inr y ∧ y.flatExpr.PresBy L ann str (ok k) (val k)) (hM' : ∀ k ∈ M, ∃ (y : AggTok T K'), u' k = Sum.inr y ∧ y.flatExpr.PresBy L' ann' str' (ok k) (val k)) (x₀ : AggTok T K) (hx₀ : x₀.isNested = false) (ok₀ : List ρ → Prop) (val₀ : List ρ → T) (hx₀b : x₀.flatExpr.PresBy L ann str ok₀ val₀) (x₀' : AggTok T K') (hx₀' : x₀'.isNested = false) (hx₀b' : x₀'.flatExpr.PresBy L' ann' str' ok₀ val₀) : classWorlds u' M x₀' = Multiset.map (fun (w : K × K × (Fin n → Option T)) => (f w.1, f w.2.1, w.2.2)) (classWorlds u M x₀)

The joint worlds of a family under a homomorphism. On the two sides the family's values are presented, through the same readings, by two listings, the second a tie-block permutation of the first pushed through f – occurrences swapped only where their rows read alike. Then the family's worlds correspond, annotations pushed through f and every value unchanged: the values of the family are reordered together.

theorem jointWorlds_hom {T K : Type} [CommSemiringWithMonus K] [ValueType T] [DecidableEq K] {K' : Type} [CommSemiringWithMonus K'] [DecidableEq K'] (f : K →+* K') {n : ℕ} (u : Tuple (GenValue T K) n) (u' : Tuple (GenValue T K') n) (cols : List (Fin n)) (hagg : ∀ k ∈ cols, (∃ (x : AggTok T K), u k = Sum.inr x) ↔ ∃ (x' : AggTok T K'), u' k = Sum.inr x') (hkey : ∀ k ∈ cols, ∀ l ∈ cols, ∀ (x y : AggTok T K) (x' y' : AggTok T K'), u k = Sum.inr x → u l = Sum.inr y → u' k = Sum.inr x' → u' l = Sum.inr y' → (x'.classKey = y'.classKey ↔ x.classKey = y.classKey)) (hclass : ∀ k ∈ cols, ∀ (x : AggTok T K) (x' : AggTok T K'), u k = Sum.inr x → u' k = Sum.inr x' → classWorlds u' (List.map Prod.fst (List.filter (fun (p : Fin n × AggTok T K) => decide (p.2.classKey = x.classKey)) (tokCols u cols))) x' = Multiset.map (fun (w : K × K × (Fin n → Option T)) => (f w.1, f w.2.1, w.2.2)) (classWorlds u (List.map Prod.fst (List.filter (fun (p : Fin n × AggTok T K) => decide (p.2.classKey = x.classKey)) (tokCols u cols))) x)) : jointWorlds u' cols = Multiset.map (fun (w : K × K × (Fin n → Option T)) => (f w.1, f w.2.1, w.2.2)) (jointWorlds u cols)

The joint worlds of a row under a homomorphism. If the two rows hold aggregate values at the same compared columns, group them into families alike, and each family's worlds correspond, so do the joint worlds.

Families presented on both sides

What the joint reading of a row needs under a homomorphism, collected over a set S of pairs of corresponding values (the target's and the source's): that the two sides group them into families alike, and that each family is presented – its flat values built from one listing on each side, the two listings tie-block permuted (ListingRel), or its nested values having corresponding worlds (NestedValue.WCorr).

structure ListingRel {K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (T : Type) : Type 1

Two listings of a family's occurrences, related by a homomorphism: the target's is a tie-block permutation of the source's pushed through f, occurrences swapped only where their rows read alike.

• ρ : Type
• β : Type
• β' : Type
• L : List self.β
• ann : self.β → K
• str : self.β → self.ρ
• L' : List self.β'
• ann' : self.β' → K'
• str' : self.β' → self.ρ
• e : self.β → self.β'
• eqv : self.β' → self.β' → Prop
• heqv {a b : self.β'} : self.eqv a b → self.str' a = self.str' b
• hperm : TiePerm self.eqv self.L' (List.map self.e self.L)
• hstr (b : self.β) : self.str' (self.e b) = self.str b
• hann (b : self.β) : self.ann' (self.e b) = f (self.ann b)

def ListingRel.Member {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {f : K →+* K'} (D : ListingRel f T) (y' : AggTok T K') (y : AggTok T K) : Prop

A pair of flat values presented by a related pair of listings, through the same readings.

Equations

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

def NestedValue.WCorr {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq T] [DecidableEq K] [DecidableEq K'] (f : K →+* K') (b' : NestedValue T K') (b : NestedValue T K) : Prop

The worlds of two nested values correspond under a homomorphism: both enumerations are images of one bag of indices, and at each index the two worlds keep and leave out annotations related by f, read the same inner values, and ask the same of what they keep. This is all a reading of a nested value asks of its worlds – its admissibility, its value and its weight – and it reads only the storey and the occurrences of the two values, so a term over a nested column keeps it.

Equations

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

def NestMember {T K K' : Type} (y' : AggTok T K') (y : AggTok T K) : Prop

A pair of nested values with the same outer aggregate and convention.

Equations

• NestMember y' y = ∃ (b : NestedValue T K) (b' : NestedValue T K'), y = AggTok.nest b ∧ y' = AggTok.nest b' ∧ b'.agg = b.agg ∧ b'.scalar = b.scalar

def FamPres {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq T] [DecidableEq K] [DecidableEq K'] (f : K →+* K') (S : AggTok T K' × AggTok T K → Prop) : Prop

A set of corresponding values whose families are presented on both sides.

Equations

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

theorem classWorlds_of_wcorr {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [ValueType T] [DecidableEq K] [DecidableEq K'] (f : K →+* K') {n : ℕ} (u : Tuple (GenValue T K) n) (u' : Tuple (GenValue T K') n) (M : List (Fin n)) (a : NestedValue T K) (a' : NestedValue T K') (hw : NestedValue.WCorr f a' a) (hM : ∀ k ∈ M, ∃ (b : NestedValue T K) (b' : NestedValue T K'), u k = Sum.inr (AggTok.nest b) ∧ u' k = Sum.inr (AggTok.nest b') ∧ b'.agg = b.agg ∧ b'.scalar = b.scalar) : classWorlds u' M (AggTok.nest a') = Multiset.map (fun (w : K × K × (Fin n → Option T)) => (f w.1, f w.2.1, w.2.2)) (classWorlds u M (AggTok.nest a))

A nested family's worlds under a homomorphism. If the representatives' worlds correspond and every column of the family holds a nested value with the same outer aggregate and convention on both sides, the family's worlds correspond, the pair pushed through f.

theorem jointWorlds_of_famPres {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [ValueType T] [DecidableEq K] [DecidableEq K'] (f : K →+* K') {n : ℕ} (u : Tuple (GenValue T K) n) (u' : Tuple (GenValue T K') n) (cols : List (Fin n)) (hagg : ∀ k ∈ cols, (∃ (x : AggTok T K), u k = Sum.inr x) ↔ ∃ (x' : AggTok T K'), u' k = Sum.inr x') (hF : FamPres f fun (p : AggTok T K' × AggTok T K) => ∃ k ∈ cols, u' k = Sum.inr p.1 ∧ u k = Sum.inr p.2) : jointWorlds u' cols = Multiset.map (fun (w : K × K × (Fin n → Option T)) => (f w.1, f w.2.1, w.2.2)) (jointWorlds u cols)

The joint worlds of a row whose families are presented on both sides correspond.

Closure under terms

A term over an aggregate column (AggTok.postcompTerm) composes the value's outer function and keeps its family: the same occurrences, the same group key, a family identifier recording the term. So it stays in its class, and a presented family stays presented.

inductive PCl {T K K' : Type} [ValueType T] (S : AggTok T K' × AggTok T K → Prop) : AggTok T K' × AggTok T K → Prop

The closure of a set of corresponding values under terms, taken on both sides alike.

• base {T K K' : Type} [ValueType T] {S : AggTok T K' × AggTok T K → Prop} {p : AggTok T K' × AggTok T K} : S p → PCl S p
• step {T K K' : Type} [ValueType T] {S : AggTok T K' × AggTok T K → Prop} {p : AggTok T K' × AggTok T K} (t : TermIn T 1 0) : PCl S p → PCl S (AggTok.postcompTerm t p.1, AggTok.postcompTerm t p.2)
• stepF {T K K' : Type} [ValueType T] {S : AggTok T K' × AggTok T K → Prop} {p : AggTok T K' × AggTok T K} (gf : T → T) : PCl S p → PCl S (AggTok.postcomp gf p.1, AggTok.postcomp gf p.2)

The operator a family records

def FamId.lab {T : Type} : FamId T → ℕ

The label of the operator a family identifier records.

Equations

• (FamId.mk l key params col terms).lab = l

def AggTok.lab {T K : Type} (x : AggTok T K) : ℕ

The label of the operator that built an aggregate value.

Equations

• x.lab = x.fam.lab

The operators' labels

The hom commutation reads several values of one family in one world, so what it asks of a query is that two operators building values never share a label (AggQueryIn.labelsDistinct): values of different operators are then in different families, and an identifier determines its value across every evaluation the query performs (AggQueryIn.builds_coherent).

def labCons {α : Type} (w : ℕ) (lab : α) (L : List α) : List α

An operator's label, where it builds a column: an aggregation with no aggregate builds no value, so its label is not one of a value.

Equations

• labCons w lab L = if w = 0 then L else lab :: L

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

The labels of the operators that build aggregate values, an aggregation with no aggregate building none (labCons).

Equations

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

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

No two operators building aggregate values share a label.

Equations

• q.labelsDistinct = q.labels.Nodup

An expression's world statistics under a homomorphism

Home · Documentation · Publications · Contributors · Source · Cite