Aggregate expressions

SQL computes on the results of aggregates – count(*) + 1, x * 100 / sum(x) OVER (…), CASE WHEN sum(x) > 0 THEN … END – and so do the ranks. A term that mentions a column of aggregate kind produces a column of aggregate kind, and what that column carries is a formal aggregate expression e = g(a₁ … a_p): the function g the term computes, applied to the aggregate values a₁ … a_p of the tuple it reads. The regular values it reads are constants of g.

The worlds are the point. With U_j the occurrences of a_j and V = ⋃_j U_j, a world of e is a subfamily W ⊆ V meeting U_j for each grouped a_j – a scalar one is exempt, its empty world being one of its worlds – and the value there is g(val_{a₁}(W ∩ U₁) … val_{a_p}(W ∩ U_p)). Reading one world at a time is what makes the leaves answer together: two aggregates over the same group are read over the same occurrences, and an expression of them is not a function of their values separately.

An occurrence family is shared, so it is stored once: occs lists, per occurrence, the value every leaf reads there and the occurrence's annotation, and reads says which occurrences each leaf reads. That is V with its U_j.

Nothing asks that every occurrence be read by some leaf, and nothing may: a FILTER clause cuts what a leaf reads and never the family, because a filtered-out occurrence still witnesses its group – it belongs to V and counts in β, so that δ(β) is the group's existence and not the filtered subgroup's. An occurrence every leaf filters out is therefore a legitimate member of V, and count(*) FILTER (WHERE false) over a non-empty group returning a row with 0 is what asking otherwise would break.

AggExpr.ofValue embeds a token as the expression of itself, and AggExpr.predProv_ofValue says the embedding changes no reading: the expression of a token has the token's predicate provenance, in the token's own convention. Any deterministic function of SQL can be g, since only its value in each world is used.

structure AggExpr (T K : Type) : Type

A formal aggregate expression: a function of the aggregate values a term reads, over one shared family of occurrences.

• arity : ℕ

  How many aggregate values the expression combines.

• occs : List ((Fin self.arity → T) × K × (Fin self.arity → Bool) × (Fin self.arity → Bool))

  The occurrence family V: per occurrence, the value each leaf reads there, the occurrence's annotation, which leaves have it in their group (or frame), and which of those leaves' FILTER clauses keep it.

  The two flag families do two different jobs, and a FILTER clause is what tells them apart. The first fixes the worlds: a grouped leaf asks the world to meet its group (IsWorld), because that is what records the group's existence, and a clause does not change which rows exist. The second fixes what the leaf reads (reads, leafSeq): a clause takes an occurrence out of the aggregate's sequence while leaving it in the family, so the world in which only rejected rows are present is still a world, annotated as it should be, and the leaf reads f [] there. Cutting the family instead loses exactly that world, and no convention over the cut family recovers it (chain_count_zero_when_ne).

  Both sit in the occurrence rather than beside the list as Finsets of positions. That way a recursion over the family carries them along (AggExpr.exprProvAux) and a reading of one leaf is a List.filter of the selected sequence rather than an intersection of position sets – so nothing has to be transported when the family is rebuilt at the same length.

• aggs : Fin self.arity → SeqAggFunc T

  The aggregate each leaf reads its sequence with.

• scalar : Fin self.arity → Bool

  Whether each leaf is read in the scalar convention.

• g : (Fin self.arity → T) → T

  The function the term computes.

• fam : FamId T

  Which occurrence family the expression reads (AggValue.fam).

• oids : List (OccId T)

  The identities of its occurrences, one per element of occs, where the operator that built it records them (AggValue.oids); empty otherwise. No reading of the expression looks at them.

def AggExpr.anns {T K : Type} (e : AggExpr T K) : Fin e.occs.length → K

The occurrence annotations, as a function on positions.

Equations

• e.anns i = (e.occs.get i).2.1

def AggExpr.inFrame {T K : Type} (e : AggExpr T K) (j : Fin e.arity) : Finset (Fin e.occs.length)

The occurrences in the j-th leaf's group, read off the family: what a world has to meet for the leaf to have a value, and what the leaf's FILTER clause then cuts down to reads.

Equations

• e.inFrame j = {i : Fin e.occs.length | (e.occs.get i).2.2.1 j = true}

def AggExpr.reads {T K : Type} (e : AggExpr T K) (j : Fin e.arity) : Finset (Fin e.occs.length)

The occurrences U_j the j-th leaf reads: those of its group its own clause keeps. With no clause this is the group itself.

Equations

• e.reads j = {i : Fin e.occs.length | ((e.occs.get i).2.2.1 j && (e.occs.get i).2.2.2 j) = true}

def AggExpr.leafSeq {T K : Type} (e : AggExpr T K) (j : Fin e.arity) (W : Finset (Fin e.occs.length)) : List T

The sequence the j-th leaf reads in the world W: the values it reads at the occurrences of W it reads, in order.

Equations

• e.leafSeq j W = List.map (fun (o : (Fin e.arity → T) × K × (Fin e.arity → Bool) × (Fin e.arity → Bool)) => o.1 j) (Having.seqOf e.occs (W ∩ e.reads j))

theorem AggExpr.leafSeq_eq_filter {T K : Type} (e : AggExpr T K) (j : Fin e.arity) (W : Finset (Fin e.occs.length)) : e.leafSeq j W = List.map (fun (z : (Fin e.arity → T) × K × (Fin e.arity → Bool) × (Fin e.arity → Bool)) => z.1 j) (List.filter (fun (z : (Fin e.arity → T) × K × (Fin e.arity → Bool) × (Fin e.arity → Bool)) => z.2.2.1 j && z.2.2.2 j) (Having.seqOf e.occs W))

A leaf reads a filter of the selected sequence. With the leaf flags in the occurrences, intersecting the world with U_j and then selecting is selecting and then filtering – which is what lets a recursion over the family read every leaf as it goes.

def AggExpr.leafVal {T K : Type} (e : AggExpr T K) (j : Fin e.arity) (W : Finset (Fin e.occs.length)) : T

The value the j-th leaf takes in the world W.

Equations

• e.leafVal j W = e.aggs j (e.leafSeq j W)

def AggExpr.IsWorld {T K : Type} (e : AggExpr T K) (W : Finset (Fin e.occs.length)) : Prop

W is a world of the expression: it meets the group of every grouped leaf. A scalar leaf is exempt – the empty world is one of its worlds – which is the same case split AggValue.predProv and predProvScalar make.

It is the group and not what the leaf reads: a FILTER clause changes what the aggregate reads of a world, not which worlds there are, so a leaf whose clause rejects everything still has the worlds of its group and reads f [] in each.

Equations

• e.IsWorld W = ∀ (j : Fin e.arity), e.scalar j = false → (W ∩ e.inFrame j).Nonempty

@[instance_reducible]

instance AggExpr.instDecidablePredFinsetFinLengthProdForallArityForallBoolOccsIsWorld {T K : Type} (e : AggExpr T K) : DecidablePred e.IsWorld

Equations

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

def AggExpr.valOn {T K : Type} (e : AggExpr T K) (W : Finset (Fin e.occs.length)) : T

The value of the expression in the world W.

Equations

• e.valOn W = e.g fun (j : Fin e.arity) => e.leafVal j W

def AggExpr.collapse {T K : Type} (e : AggExpr T K) : T

The deterministic reading: every occurrence present.

Equations

• e.collapse = e.valOn Finset.univ

def AggExpr.disp {T K : Type} (e : AggExpr T K) (hTop : K → Bool) : T

The displayed value: the value of the expression in the family of its occurrences that the database as it is keeps – those whose annotation hTop maps to true. When every occurrence is annotated by sums and products of input tokens this is every occurrence, and the displayed value is the collapse; it is smaller when occurrences come through a difference or a selection on aggregate values, which are kept for the worlds where they exist and do not count in what SQL returns.

Equations

• e.disp hTop = e.valOn {i : Fin e.occs.length | hTop (e.anns i) = true}

def AggExpr.predProv {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (e : AggExpr T K) (op : CompOp) (c : T) : K

Predicate provenance of a comparison against an expression: the ⊕-sum, over the worlds of the expression, of the world's annotation times the characteristic value of the comparison there.

Equations

• e.predProv op c = ∑ W : Finset (Fin e.occs.length) with e.IsWorld W, Having.worldAnn e.anns W * Having.chi op (e.valOn W) c

def AggExpr.predProvWith {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (e : AggExpr T K) (P : T → Kleene) : K

Predicate provenance of an arbitrary three-valued test, the reading a range atom and a null test need: predProv is the case of a comparison against a constant (predProv_eq_predProvWith).

Equations

• e.predProvWith P = ∑ W : Finset (Fin e.occs.length) with e.IsWorld W, Having.worldAnn e.anns W * Having.chiOf P (e.valOn W)

The expression read as a column

An aggregate column holds one of these, so an expression owes what a token owes: the convention it is read in, the family it carries, the value it takes under a valuation of the annotations, and the values it takes over its worlds. Each is the AggValue notion with IsWorld in place of “non-empty if grouped” and the shared family in place of the token's own.

def AggExpr.isScalar {T K : Type} (e : AggExpr T K) : Bool

The convention the expression is read in: scalar exactly where every leaf is, since the empty world is a world of the expression only when no leaf demands an occurrence.

Equations

• e.isScalar = (List.finRange e.arity).all e.scalar

def AggExpr.annList {T K : Type} (e : AggExpr T K) : List K

The family the expression carries: the annotations of the shared occurrences, which is what the supersede test compares and what makes two columns one family.

Equations

• e.annList = List.map (fun (o : (Fin e.arity → T) × K × (Fin e.arity → Bool) × (Fin e.arity → Bool)) => o.2.1) e.occs

def AggExpr.realizedWorld {T K : Type} (e : AggExpr T K) (ν : K → Bool) : Finset (Fin e.occs.length)

The world a valuation of the annotations realizes: the occurrences it keeps.

Equations

• e.realizedWorld ν = {i : Fin e.occs.length | ν (e.anns i) = true}

def AggExpr.specialize {T K : Type} (e : AggExpr T K) (ν : K → Bool) : T

The world-faithful reading: the value in the realized world.

Equations

• e.specialize ν = e.valOn (e.realizedWorld ν)

def AggExpr.vals {T K : Type} [DecidableEq T] (e : AggExpr T K) : Finset T

Val(e): the values the expression takes over its worlds, for a key reading.

Equations

• e.vals = Finset.image e.valOn {W : Finset (Fin e.occs.length) | e.IsWorld W}

def AggExpr.postcomp {T K : Type} (gf : T → T) (e : AggExpr T K) : AggExpr T K

Reading the expression through a function: the term gf(e), which is again an expression over the same family.

Equations

• AggExpr.postcomp gf e = { arity := e.arity, occs := e.occs, aggs := e.aggs, scalar := e.scalar, g := fun (v : Fin e.arity → T) => gf (e.g v), fam := e.fam, oids := e.oids }

def AggExpr.mapAnn {T K K' : Type} (h : K → K') (e : AggExpr T K) : AggExpr T K'

The annotation pushforward: the occurrences keep their values, their readings and which leaves read them, their annotations going through h.

Equations

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

The world statistics of a family

What a nested value makes of one of its occurrences is a function of this: over every subfamily, the product of the annotations it keeps, the sum of those it leaves out, and the occurrences it selects read as values and leaf flags. The factor the nested world carries is the first two (NestedValue.World.ann: the product kept, times 𝟙 minus the sum left out), the value its leaf reads is a filter of the third (leafSeq_eq_filter), and whether the subfamily is a world is read off the third as well. Written as a recursion over the family rather than as a sum over subfamilies, so that a tie-block permutation of the family can be followed step by step.

def AggExpr.strip {T K : Type} {q : ℕ} (o : (Fin q → T) × K × (Fin q → Bool) × (Fin q → Bool)) : (Fin q → T) × (Fin q → Bool) × (Fin q → Bool)

An occurrence read without its annotation: what a leaf sees of it.

Equations

• AggExpr.strip o = (o.1, o.2.2)

def AggExpr.subStats {T K : Type} {q : ℕ} [CommSemiringWithMonus K] : List ((Fin q → T) × K × (Fin q → Bool) × (Fin q → Bool)) → Multiset (K × K × List ((Fin q → T) × (Fin q → Bool) × (Fin q → Bool)))

The world statistics of a family: one entry per subfamily, giving the product of the annotations kept, the sum of those left out, and the selected occurrences stripped of their annotations.

Equations

• One or more equations did not get rendered due to their size.
• AggExpr.subStats [] = {(1, 0, [])}

def AggExpr.valOfSel {T K : Type} (e : AggExpr T K) (sel : List ((Fin e.arity → T) × (Fin e.arity → Bool) × (Fin e.arity → Bool))) : T

The value an expression takes on a selected subfamily, read off the selection alone: each leaf aggregates what it reads among the selected occurrences.

Equations

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

def AggExpr.isWorldOfSel {T K : Type} (e : AggExpr T K) (sel : List ((Fin e.arity → T) × (Fin e.arity → Bool) × (Fin e.arity → Bool))) : Bool

Whether a selected subfamily is a world, read off the selection alone: every grouped leaf has an occurrence of its group among the selected.

Equations

• e.isWorldOfSel sel = decide (∀ (j : Fin e.arity), e.scalar j = false → ∃ z ∈ sel, z.2.1 j = true)

def AggExpr.worldStats {T K : Type} [CommSemiringWithMonus K] (e : AggExpr T K) : Multiset (K × K × T × Bool)

What a nested value reads of an occurrence: over every subfamily, the product of the annotations kept, the sum of those left out, the value the expression takes there and whether it is a world. The arity does not appear in the type, so two aggregate columns can be compared by it – which is what GenValue.Equiv needs for a column a nested value reads, since a nested world's weight is this and not the four readings (NestedValue.World.ann).

The fourth component is the expression's own world condition (AggExpr.IsWorld: each grouped leaf's family met by the subfamily), which is the second conjunct of NestedValue.World.IsWorldWith and so common to both readings of a nested world. It is not that comparison's parameter, which is extra, a clause on the subfamily an absent occurrence may take – nothing an inner expression alone decides.

These four are what a world of the outer family needs of this occurrence and no more – what it holds, what it leaves out, what it reads there and whether that is a reading at all – so the bag of them is the nested analogue of the single annotation an ordinary occurrence supplies. That a tie-block permutation preserves it (worldStats_congr) and that every operator's aggregate column gives it then follow from that reading, which is why the statistic is the object to compare columns by rather than one that happens to go through.

Equations

• e.worldStats = Multiset.map (fun (S : Finset (Fin e.occs.length)) => (∏ j ∈ S, e.anns j, ∑ j ∈ Sᶜ, e.anns j, e.valOn S, decide (e.IsWorld S))) Finset.univ.val

A token is the expression of itself

def AggExpr.ofValue {T K : Type} (a : AggValue T K) : AggExpr T K

The expression that reads one aggregate value and returns it.

Equations

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

theorem AggExpr.predProv_ofValue {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (a : AggValue T K) (op : CompOp) (c : T) : (ofValue a).predProv op c = a.predProvOf op c

The embedding changes no reading. The expression of a token has the token's predicate provenance, in the convention the token carries: every world where it is read scalar, the non-empty ones where it is not.

Unary expressions: a function of one aggregate value

def AggValue.postcomp {T K : Type} (gf : T → T) (a : AggValue T K) : AggValue T K

A function of one aggregate value is an aggregate value: the same occurrences, read in the same convention, with the aggregate read through gf. This is what a term mentioning one aggregate column produces – count(*) + 1, the ranks – and it is not a shortcut: valOn_ofUnary says it reads in each world what the aggregate expression gf(a) reads there, isWorld_ofUnary that it has the same worlds, and predProvWith_ofUnary that a comparison against either has the same predicate provenance.

Equations

• AggValue.postcomp gf a = { agg := fun (L : List T) => gf (a.agg L), occs := a.occs, scalar := a.scalar, fam := a.fam, oids := a.oids }

def AggExpr.ofUnary {T K : Type} (gf : T → T) (a : AggValue T K) : AggExpr T K

The unary aggregate expression gf(a): one leaf, read through gf.

Equations

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

def AggExpr.ofSeqWhen {T K : Type} [ValueType T] {c m : ℕ} (f : SeqAggFunc T) (t : TermIn T c m) (keep : Tuple T m → Bool) (U : List (AnnotatedTuple T K m)) (sc : Bool) (γ : Fin c → T := fun (x : Fin c) => 0) : AggExpr T K

A filtered aggregate of an occurrence sequence, as a one-leaf expression. The family is the whole sequence – a group, or the frame of a window – every occurrence in the leaf's group, so the worlds are the sequence's own, and what the clause cuts is what the leaf reads. The world in which only rejected rows are present is therefore a world, annotated as the group's worlds are, and the leaf reads f [] in it: the row SQL emits for a group all of whose rows the clause rejects.

This is what an AggValue cannot be. Its occurrence carries a value and an annotation, so a clause can only be applied when the token is built, cutting the family – and then that world is gone and no convention recovers it (chain_count_zero_when_ne).

Equations

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

def AggExpr.ofSeqDistWhen {T K : Type} [ValueType T] [AddCommMonoid K] {c m : ℕ} (f : SeqAggFunc T) (t : TermIn T c m) (keep : Tuple T m → Bool) (U : List (AnnotatedTuple T K m)) (sc : Bool) (γ : Fin c → T := fun (x : Fin c) => 0) : AggExpr T K

A filtered DISTINCT aggregate of an occurrence sequence. The occurrences the clause keeps are merged by value – one occurrence per class, carrying the ⊕ of its members, the classes in the domain's order, which is what AggValue.mergeOccs does and what a DISTINCT aggregate is (a deduplication annotating each distinct value by the ⊕ of its occurrences) – and read. Each rejected occurrence stays as its own occurrence, unmerged and unread.

Both halves are forced. A rejected occurrence must not join a kept class even where the values agree, since joining it would make it read; and it must stay in the family, because the family is what holds the worlds.

Equations

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

def AggExpr.distPayload {T K : Type} [ValueType T] [AddCommMonoid K] {c m : ℕ} (t : TermIn T c m) (keep : Tuple T m → Bool) (U : List (AnnotatedTuple T K m)) (γ : Fin c → T) : List (T × K)

The payload the leaf reads: the kept occurrences merged by value.

Equations

• AggExpr.distPayload t keep U γ = AggValue.mergeOccs (List.map (fun (p : AnnotatedTuple T K m) => (t.eval p.1 γ, p.2)) (List.filter (fun (p : AnnotatedTuple T K m) => keep p.1) U))

def AggExpr.ofGroupWhen {T K : Type} [ValueType T] {c m : ℕ} (f : SeqAggFunc T) (t : TermIn T c m) (keep : Tuple T m → Bool) (U : List (AnnotatedTuple T K m)) (γ : Fin c → T := fun (x : Fin c) => 0) : AggExpr T K

A filtered aggregate of a group is the grouped convention of it: the worlds are the group's non-empty subfamilies. A frame that may exclude the row it is computed for takes the scalar one, as it does with no clause.

Equations

• AggExpr.ofGroupWhen f t keep U γ = AggExpr.ofSeqWhen f t keep U false γ

Home · Documentation · Publications · Contributors · Source · Cite