Determinacy: the listing an aggregate reads, and the query that is refused

An aggregate reads its group – or a window's frame – as a sequence, and the clause only partly fixes that sequence: rows the clause leaves tied may be listed either way. A query is admitted only where the listing cannot matter: each aggregate is symmetric, or any two rows its clause ties carry equal values of the term it aggregates. That condition is about the rows, so it is a judgment about the query and the instance, and a query that fails it is refused rather than given a value.

This module says all three things in Lean.

• The listing is invisible where the condition holds. ValueFrame.windowValue_eq_of_listing and Relation.groupSeqOrd_map_eq_of_listing: any listing of the frame or of the group in the clause's order reads as the evaluator's listing does. Both rest on List.map_eq_of_pairwise_of_symm – two sorted listings of one bag read alike, for a reading that cannot tell two mutually-comparable elements apart – and on OrderSpec.peer_of_readLe, which says that mutual comparability under the library's reading is peerhood of the clause.
• The condition itself, AggQueryIn.DeterminateOn q D γ: at each aggregation and each window of q, either the aggregate reads its input as a bag (SeqAggFunc.Symmetric) or the term is constant on the rows the clause ties (Relation.rowsAgree). It is quantified over the instance, in the manner of AggQueryIn.recSettles, and at an apply it follows the rows the left side offers.
• The evaluator that refuses, AggQueryIn.evaluateChecked: the plain answer where the condition holds, and none where it does not. AggQueryIn.windowValue_eq_of_listing_of_determinateOn and gammaAgg_eq_of_listing_of_determinateOn are what its some means at the two operators that read an order.

What this module does not do is change AggQueryIn.evaluatePlain, which keeps its own listing – the clause's order with ties broken by the row. That listing is one the condition admits, and every result of the metatheory relates two readings of one listing, so no theorem needs determinacy: the hom commutation, the random world, the rewriting and the adequacy hold on every instance, determinate or not. Determinacy is what a second listing asks for, which is why it is the hypothesis the re-typing of Provenance.AllRegular carries at a window: erasing a column's tag lets it into the tie-break, and ValueFrame.windowValueOpt_readTuple_of_det is where rowsAgree and OrderSpec.map_eq_of_keySorted are put to work.

theorem List.map_eq_of_pairwise_of_symm {α γ : Type} {R : α → α → Prop} {q : α → γ} {S : α → Prop} (hq : ∀ (x y : α), S x → S y → R x y → R y x → q x = q y) (L L' : List α) : (∀ x ∈ L, S x) → L.Perm L' → Pairwise R L → Pairwise R L' → map q L = map q L'

Two sorted listings of one bag read alike, for a reading that cannot tell two mutually-comparable elements of the bag apart.

theorem OrderSpec.peer_of_readLe {T : Type} [ValueType T] {p : ℕ} {α β : Type} [LinearOrder β] {key : β → Tuple T p} {val : α → β} {o : OrderSpec p} {x y : α} (h₁ : readLe key val o x y = true) (h₂ : readLe key val o y x = true) : o.peer (key (val x)) (key (val y)) = true

Mutual comparability is peerhood: the clause's reading breaks a tie by the row, so two occurrences each of which it puts first are peers of the clause.

theorem ValueFrame.windowValue_eq_of_listing {T : Type} [ValueType T] {n m p c : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) (t : TermIn T c n) (f : SeqAggFunc T) (R : Multiset (Tuple T n)) {u : Tuple T n} (hu : u ∈ R) (γ : Fin c → T) (hdet : ∀ (y z : Tuple T n), y ∈ R → z ∈ R → o.peer (O.key y) (O.key z) = true → t.eval y γ = t.eval z γ) (L : List (Tuple T n)) (hL : ↑L = frameOf id P O w R u) (hsorted : List.Pairwise (fun (y z : Tuple T n) => OrderSpec.readLe O.key id o y z = true) L) : f (List.map (fun (v : Tuple T n) => t.eval v γ) L) = windowValue P O o w t f R u γ

Any listing of a frame in the clause's order gives the window's value, where the aggregated term cannot tell two peers of the clause apart: the evaluator's listing is one of them, so the value it computes is the value every admissible listing computes.

def GroupOrder.peers {T : Type} [ValueType T] {k : ℕ} (ord : GroupOrder T k) (y z : Tuple T k) : Bool

Which rows a grouping's ORDER BY leaves tied: with no clause, all of them – an order-dependent aggregate then reads a sequence the clause does not fix at all, so its term has to be constant on the group.

Equations

• GroupOrder.unord.peers y z = true
• (GroupOrder.byCols cols spec).peers y z = spec.peer (cols.key y) (cols.key z)

def GroupOrder.SortedBy {T : Type} [ValueType T] {k : ℕ} (ord : GroupOrder T k) (L : List (Tuple T k)) : Prop

A listing of a group in the clause's order.

Equations

• GroupOrder.unord.SortedBy L = True
• (GroupOrder.byCols cols spec).SortedBy L = List.Pairwise (fun (y z : Tuple T k) => OrderSpec.readLe cols.key id spec y z = true) L

theorem Relation.groupSeqOrd_map_eq_of_listing {T : Type} [ValueType T] {k n₁ : ℕ} {γ' : Type} (is : Tuple (Fin k) n₁) (ord : GroupOrder T k) (r : Multiset (Tuple T k)) (g : Tuple T n₁) (read : Tuple T k → γ') (hdet : ∀ (y z : Tuple T k), y ∈ r → z ∈ r → ord.peers y z = true → read y = read z) (L : List (Tuple T k)) (hperm : L.Perm (groupSeq is r g)) (hsorted : ord.SortedBy L) : List.map read L = List.map read (groupSeqOrd is ord r g)

Any listing of a group in the clause's order reads as the evaluator's does, where the term cannot tell two rows the clause leaves tied apart.

noncomputable def AggQueryIn.readRows {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) (D : Database T) (γ : Fin c → T) : Multiset (Tuple T n)

What a window reads of its input: its rows with the aggregate columns nulled, which is the listing the clause orders.

Equations

• q.readRows D γ = Multiset.map (ColKind.readTuple κ) (q.evaluatePlain D γ)

def Relation.rowsAgree {T : Type} {k : ℕ} (r : Multiset (Tuple T k)) (tie : Tuple T k → Tuple T k → Bool) (read : Tuple T k → T) : Prop

A reading that cannot tell two tied rows of a relation apart.

Equations

• Relation.rowsAgree r tie read = ∀ (y z : Tuple T k), y ∈ r → z ∈ r → tie y z = true → read y = read z

def Relation.allRows {T : Type} {k : ℕ} (r : Multiset (Tuple T k)) (Q : Tuple T k → Prop) : Prop

Every row of a relation satisfies a property.

Equations

• Relation.allRows r Q = ∀ u ∈ r, Q u

def AggQueryIn.DeterminateOn {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} : AggQueryIn T c n κ l → Database T → (Fin c → T) → Prop

The query's aggregates cannot tell their listings apart, on this instance: at each aggregation and each window, either the aggregate reads its input as a bag, or the term it aggregates is constant on the rows the clause leaves tied. This is the condition under which a query is admitted – a condition on the rows, so a judgment about the query and the instance, which is why it is quantified here and not read off the syntax.

Equations

• One or more equations did not get rendered due to their size.
• (AggQueryIn.Rel x✝² a).DeterminateOn x✝¹ x✝ = True
• (AggQueryIn.Hole x✝³ s x✝²).DeterminateOn x✝¹ x✝ = True
• (AggQueryIn.Param pv x✝²).DeterminateOn x✝¹ x✝ = True
• AggQueryIn.Empty.DeterminateOn x✝¹ x✝ = True
• (AggQueryIn.Proj ps q).DeterminateOn x✝¹ x✝ = q.DeterminateOn x✝¹ x✝
• (AggQueryIn.Sel φ q hφ).DeterminateOn x✝¹ x✝ = q.DeterminateOn x✝¹ x✝
• (q₁.Prod q₂).DeterminateOn x✝¹ x✝ = (q₁.DeterminateOn x✝¹ x✝ ∧ q₂.DeterminateOn x✝¹ x✝)
• (q₁.Apply q₂).DeterminateOn x✝¹ x✝ = (q₁.DeterminateOn x✝¹ x✝ ∧ Relation.allRows (q₁.evaluatePlain x✝¹ x✝) fun (u : Tuple T n₁) => q₂.DeterminateOn x✝¹ (Fin.append u x✝))
• (q₁.Sum q₂).DeterminateOn x✝¹ x✝ = (q₁.DeterminateOn x✝¹ x✝ ∧ q₂.DeterminateOn x✝¹ x✝)
• q.Dedup.DeterminateOn x✝¹ x✝ = q.DeterminateOn x✝¹ x✝
• (q₁.Diff q₂).DeterminateOn x✝¹ x✝ = (q₁.DeterminateOn x✝¹ x✝ ∧ q₂.DeterminateOn x✝¹ x✝)
• (AggQueryIn.Explode k a q).DeterminateOn x✝¹ x✝ = q.DeterminateOn x✝¹ x✝
• (AggQueryIn.Retag h q).DeterminateOn x✝¹ x✝ = q.DeterminateOn x✝¹ x✝
• (AggQueryIn.Mu s q₀ q₁).DeterminateOn x✝¹ x✝ = (q₀.DeterminateOn x✝¹ x✝ ∧ q₁.DeterminateOn x✝¹ x✝)
• (AggQueryIn.MuSet s q₀ q₁).DeterminateOn x✝¹ x✝ = (q₀.DeterminateOn x✝¹ x✝ ∧ q₁.DeterminateOn x✝¹ x✝)
• (AggQueryIn.GammaNest is his p f q).DeterminateOn x✝¹ x✝ = q.DeterminateOn x✝¹ x✝
• (AggQueryIn.ProvSum is his t q).DeterminateOn x✝¹ x✝ = q.DeterminateOn x✝¹ x✝

noncomputable def AggQueryIn.evaluateChecked {T : Type} [ValueType T] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) (D : Database T) (γ : Fin c → T) : Option (Relation T n)

The evaluator that refuses: the plain answer where the query's aggregates cannot tell their listings apart on this instance, and nothing where one of them can.

Equations

• q.evaluateChecked D γ = if q.DeterminateOn D γ then some (q.evaluatePlain D γ) else none

theorem AggQueryIn.windowValue_eq_of_listing_of_determinateOn {T : Type} [ValueType T] {lab c n m p : ℕ} {rd : Fin c → Bool} {κ : Fin n → ColKind} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (t : TermIn T c n) (f : SeqAggFunc T) (q : AggQueryIn T c n κ) (hrr : WinReadsReg κ P O t) (dist : Bool) (keep : Option (Selection T n)) (D : Database T) (γ : Fin c → T) (hdet : (Win P O o w t f q hrr dist keep).DeterminateOn D γ) {u : Tuple T n} (hu : u ∈ q.readRows D γ) (L : List (Tuple T n)) (hL : ↑L = ValueFrame.frameOf id P O w (q.readRows D γ) u) (hsorted : List.Pairwise (fun (y z : Tuple T n) => OrderSpec.readLe O.key id o y z = true) L) : (if dist = true then f.distinct else f) (List.map (fun (v : Tuple T n) => t.eval v γ) L) = ValueFrame.windowValue P O o w t (if dist = true then f.distinct else f) (q.readRows D γ) u γ

What the refusal buys at a window: where the checked evaluator answers, the column it computes is the value every listing of the frame in the clause's order gives – so the listing the evaluator happens to take decides nothing.

Listings that agree only on the clause

A re-typing, or any other change of what breaks a tie, leaves a listing sorted by the clause's keys and reorders it inside a block of peers. That is weaker than OrderSpec.readLe-sortedness and it is all the invariance needs.

theorem OrderSpec.map_eq_of_keySorted {T : Type} [ValueType T] {p : ℕ} {α γ : Type} (key : α → Tuple T p) (o : OrderSpec p) (q : α → γ) {S : α → Prop} (hq : ∀ (x y : α), S x → S y → o.peer (key x) (key y) = true → q x = q y) (L L' : List α) (hS : ∀ x ∈ L, S x) (hperm : L.Perm L') (hL : List.Pairwise (fun (x y : α) => o.le (key x) (key y) = true) L) (hL' : List.Pairwise (fun (x y : α) => o.le (key x) (key y) = true) L') : List.map q L = List.map q L'

Two listings of one bag sorted by the clause's keys read alike, for a reading that is constant on the clause's peers. This is the invariance a change of tie-break asks for: the blocks of peers come in the order the clause fixes, and inside a block the reading does not look.

Home · Documentation · Publications · Contributors · Source · Cite