Nested aggregate values

When the term of an aggregation or a window reads an aggregate column, the aggregate value it builds is nested: what it aggregates, at each of its occurrences, is not a value of the domain but another aggregate value. Its occurrences are those of its own family U together with those of the inner values, and its value in a world is the outer aggregate applied to the inner values read in that world.

An AggValue cannot hold this: its reading consults its own occurrence list alone. NestedValue carries, per outer occurrence, the inner aggregate value the term reads there, and a World chooses which outer occurrences are present and which occurrences of each inner family are. An inner value may itself be nested, to any depth: NestInner T K j is a value of storey j, an aggregate expression at storey 0 and an expression or an inner node (NestNode) above it.

Inner families are shared

Two outer occurrences may read one inner family: a join, a product or an apply repeats a row carrying an aggregate value, and a grouping over the result sees the value once per copy. The inner family is then one family, decided once in each world, not once per copy – the inner occurrences are objects, and an object is present or absent, not both. So a world decides each family once: the value's own occurrences (World.root), the positions kept of each expression family (World.leaf) and the occurrences present of each inner node (World.node), read through the decider that looks a family up by its key (World.dec); a world's annotation counts each inner occurrence once. Two inner expressions belong to one family when they carry the same family identifier and the same occurrence annotations (leafKey), which is how the joint reading of a selection groups the aggregate columns of a row (AggTok.classKey); two inner nodes, when they carry the same family identifier and the same occurrences (NestNode.key).

No sequence, and so a bag

≼ orders plain tuples, and an occurrence of a nested value carries a tuple with an aggregate column, so there is nothing to order these occurrences by: the family a nested value aggregates is a bag, and so is each inner node's. Its aggregate is accordingly a function of a bag, a world is made of bags of decisions, and worlds enumerates the worlds off those bags. Nothing indexes an occurrence, so no reading has to be shown invariant under a relisting of the family, and an operator building a nested value needs no order to list its group in – which is what it could not have, a listing of a multiset not being computable.

Which worlds count

A world meets the family of each grouped inner value that it reads, which is to say each inner value at an outer occurrence the world keeps – World.IsWorld. The condition is on the inner values read and not on all of them: an outer occurrence absent from the world contributes nothing to the value there, and asking its inner family to be met would ask a group to be non-empty while the row carrying it is absent.

This is not the condition a predicate's worlds satisfy, which meet every grouped family the predicate mentions with no such conditionality – and the difference is structural rather than an oversight. A predicate's families all belong to one tuple, which exists or does not, so demanding all of them demands that the tuple exist. A nested value's inner families each belong to outer occurrences, and the world is choosing which of those occurrences are present, so a blanket condition would quantify over occurrences the world has already excluded.

Whether a world should also be barred from meeting an inner family no present occurrence reads is settled in the negative (World.IsWorldWith sets out why); the refuted reading is kept as World.IsWorldCoherent so that its refutation can be stated.

def trW {a b : ℕ} (W : Finset (Fin a)) : Finset (Fin b)

A subfamily of one listing of a family read in another: the positions with the same index.

Equations

• trW W = {i : Fin b | ∃ j ∈ W, ↑j = ↑i}

Storeys

A nested value reads, at each of its occurrences, an inner value that may itself be nested. The types say how deep: NestInner T K j is what an occurrence of a value of storey j reads – at storey 0 an aggregate expression, at storey j + 1 either something storey j reads or a node of storey j, an outer aggregate over a bag of occurrences reading storey-j values. A node can only hold inner values of lower storeys, which is what makes every reading a recursion on the storey.

structure NestNode (T K X : Type) : Type

A node of a nested value: an outer aggregate over a bag of occurrences, each carrying what it reads (of type X) and its annotation.

• agg : Multiset T → T

  The outer aggregate, as a function of a bag. It cannot read a sequence: the order ≼ is an order on plain tuples, and an occurrence of a nested value carries a tuple with an aggregate column, so there is no sequence for an order-dependent aggregate to read. An ordinary aggregate becomes one of these when it is symmetric (SeqAggFunc.onBag), and an order-dependent outer aggregate has no nested reading at all – it goes through the alternatives (AggQueryIn.Explode), after which nothing is nested.

• occs : Multiset (X × K)

  The occurrences: per occurrence, what the term reads there and the occurrence's own annotation. A bag, for the reason the aggregate is a function of one – nothing orders a tuple with an aggregate column.

• scalar : Bool

  Whether the outer reading is scalar – whether the empty world is one of its worlds.

• fam : FamId T

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

def NestInner (T K : Type) : ℕ → Type

What an occurrence of a nested value of storey j reads. At storey 0, an aggregate expression: a term over several aggregate columns is one – sum(c₁ - c₂) over a block with two counts is as ordinary as avg(c) over one – and an ordinary token embeds as the expression of itself (AggExpr.ofValue). At storey j + 1, what storey j reads, or a node of storey j.

Equations

• NestInner T K 0 = AggExpr T K
• NestInner T K j.succ = (NestInner T K j ⊕ NestNode T K (NestInner T K j))

structure NestedValue (T K : Type) : Type

A nested aggregate value: a node of some storey. Storey 0 is a value whose occurrences read aggregate expressions; storey j + 1 one whose occurrences may read nested values of storey j and below.

• lev : ℕ

  The storey.

• agg : Multiset T → T

  The outer aggregate (NestNode.agg).

• occs : Multiset (NestInner T K self.lev × K)

  The occurrences (NestNode.occs).

• scalar : Bool

  Whether the outer reading is scalar.

• fam : FamId T

  Which occurrence family the value reads.

Which occurrences are one

A nested value's occurrences are its own and those of every value it reads, at every storey, and an occurrence is one object however many times it is read. Two outer occurrences may read one inner family: a join, a product or an apply repeats a row carrying an aggregate value, and a grouping over the result sees the value once per copy. The inner family is then one family, decided once in each world – the inner occurrences are objects, and an object is present or absent, not both. The same holds one storey up: a nested value repeated by a join, then read by a second-level grouping, has its occurrences decided once.

So a world decides each family once. An aggregate expression's family is keyed by its family identifier and its annotations (leafKey) – the key a joint reading groups a row's aggregate columns by (AggTok.classKey); a node's occurrences by its family identifier and the occurrences themselves (NestNode.key).

@[reducible, inline]

abbrev LeafKey (T K : Type) : Type

The key of an expression's family: its family identifier and its occurrence annotations.

Equations

• LeafKey T K = ((ℕ × List T × List (T ⊕ FamId T)) × List K)

def leafKey {T K : Type} (e : AggExpr T K) : LeafKey T K

The key of an expression's family.

Equations

• leafKey e = (e.fam.family, e.annList)

@[reducible, inline]

abbrev NodeKey (T K : Type) (j : ℕ) : Type

The key of a node's occurrences: its family identifier and its occurrences.

Equations

• NodeKey T K j = ((ℕ × List T × List (T ⊕ FamId T)) × Multiset (NestInner T K j × K))

def NestNode.key {T K : Type} {j : ℕ} (N : NestNode T K (NestInner T K j)) : NodeKey T K j

The key of a node's occurrences.

Equations

• N.key = (N.fam.family, N.occs)

@[instance_reducible]

instance instDecidableEqLeafKey {T K : Type} [DecidableEq T] [DecidableEq K] : DecidableEq (LeafKey T K)

Equations

• instDecidableEqLeafKey = instDecidableEqProd

def NestInner.leaves {T K : Type} (j : ℕ) : NestInner T K j → Multiset (LeafKey T K)

The expression families an inner value reads, with repetition.

Equations

• NestInner.leaves 0 e = {leafKey e}
• NestInner.leaves j.succ (Sum.inl x_2) = NestInner.leaves j x_2
• NestInner.leaves j.succ (Sum.inr N) = N.occs.bind fun (o : NestInner T K j × K) => NestInner.leaves j o.1

def NestInner.nodes {T K : Type} (j : ℕ) : NestInner T K j → Multiset ((i : ℕ) × NodeKey T K i)

The nodes an inner value reads, each with its storey, with repetition.

Equations

• NestInner.nodes 0 e = 0
• NestInner.nodes j.succ (Sum.inl x_2) = NestInner.nodes j x_2
• NestInner.nodes j.succ (Sum.inr N) = ⟨j, N.key⟩ ::ₘ N.occs.bind fun (o : NestInner T K j × K) => NestInner.nodes j o.1

def NestInner.collapse {T K : Type} (j : ℕ) : NestInner T K j → T

The deterministic reading: every occurrence present.

Equations

• NestInner.collapse 0 e = AggExpr.collapse e
• NestInner.collapse j.succ (Sum.inl x_2) = NestInner.collapse j x_2
• NestInner.collapse j.succ (Sum.inr N) = N.agg (Multiset.map (fun (o : NestInner T K j × K) => NestInner.collapse j o.1) N.occs)

def NestedValue.toNode {T K : Type} (a : NestedValue T K) : NestNode T K (NestInner T K a.lev)

The value as a node of its storey.

Equations

• a.toNode = { agg := a.agg, occs := a.occs, scalar := a.scalar, fam := a.fam }

def NestedValue.ofNode {T K : Type} {j : ℕ} (N : NestNode T K (NestInner T K j)) : NestedValue T K

The value of a node of storey j.

Equations

• NestedValue.ofNode N = { lev := j, agg := N.agg, occs := N.occs, scalar := N.scalar, fam := N.fam }

def NestedValue.ofOccs {T K : Type} (agg : Multiset T → T) {j : ℕ} (U : Multiset (NestInner T K j × K)) (scalar : Bool) (fam : FamId T) : NestedValue T K

The nested value of a bag of occurrences.

Equations

• NestedValue.ofOccs agg U scalar fam = { lev := j, agg := agg, occs := U, scalar := scalar, fam := fam }

def NestedValue.leaves {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) : Multiset (LeafKey T K)

The expression families of a nested value, each once.

Equations

• a.leaves = (a.occs.bind fun (o : NestInner T K a.lev × K) => NestInner.leaves a.lev o.1).dedup

noncomputable def NestedValue.nodes {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) : Multiset ((i : ℕ) × NodeKey T K i)

The inner nodes of a nested value, each once. Two nodes are one when their keys are, and a key carries inner values, so they are compared classically: a value of storey 0 has no inner node, and nothing is compared there.

Equations

• a.nodes = (a.occs.bind fun (o : NestInner T K a.lev × K) => NestInner.nodes a.lev o.1).dedup

def NestedValue.collapse {T K : Type} (a : NestedValue T K) : T

The deterministic reading: the outer aggregate of the inner collapses.

Equations

• a.collapse = a.agg (Multiset.map (fun (o : NestInner T K a.lev × K) => NestInner.collapse a.lev o.1) a.occs)

Reading under a decision

A world is a decision about every occurrence a value holds. The readings are written against a decider – what is kept of each expression family (by position) and of each node's occurrences (each with a presence flag) – so that a world read off the enumeration and the world a valuation cuts out are read by one recursion.

structure NestDec (T K : Type) : Type

A decision about every family: the positions kept of each expression family, and of each node's occurrences, each with whether it is present.

• leaf : LeafKey T K → Finset ℕ

  The positions kept of an expression family.

• node (j : ℕ) : NodeKey T K j → Multiset (NestInner T K j × K × Bool)

  The occurrences of a node, each with whether it is present.

def trS {n : ℕ} (S : Finset ℕ) : Finset (Fin n)

A set of positions, read on a family of a given length.

Equations

• trS S = {i : Fin n | ↑i ∈ S}

def NestInner.val {T K : Type} (D : NestDec T K) (j : ℕ) : NestInner T K j → T

The value an inner value reads under a decision.

Equations

• One or more equations did not get rendered due to their size.
• NestInner.val D 0 e = AggExpr.valOn e (trS (D.leaf (leafKey e)))
• NestInner.val D j.succ (Sum.inl x_2) = NestInner.val D j x_2

def NestInner.ok {T K : Type} (D : NestDec T K) (j : ℕ) : NestInner T K j → Prop

Whether a decision is a world of an inner value: each expression family it reads met where its leaves are grouped (AggExpr.IsWorld), and each node it reads met unless scalar – and, of each node, only the occurrences the decision keeps are asked anything. The condition is one-directional: a present occurrence asks its inner family to be met, a met inner family does not make an occurrence present.

Equations

• NestInner.ok D 0 e = AggExpr.IsWorld e (trS (D.leaf (leafKey e)))
• NestInner.ok D j.succ (Sum.inl x_2) = NestInner.ok D j x_2
• NestInner.ok D j.succ (Sum.inr N) = ((N.scalar = true ∨ ∃ m ∈ D.node j N.key, m.2.2 = true) ∧ ∀ m ∈ D.node j N.key, m.2.2 = true → NestInner.ok D j m.1)

def NestInner.decOk {T K : Type} (D : NestDec T K) (j : ℕ) (x : NestInner T K j) : Decidable (ok D j x)

Whether a decision is a world of an inner value is decidable.

Equations

• One or more equations did not get rendered due to their size.
• NestInner.decOk D j.succ (Sum.inl x_2) = NestInner.decOk D j x_2

@[instance_reducible]

instance NestInner.instDecidableOk {T K : Type} (D : NestDec T K) (j : ℕ) (x : NestInner T K j) : Decidable (ok D j x)

Equations

• NestInner.instDecidableOk D j x = NestInner.decOk D j x

Worlds

A world of a nested value decides its own occurrences (root), each expression family once (leaf, the positions kept) and each inner node once (node, its occurrences with presence flags). It is read through the decider looking each family up by its key.

structure NestedValue.World (T K : Type) (d : ℕ) : Type

A world of a nested value of storey d.

• root : Multiset (NestInner T K d × K × Bool)

  The value's own occurrences, each with whether it is present.

• leaf : Multiset (LeafKey T K × Finset ℕ)

  Each expression family, with the positions kept.

• node : Multiset ((j : ℕ) × NodeKey T K j × Multiset (NestInner T K j × K × Bool))

  Each inner node, with its occurrences and whether each is present.

def NestedValue.leafSub {T K : Type} [DecidableEq T] [DecidableEq K] (L : Multiset (LeafKey T K × Finset ℕ)) (κ : LeafKey T K) : Finset ℕ

The positions an expression family keeps, looked up by key.

Equations

• NestedValue.leafSub L κ = (Multiset.map Prod.snd (Multiset.filter (fun (e : LeafKey T K × Finset ℕ) => e.1 = κ) L)).sup

noncomputable def NestedValue.nodeDec {T K : Type} (N : Multiset ((j : ℕ) × NodeKey T K j × Multiset (NestInner T K j × K × Bool))) (j : ℕ) (κ : NodeKey T K j) : Multiset (NestInner T K j × K × Bool)

The decision about a node's occurrences, looked up by key.

Equations

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

noncomputable def NestedValue.World.dec {T K : Type} [DecidableEq T] [DecidableEq K] {d : ℕ} (W : World T K d) : NestDec T K

The decider a world reads by.

Equations

• W.dec = { leaf := NestedValue.leafSub W.leaf, node := NestedValue.nodeDec W.node }

noncomputable def NestedValue.World.kept {T K : Type} [DecidableEq T] [DecidableEq K] {d : ℕ} (W : World T K d) : Multiset T

The inner values a world reads: one per outer occurrence it keeps. The outer family is met when this is not empty, and the value read in the world is the outer aggregate of it.

Equations

• W.kept = Multiset.map (fun (m : NestInner T K d × K × Bool) => NestInner.val W.dec d m.1) (Multiset.filter (fun (m : NestInner T K d × K × Bool) => m.2.2 = true) W.root)

def NestedValue.World.IsWorldOf {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) (W : World T K a.lev) : Prop

Whose world it is: it decides on exactly the value's own occurrences, expression families and inner nodes, each family's kept positions among its own.

Equations

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

def NestedValue.World.IsWorldWith {T K : Type} [DecidableEq T] [DecidableEq K] {d : ℕ} (W : World T K d) (a : NestedValue T K) (extra : World T K d → Prop) : Prop

Admissibility, with the coherence condition as a parameter. extra is the clause asking whether a world is barred from meeting an inner family no present occurrence reads. The reading is IsWorld, extra vacuous: barring it is not a convention but wrong.

Why: the world a valuation realizes sets an occurrence present exactly when the valuation makes its outer annotation true, and keeps the inner occurrences it makes true, independently (realizedWorld). A selection on an aggregate value brings a failing group's row to 𝟘 while its aggregate column stays realized, so the actual world keeps the inner occurrences of an absent outer one. Barring that configuration removes the world as it is: over 𝔹 the two readings give ⊤ and 𝟘 on nestedIncoherentWitness (in HavingQueryCounterexamples; nestedIncoherent_ne_coherent, realizedWorld_not_coherent), so a coherent reading would contradict World.ann_eval_iff and the possible-world results resting on it.

The condition is one-directional and must be: a present outer occurrence needs its inner family met, but a met family does not make its occurrence present. The parameter stays because it is what the two readings are compared through.

Equations

• W.IsWorldWith a extra = ((a.scalar = true ∨ 0 < W.kept.card) ∧ (∀ m ∈ W.root, m.2.2 = true → NestInner.ok W.dec d m.1) ∧ extra W)

def NestedValue.World.IsWorld {T K : Type} [DecidableEq T] [DecidableEq K] {d : ℕ} (W : World T K d) (a : NestedValue T K) : Prop

The worlds a nested value admits: the outer family met unless the reading is scalar, and, of each inner value the world reads, its own world condition (NestInner.ok) – each grouped expression family met, each grouped node met, recursively along the occurrences kept.

Equations

• W.IsWorld a = W.IsWorldWith a fun (x : NestedValue.World T K d) => True

def NestedValue.World.IsWorldCoherent {T K : Type} [DecidableEq T] [DecidableEq K] {d : ℕ} (W : World T K d) (a : NestedValue T K) : Prop

The reading that bars a world from meeting an expression family no present occurrence of the value reads directly. Refuted, not an alternative: it removes the world a valuation realizes where a selection has brought an outer annotation to 𝟘, which IsWorldWith's docstring sets out. Kept so that the refutation can be stated.

Equations

• W.IsWorldCoherent a = W.IsWorldWith a fun (W : NestedValue.World T K d) => ∀ e ∈ W.leaf, (∀ m ∈ W.root, m.2.2 = true → e.1 ∉ NestInner.leaves d m.1) → e.2 = ∅

@[instance_reducible]

noncomputable instance NestedValue.instDecidableIsWorld {T K : Type} [DecidableEq T] [DecidableEq K] {d : ℕ} (W : World T K d) (a : NestedValue T K) : Decidable (W.IsWorld a)

Equations

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

noncomputable def NestedValue.valOn {T K : Type} [DecidableEq T] [DecidableEq K] {d : ℕ} (a : NestedValue T K) (W : World T K d) : T

The value of a nested aggregate in a world: the outer aggregate of the bag of inner values read there.

Equations

• a.valOn W = a.agg W.kept

Looking a family up

Reading with the support fixed

What an inner value reads depends on the decision only at the families it reads.

def NestInner.fullDec {T K : Type} : NestDec T K

The full decision: everything kept.

Equations

• NestInner.fullDec = { leaf := fun (κ : LeafKey T K) => Finset.range κ.2.length, node := fun (x : ℕ) (κ : NodeKey T K x) => Multiset.map (fun (o : NestInner T K x × K) => (o.1, o.2, true)) κ.2 }

def NestInner.realDec {T K : Type} (ν : K → Bool) : NestDec T K

The decision a valuation of the annotations makes: it keeps the occurrences, of every family and every node, whose annotations it makes true.

Equations

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

def NestInner.specialize {T K : Type} (ν : K → Bool) (j : ℕ) (x : NestInner T K j) : T

The world-faithful reading of an inner value under a valuation.

Equations

• NestInner.specialize ν j x = NestInner.val (NestInner.realDec ν) j x

The worlds of a nested value, enumerated

The worlds are the decisions one can make about each family – at each of the value's own occurrences and each inner node's, present or not; at each expression family, which positions are kept – so they are built by running over the families and letting every world so far gain every decision available at the next one. Everything is a bag and the construction has to be read off it rather than off a listing, which is what the steps being left-commutative says – and the multiplicities are kept: two occurrences carrying the same inner value and the same annotation are two occurrences, and a world may keep one and drop the other.

def NestedValue.addMem {K X : Type} (o : X × K) (acc : Multiset (Multiset (X × K × Bool))) : Multiset (Multiset (X × K × Bool))

The presence decisions over a bag of occurrences.

Equations

• NestedValue.addMem o acc = {true, false}.bind fun (b : Bool) => Multiset.map (fun (ms : Multiset (X × K × Bool)) => (o.1, o.2, b) ::ₘ ms) acc

instance NestedValue.instLeftCommutativeProdMultisetBoolAddMem {K X : Type} : LeftCommutative addMem

def NestedValue.memChoices {K X : Type} (M : Multiset (X × K)) : Multiset (Multiset (X × K × Bool))

Every choice of presence over a bag of occurrences.

Equations

• NestedValue.memChoices M = Multiset.foldr NestedValue.addMem {0} M

def NestedValue.addLeaf {T K : Type} (κ : LeafKey T K) (acc : Multiset (Multiset (LeafKey T K × Finset ℕ))) : Multiset (Multiset (LeafKey T K × Finset ℕ))

The positions one can keep of an expression family.

Equations

• NestedValue.addLeaf κ acc = (Finset.range κ.2.length).powerset.val.bind fun (S : Finset ℕ) => Multiset.map (fun (x : Multiset (LeafKey T K × Finset ℕ)) => (κ, S) ::ₘ x) acc

instance NestedValue.instLeftCommutativeLeafKeyMultisetProdFinsetNatAddLeaf {T K : Type} : LeftCommutative addLeaf

def NestedValue.addNode {T K : Type} (κ : (j : ℕ) × NodeKey T K j) (acc : Multiset (Multiset ((j : ℕ) × NodeKey T K j × Multiset (NestInner T K j × K × Bool)))) : Multiset (Multiset ((j : ℕ) × NodeKey T K j × Multiset (NestInner T K j × K × Bool)))

The decisions one can make about a node's occurrences.

Equations

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

instance NestedValue.instLeftCommutativeSigmaNatNodeKeyMultisetProdNestInnerBoolAddNode {T K : Type} : LeftCommutative addNode

noncomputable def NestedValue.worlds {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) : Multiset (World T K a.lev)

The worlds of a nested value.

Equations

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

What a world of a nested value is annotated

The annotation is the one every family gets: the product of what is present times 𝟙 ⊖ the sum of what is absent – the value's own occurrences, each expression family once and each inner node's occurrences once, however many occurrences read them, at every storey together. It does not depend on which worlds are admitted, that being a separate question from how a given one is weighed.

def NestedValue.decProd {K : Type} [CommSemiringWithMonus K] {X : Type} (D : Multiset (X × K × Bool)) : K

What a decision over a bag of occurrences keeps.

Equations

• NestedValue.decProd D = (Multiset.map (fun (m : X × K × Bool) => if m.2.2 = true then m.2.1 else 1) D).prod

def NestedValue.decAbs {K : Type} [CommSemiringWithMonus K] {X : Type} (D : Multiset (X × K × Bool)) : K

What a decision over a bag of occurrences leaves out.

Equations

• NestedValue.decAbs D = (Multiset.map (fun (m : X × K × Bool) => if m.2.2 = true then 0 else m.2.1) D).sum

def NestedValue.leafProd {T K : Type} [CommSemiringWithMonus K] (e : LeafKey T K × Finset ℕ) : K

What a decision about an expression family keeps.

Equations

• NestedValue.leafProd e = ∏ i ∈ e.2, e.1.2.getD i 0

def NestedValue.leafAbs {T K : Type} [CommSemiringWithMonus K] (e : LeafKey T K × Finset ℕ) : K

What a decision about an expression family leaves out.

Equations

• NestedValue.leafAbs e = ∑ i ∈ Finset.range e.1.2.length \ e.2, e.1.2.getD i 0

def NestedValue.World.presentProd {T K : Type} [CommSemiringWithMonus K] {d : ℕ} (W : World T K d) : K

The product of the annotations a world keeps.

Equations

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

def NestedValue.World.absentSum {T K : Type} [CommSemiringWithMonus K] {d : ℕ} (W : World T K d) : K

The sum of the annotations a world leaves out.

Equations

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

def NestedValue.World.ann {T K : Type} [CommSemiringWithMonus K] {d : ℕ} (W : World T K d) : K

The annotation of a world of a nested value.

Equations

• W.ann = W.presentProd * (1 - W.absentSum)

Worlds built from a decision

The full world and the realized one are each a decision applied to every family the value holds (World.ofDec), which a world reads back exactly where the value reads.

noncomputable def NestedValue.World.ofDec {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) (R : Multiset (NestInner T K a.lev × K × Bool)) (D : NestDec T K) : World T K a.lev

The world a decision makes of a value: its own occurrences decided by R, and every family by D.

Equations

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

noncomputable def NestedValue.World.full {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) : World T K a.lev

The world in which every occurrence, outer and inner, is present.

Equations

• NestedValue.World.full a = NestedValue.World.ofDec a (Multiset.map (fun (o : NestInner T K a.lev × K) => (o.1, o.2, true)) a.occs) NestInner.fullDec

noncomputable def NestedValue.realizedWorld {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) (ν : K → Bool) : World T K a.lev

The world a valuation of the annotations realizes: every occurrence, of the value, of each expression family and of each inner node, whose annotation the valuation makes true – the outer and the inner ones independently.

Equations

• a.realizedWorld ν = NestedValue.World.ofDec a (Multiset.map (fun (o : NestInner T K a.lev × K) => (o.1, o.2, ν o.2)) a.occs) (NestInner.realDec ν)

noncomputable def NestedValue.specialize {T K : Type} [DecidableEq T] [DecidableEq K] (a : NestedValue T K) (ν : K → Bool) : T

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

Equations

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

The readings over the nested worlds

With the world set fixed – the coherence clause not imposed – the readings a nested value owes can be written: the predicate provenance of a test of its value, and the values it takes. Both are the AggValue ones with World in place of a subfamily and World.ann in place of Having.worldAnn, and the sum runs over the enumerated worlds.

noncomputable def NestedValue.predProvWith {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (a : NestedValue T K) (P : T → Kleene) : K

The predicate provenance of a test of a nested value: the ⊕ over its worlds of the world's annotation times the truth of the test there.

Equations

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

noncomputable def NestedValue.predProvOf {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (a : NestedValue T K) (op : CompOp) (c : T) : K

The comparison case.

Equations

• a.predProvOf op c = a.predProvWith fun (v : T) => op.eval3 v c

noncomputable def NestedValue.vals {T K : Type} [ValueType T] [DecidableEq K] (a : NestedValue T K) : Finset T

The values a nested value takes over its worlds, for a key reading.

Equations

• a.vals = (Multiset.map a.valOn (Multiset.filter (fun (W : NestedValue.World T K a.lev) => W.IsWorld a) a.worlds)).toFinset

theorem NestedValue.predProvWith_delta_absorb {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (a : NestedValue T K) (hsc : a.scalar = false) (P : T → Kleene) : a.predProvWith P * SemiringWithMonus.delta (Multiset.map Prod.snd a.occs).sum = a.predProvWith P

A nested value's predicate provenance absorbs the δ-guard of its own outer family, provided the reading is grouped – which is what makes every admissible world keep an occurrence, so that one occurrence annotation is there to swallow δ of the family's sum. Where the reading is scalar the empty world is a world and there is nothing to absorb with.

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

Reading a nested value's aggregate through a function – what a term over the aggregate column it produces reads. The occurrences, the convention and so the worlds are untouched, so every reading is the reading of the value, read through gf.

Equations

• NestedValue.postcomp gf a = { lev := a.lev, agg := fun (s : Multiset T) => gf (a.agg s), occs := a.occs, scalar := a.scalar, fam := a.fam }

The pushforward of the annotations

Changing the annotation semiring moves no value and no occurrence: each inner value keeps its occurrences and each node its own. Only the annotations travel.

def NestInner.mapAnn {T K K' : Type} (h : K → K') (j : ℕ) : NestInner T K j → NestInner T K' j

The pushforward of an inner value.

Equations

• One or more equations did not get rendered due to their size.
• NestInner.mapAnn h 0 e = AggExpr.mapAnn h e
• NestInner.mapAnn h j.succ (Sum.inl x_2) = Sum.inl (NestInner.mapAnn h j x_2)

def NestedValue.mapAnn {T K K' : Type} (h : K → K') (a : NestedValue T K) : NestedValue T K'

The pushforward of a nested value: both the inner values and the outer annotations go through h.

Equations

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

Nothing nested: the degenerate case

A nested value whose inner values read nothing is an ordinary aggregate value, and it had better be annotated like one. constInner v is the inner value that reads no occurrence and returns v; ofAggValue builds the nested value of a token by putting one at each of its occurrences, all reading the one empty family, and ann_worldOf says a world of it carries exactly Having.worldAnn of the token's own family.

def NestedValue.constInner {T K : Type} (v : T) : AggExpr T K

The inner reading that reads nothing and returns v: the expression of the token with no occurrence whose aggregate is v. Its only world is the empty one, and it contributes no occurrence.

Equations

• NestedValue.constInner v = AggExpr.ofValue { agg := fun (x : List T) => v, occs := [], scalar := true, fam := FamId.none }

def NestedValue.ofAggValue {T K : Type} (a : AggValue T K) (hsym : a.agg.Symmetric) : NestedValue T K

The nested value of an ordinary token: nothing is nested, each occurrence carrying a value rather than a family. The token's aggregate has to be symmetric to be the outer one, a nested value's aggregate being a function of the bag.

Equations

• NestedValue.ofAggValue a hsym = { lev := 0, agg := a.agg.onBag ⋯, occs := ↑(List.map (fun (o : T × K) => (NestedValue.constInner o.1, o.2)) a.occs), scalar := a.scalar, fam := a.fam }

def NestedValue.worldOf {T K : Type} [DecidableEq T] [DecidableEq K] (a : AggValue T K) (W : Finset (Fin a.occs.length)) : World T K 0

A world of an unnested token, as a world of its nested form: the one empty inner family, and the occurrences the subfamily keeps.

Equations

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

The aggregate side of a lifted value

A column of aggregate kind holds an ordinary token, a nested one or an aggregate expression. AggTok is that choice, and GenValue is built on it, so an ordinary token keeps its type and everything already proved about AggValue applies to the tok case unchanged. The nest case has its own readings: the pushforward keeps the values the column takes (AggTok.vals_mapAnn), and the hom commutation relates two nested values family by family (NestInner.Rel), their world enumerations being images of one index bag (wcorr_of_rel). It also absorbs the δ-guard of its own family (NestedValue.predProvWith_delta_absorb), which is what the evaluator's supersede bookkeeping needs, and over 𝔹[X] only the world a valuation cuts out is annotated true (NestedValue.World.ann_eval_iff), which is what the random-world reading needs. So the results of the metatheory ask nothing of the kind of token a column holds; the one-token mapAnn commutations (AggTok.predProvOf_mapAnn and its siblings) ask isNested = false, and nothing downstream reads them on a nested column. What a result may exclude is the operator that builds one – second-level aggregation, AggQueryIn.GammaNest – and it does that with AggQueryIn.noGammaNest, not with a condition on the column; GenRow.NoNested is what AggQueryIn.evaluate_noNested gives a query that has no such operator.

inductive AggTok (T K : Type) : Type

An aggregate column's value: an ordinary token, or a nested one whose occurrences include those of the aggregate values its term read.

• tok {T K : Type} : AggValue T K → AggTok T K

  An ordinary aggregate value.

• nest {T K : Type} : NestedValue T K → AggTok T K

  A nested one.

• expr {T K : Type} : AggExpr T K → AggTok T K

  An aggregate expression: a function of several aggregate values over one shared family of occurrences, which is what a term over more than one aggregate column produces. A term over one stays a tok, post-composed, since AggValue.postcomp represents that case already and keeping it spares the metatheory a case.

def AggTok.fam {T K : Type} : AggTok T K → FamId T

The occurrence family the value reads (AggValue.fam).

Equations

• (AggTok.tok a).fam = a.fam
• (AggTok.nest a).fam = a.fam
• (AggTok.expr a).fam = a.fam

def AggTok.setFam {T K : Type} (φ : FamId T) (ids : Option (List (OccId T)) := none) : AggTok T K → AggTok T K

The value, read as one of the family φ: what the operator that computes it stamps on it. Nothing else changes.

Equations

• AggTok.setFam φ ids (AggTok.tok a) = AggTok.tok { agg := a.agg, occs := a.occs, scalar := a.scalar, fam := φ, oids := ids.getD a.oids }
• AggTok.setFam φ ids (AggTok.nest a) = AggTok.nest { lev := a.lev, agg := a.agg, occs := a.occs, scalar := a.scalar, fam := φ }
• AggTok.setFam φ ids (AggTok.expr a) = AggTok.expr { arity := a.arity, occs := a.occs, aggs := a.aggs, scalar := a.scalar, g := a.g, fam := φ, oids := ids.getD a.oids }

def AggTok.collapse {T K : Type} : AggTok T K → T

The deterministic reading.

Equations

• (AggTok.tok a).collapse = a.collapse
• (AggTok.nest a).collapse = a.collapse
• (AggTok.expr a).collapse = a.collapse

def AggTok.scalar {T K : Type} : AggTok T K → Bool

Whether the value is read in the scalar convention.

Equations

• (AggTok.tok a).scalar = a.scalar
• (AggTok.nest a).scalar = a.scalar
• (AggTok.expr a).scalar = a.isScalar

def AggTok.annList {T K : Type} [AddCommMonoid K] : AggTok T K → List K

The occurrence-annotation list. It is what the evaluator's supersede test compares, and what makes a family.

A nested value's family is a bag of annotations, which no sequence lists, so what is given here is the single annotation it sums to – what a guard reads of a family (δ of its ⊕) and no more. The supersede test therefore compares a nested token's family coarsely: it matches a pending group factor only when that factor is that one sum. Comparing the bag itself is what the test would have to do, and is what annList owes once an operator builds a nested token; nothing depends on it in the meantime, nested tokens being excluded from the metatheory that runs the test (GenRow.NoNested).

Equations

• (AggTok.tok a).annList = List.map Prod.snd a.occs
• (AggTok.nest a).annList = [(Multiset.map Prod.snd a.occs).sum]
• (AggTok.expr a).annList = a.annList

def AggTok.isNested {T K : Type} : AggTok T K → Bool

Whether the value is nested.

Equations

• (AggTok.tok a).isNested = false
• (AggTok.nest a).isNested = true
• (AggTok.expr a).isNested = false

def AggTok.isTok {T K : Type} : AggTok T K → Bool

Whether the column holds an ordinary aggregate value. The readings that cover neither a nested value nor an expression over several of them require this; it is a statement about the proofs and not about the definitions, and AggQueryIn.evaluate_ordinaryTokens discharges it for every row of a query with no multi-frame window and no second-level aggregation.

Equations

• (AggTok.tok a).isTok = true
• (AggTok.nest a).isTok = false
• (AggTok.expr a).isTok = false

Lifted values over the widened token

AggValue.collapseSum and AggValue.mapAnnSum keep their names and their meaning; only the token they range over is the widened one. An ordinary token coerces into it, so a lifted value is still written Sum.inr a.

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

Push the annotations forward through a token, ordinary or nested.

Equations

• AggTok.mapAnn h (AggTok.tok a) = AggTok.tok (AggValue.mapAnn h a)
• AggTok.mapAnn h (AggTok.nest a) = AggTok.nest (NestedValue.mapAnn h a)
• AggTok.mapAnn h (AggTok.expr a) = AggTok.expr (AggExpr.mapAnn h a)

The readings, on each kind of token

Each reading delegates: to AggValue on an ordinary token, to NestedValue on a nested one – over World.IsWorld, the admitted world set – and to AggExpr on an expression, whose worlds are the subfamilies of the shared family meeting every grouped leaf. So the definitions cover all three kinds; what the metatheory proves beyond an ordinary token it fences with AggTok.isTok, which is a statement about the proofs and not about the definitions.

noncomputable def AggTok.predProvOfWith {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (P : T → Kleene) : AggTok T K → K

The predicate provenance of a comparison against the token, in its own convention. On a nested token it is the sum over the nested worlds.

Equations

• AggTok.predProvOfWith P (AggTok.tok a) = a.predProvOfWith P
• AggTok.predProvOfWith P (AggTok.nest a) = a.predProvWith P
• AggTok.predProvOfWith P (AggTok.expr a) = a.predProvWith P

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

Read the token's aggregate through a function – what a term over one aggregate column produces.

Equations

• AggTok.postcomp gf (AggTok.tok a) = AggTok.tok { agg := fun (L : List T) => gf (a.agg L), occs := a.occs, scalar := a.scalar, fam := a.fam, oids := a.oids }
• AggTok.postcomp gf (AggTok.nest a) = AggTok.nest (NestedValue.postcomp gf a)
• AggTok.postcomp gf (AggTok.expr a) = AggTok.expr (AggExpr.postcomp gf a)

noncomputable def AggTok.predProvOf {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (op : CompOp) (c : T) (x : AggTok T K) : K

The comparison case.

Equations

• AggTok.predProvOf op c x = AggTok.predProvOfWith (fun (v : T) => op.eval3 v c) x

noncomputable def AggTok.specialize {T K : Type} [ValueType T] [DecidableEq K] (ν : K → Bool) : AggTok T K → T

The world-faithful reading under a valuation of the annotations. On a nested token it is the value in the world the valuation realizes, inner occurrences included.

Equations

• AggTok.specialize ν (AggTok.tok a) = a.specialize ν
• AggTok.specialize ν (AggTok.nest a) = a.specialize ν
• AggTok.specialize ν (AggTok.expr a) = a.specialize ν

noncomputable def AggTok.vals {T K : Type} [ValueType T] [DecidableEq K] : AggTok T K → Finset T

The values the token takes over its worlds, for a key reading – the nested worlds on a nested token.

Equations

• (AggTok.tok a).vals = a.vals
• (AggTok.nest a).vals = a.vals
• (AggTok.expr a).vals = a.vals

noncomputable def AggTok.altProv {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (x : AggTok T K) (v : T) : K

[a ≐ v].

Equations

• x.altProv v = AggTok.predProvOfWith (fun (y : T) => CompOp.syneq.eval3 y v) x

The pushforward, token by token

Pushing the annotations forward leaves everything the metatheory reads off a column but the annotations themselves: which kind of token it is, the convention it is read in and the values it takes. The last is stated away from a nested token, whose values are the one reading still unproved.

theorem AggTok.vals_mapAnn {T K : Type} [ValueType T] [DecidableEq K] {K' : Type} [CommSemiringWithMonus K'] [DecidableEq K'] (f : K → K') (x : AggTok T K) (hx : x.isNested = false) : (mapAnn f x).vals = x.vals

The values a column takes survive the pushforward, on a token that is not nested.

The family a value is stamped with

No reading of a value looks at its family: stamping one changes which values a predicate reads together, and nothing about any one of them.

def AggValue.collapseSum {T K : Type} : T ⊕ AggTok T K → T

The deterministic reading of a lifted value.

Equations

• AggValue.collapseSum = Sum.elim id AggTok.collapse

def AggValue.eraseFamSum {T K : Type} : T ⊕ AggTok T K → T ⊕ AggTok T K

A lifted value with its family forgotten: what two queries that compute the same values through different operators agree on.

Equations

• AggValue.eraseFamSum = Sum.map id fun (a : AggTok T K) => AggTok.setFam FamId.none (some []) a

def AggValue.mapAnnSum {T K K' : Type} (h : K → K') : T ⊕ AggTok T K → T ⊕ AggTok T K'

The annotation pushforward on a lifted value.

Equations

• AggValue.mapAnnSum h = Sum.map id (AggTok.mapAnn h)

Home · Documentation · Publications · Contributors · Source · Cite