Derived operators

The operators of this file add nothing to the algebra: each is an abbreviation, a query built from the basis, and its semantics – plain and annotated – is the semantics of the query it abbreviates. What they buy is that the theorems proved of the basis apply to them as they stand, and that the translation of SQL has something to name.

Padding replaces columns by the null, which is what an outer join does to the arm with no match. Intersection is a self-join of the two deduplicated arms on all their columns, matching syntactically as SQL's INTERSECT does – and not ε(q₁ - (q₁ - q₂)), which has the same rows but annotates them by a difference of differences rather than by a conjunction of the two memberships.

The semijoin and the antijoin apply the left arm to a scalar aggregation of the filtered right one, so that each occurrence of the left arm keeps its multiplicity – a grouping on the left arm's columns would merge its duplicates, which WHERE EXISTS does not – and so that a row with no match still has its row, with count 𝟘. Comparing that count against 𝟘 is what tells the two apart. Over plain relations the decorrelation R - Π(σ_φ(R × Q)) gives the same rows, but not the same annotations, which is why the apply is needed here.

Truncation filters the rank and drops the rank column, so a row tied with the last one kept is kept too. Grouping sets are the union of one aggregation per set of the family, each padded back onto the columns of the whole key, which is what pad is for.

A FILTER clause is not an operator either: the aggregate reads its term through SQL's CASE, and the input policy – null-skipping or counting – drops what the clause nulls out.

A DISTINCT aggregate deduplicates the key columns together with the aggregated term and aggregates the added column. Over annotated relations that is what gives each distinct value one occurrence, annotated by the ⊕ of the occurrences it stands for; over plain ones it is the aggregate read over the distinct values (SeqAggFunc.distinct).

Padding

def AggQueryIn.padCol {T : Type} {n : ℕ} [ValueTypeNull T] (c : Option (Fin n)) : ProjCol T (ColKind.allReg n)

The projection column that reads column k, or the null when there is no column to read.

Equations

• AggQueryIn.padCol (some k) = ProjColIn.term (TermGIn.index k ⋯)
• AggQueryIn.padCol none = ProjColIn.term (TermGIn.const ValueTypeNull.null)

@[simp]

theorem AggQueryIn.padCol_kind {T : Type} {n : ℕ} [ValueTypeNull T] (c : Option (Fin n)) : ProjColIn.kind (padCol c) = ColKind.reg

def AggQueryIn.pad {T : Type} {n m : ℕ} [ValueTypeNull T] (π : Fin m → Option (Fin n)) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T m (ColKind.allReg m)

Padding: a projection that reads the columns π names and puts the null where π names none. It is what an outer join does to the arm with no match, and it adds no operator.

Equations

• AggQueryIn.pad π q = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (fun (j : Fin m) => AggQueryIn.padCol (π j)) q)

def AggQueryIn.padRight {T : Type} {n : ℕ} [ValueTypeNull T] (l : ℕ) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + l) (ColKind.allReg (n + l))

The padding that keeps every column of q and appends l null columns, as a left outer join does to an unmatched row.

Equations

• AggQueryIn.padRight l q = AggQueryIn.pad (fun (i : Fin (n + l)) => Fin.addCases (fun (i : Fin n) => some i) (fun (x : Fin l) => none) i) q

def AggQueryIn.padLeft {T : Type} {n : ℕ} [ValueTypeNull T] (l : ℕ) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (l + n) (ColKind.allReg (l + n))

The padding that prepends l null columns, as a right outer join does.

Equations

• AggQueryIn.padLeft l q = AggQueryIn.pad (fun (i : Fin (l + n)) => Fin.addCases (fun (x : Fin l) => none) (fun (i : Fin n) => some i) i) q

Intersection

def AggQueryIn.interCond {T : Type} [ValueType T] (k : ℕ) : GenPred T (ColKind.allReg (k + k))

The conjunction ⋀_{i<k} #i ≐ #(k+i): the two blocks of a doubled schema agree, column by column, syntactically – two nulls being the same value, as every key comparison in SQL's set operators is.

Equations

• AggQueryIn.interCond k = keyJoinCond (fun (i : Fin k) => Fin.castAdd k i) (fun (i : Fin k) => Fin.natAdd k i) ⋯ ⋯

def AggQueryIn.firstCols {T : Type} (a b : ℕ) : Tuple (ProjCol T (ColKind.allReg (a + b))) a

The projection onto the first a columns of a schema of a + b.

Equations

• AggQueryIn.firstCols a b i = ProjColIn.term (TermGIn.index (Fin.castAdd b i) ⋯)

def AggQueryIn.lastCols {T : Type} (a b : ℕ) : Tuple (ProjCol T (ColKind.allReg (a + b))) b

The projection onto the last b columns of a schema of a + b.

Equations

• AggQueryIn.lastCols a b j = ProjColIn.term (TermGIn.index (Fin.natAdd a j) ⋯)

def AggQueryIn.fstBlock {T : Type} (k : ℕ) : Tuple (ProjCol T (ColKind.allReg (k + k))) k

The projection onto the first block of a doubled schema.

Equations

• AggQueryIn.fstBlock k = AggQueryIn.firstCols k k

@[simp]

theorem AggQueryIn.firstCols_kind {T : Type} (a b : ℕ) (i : Fin a) : ProjColIn.kind (firstCols a b i) = ColKind.reg

@[simp]

theorem AggQueryIn.lastCols_kind {T : Type} (a b : ℕ) (j : Fin b) : ProjColIn.kind (lastCols a b j) = ColKind.reg

@[simp]

theorem AggQueryIn.fstBlock_kind {T : Type} (k : ℕ) (i : Fin k) : ProjColIn.kind (fstBlock k i) = ColKind.reg

theorem AggQueryIn.append_allReg (a b : ℕ) : Fin.append (ColKind.allReg a) (ColKind.allReg b) = ColKind.allReg (a + b)

Doubling an all-regular schema leaves it all-regular.

def AggQueryIn.inter {T : Type} {n : ℕ} [ValueType T] (q₁ q₂ : AggQuery T n (ColKind.allReg n)) : AggQuery T n (ColKind.allReg n)

Intersection, SQL's INTERSECT: one copy of each tuple the two arms share, matched syntactically. Its annotation is the product of the two ⊕-sums, one per arm – the provenance of a conjunction of the two memberships, which is what ε(q₁ - (q₁ - q₂)) would not give.

Equations

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

Outer joins

def AggQueryIn.innerJoin {T : Type} {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) : AggQuery T (n₁ + n₂) (ColKind.allReg (n₁ + n₂))

The inner join of the two arms: the rows that match.

Equations

• AggQueryIn.innerJoin φ q₁ q₂ = AggQueryIn.Sel φ (AggQueryIn.castKind ⋯ (AggQueryIn.Prod q₁ q₂)) ⋯

def AggQueryIn.leftUnmatched {T : Type} [ValueTypeNull T] {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) : AggQuery T (n₁ + n₂) (ColKind.allReg (n₁ + n₂))

The rows of the left arm with no match, padded on the right with nulls.

Equations

• AggQueryIn.leftUnmatched φ q₁ q₂ = AggQueryIn.padRight n₂ (AggQueryIn.Diff q₁ (AggQueryIn.castKind ⋯ (AggQueryIn.Proj (AggQueryIn.firstCols n₁ n₂) (AggQueryIn.innerJoin φ q₁ q₂))))

def AggQueryIn.rightUnmatched {T : Type} [ValueTypeNull T] {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) : AggQuery T (n₁ + n₂) (ColKind.allReg (n₁ + n₂))

The rows of the right arm with no match, padded on the left with nulls.

Equations

• AggQueryIn.rightUnmatched φ q₁ q₂ = AggQueryIn.padLeft n₁ (AggQueryIn.Diff q₂ (AggQueryIn.castKind ⋯ (AggQueryIn.Proj (AggQueryIn.lastCols n₁ n₂) (AggQueryIn.innerJoin φ q₁ q₂))))

def AggQueryIn.leftOuter {T : Type} [ValueTypeNull T] {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) : AggQuery T (n₁ + n₂) (ColKind.allReg (n₁ + n₂))

Left outer join: the matching rows, and the rows of the left arm with no match padded with nulls.

Equations

• AggQueryIn.leftOuter φ q₁ q₂ = AggQueryIn.Sum (AggQueryIn.innerJoin φ q₁ q₂) (AggQueryIn.leftUnmatched φ q₁ q₂)

def AggQueryIn.rightOuter {T : Type} [ValueTypeNull T] {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) : AggQuery T (n₁ + n₂) (ColKind.allReg (n₁ + n₂))

Right outer join.

Equations

• AggQueryIn.rightOuter φ q₁ q₂ = AggQueryIn.Sum (AggQueryIn.innerJoin φ q₁ q₂) (AggQueryIn.rightUnmatched φ q₁ q₂)

def AggQueryIn.fullOuter {T : Type} [ValueTypeNull T] {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) : AggQuery T (n₁ + n₂) (ColKind.allReg (n₁ + n₂))

Full outer join: both arms padded.

Equations

• AggQueryIn.fullOuter φ q₁ q₂ = AggQueryIn.Sum (AggQueryIn.leftOuter φ q₁ q₂) (AggQueryIn.rightUnmatched φ q₁ q₂)

What the outer joins compute

noncomputable def AggQueryIn.matchedLeft {T : Type} [ValueTypeNull T] {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) (d : Database T) : Multiset (Tuple T n₁)

The rows of the left arm that have a match: the first block of the inner join.

Equations

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

noncomputable def AggQueryIn.matchedRight {T : Type} [ValueTypeNull T] {n₁ n₂ : ℕ} (φ : GenPred T (ColKind.allReg (n₁ + n₂))) (q₁ : AggQuery T n₁ (ColKind.allReg n₁)) (q₂ : AggQuery T n₂ (ColKind.allReg n₂)) (d : Database T) : Multiset (Tuple T n₂)

The rows of the right arm that have a match: the second block of the inner join.

Equations

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

Semijoin and antijoin

R ⋉_φ Q keeps the occurrences of R that φ matches with some row of Q, and R ▷_φ Q those it matches with none. Both are read off one query: the apply of R to the scalar aggregation that counts the matches, followed by a comparison of that count against 𝟘 and a projection back onto R's columns. The counted column kap is one that is never null in a row of Q – a key column, or a constant 1 added to Q – so that the count is 𝟘 exactly where nothing matches.

@[reducible, inline]

abbrev AggQueryIn.countKinds (k : ℕ) : Fin (k + 1) → ColKind

The kind vector of a match-count row: the left arm's columns followed by the count.

Equations

• AggQueryIn.countKinds k = Fin.append (ColKind.allReg k) fun (x : Fin 1) => ColKind.agg

@[reducible, inline]

abbrev AggQueryIn.countCol (k : ℕ) : Fin (k + 1)

The column a match count appends.

Equations

• AggQueryIn.countCol k = Fin.natAdd k 0

theorem AggQueryIn.countKinds_countCol (k : ℕ) : countKinds k (countCol k) = ColKind.agg

def AggQueryIn.matchCount {T : Type} {k l : ℕ} (cnt : SeqAggFunc T) (kap : Fin l) (φ : GenPredIn T k (ColKind.allReg l)) (R : AggQuery T k (ColKind.allReg k)) (Q : AggQueryIn T k l (ColKind.allReg l)) : AggQuery T (k + 1) (countKinds k)

The match count: one row per occurrence of R, carrying that occurrence and the token that counts, with cnt over the column kap, the rows of Q the condition φ matches it with. The aggregation is the scalar one, which has its row even where nothing matches.

Equations

• AggQueryIn.matchCount cnt kap φ R Q = AggQueryIn.Apply R (AggQueryIn.GammaScalar ![#kap] ![cnt] (AggQueryIn.Sel φ Q ⋯))

def AggQueryIn.dropCount {T : Type} (k : ℕ) : Tuple (ProjCol T (countKinds k)) k

The projection that keeps the left arm's columns and drops the count.

Equations

• AggQueryIn.dropCount k i = ProjColIn.term (TermGIn.index (Fin.castAdd 1 i) ⋯)

def AggQueryIn.semijoin {T : Type} [ValueType T] {k l : ℕ} (cnt : SeqAggFunc T) (kap : Fin l) (φ : GenPredIn T k (ColKind.allReg l)) (R : AggQuery T k (ColKind.allReg k)) (Q : AggQueryIn T k l (ColKind.allReg l)) : AggQuery T k (ColKind.allReg k)

Semijoin: the occurrences of R that φ matches with at least one row of Q.

Equations

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

def AggQueryIn.antijoin {T : Type} [ValueType T] {k l : ℕ} (cnt : SeqAggFunc T) (kap : Fin l) (φ : GenPredIn T k (ColKind.allReg l)) (R : AggQuery T k (ColKind.allReg k)) (Q : AggQueryIn T k l (ColKind.allReg l)) : AggQuery T k (ColKind.allReg k)

Antijoin: the occurrences of R that φ matches with no row of Q.

Equations

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

Offset functions

first_value and last_value read one end of a frame; lag and lead read the frames of the rows strictly before and strictly after. All four are the window operator with PICKFIRST, the aggregate that takes the first value of the sequence it is given, so what tells them apart is the frame and the order the frame is read in – the two jobs the clause does, which the window operator keeps separate because the frame is an argument of its own. A value at an offset other than one needs an aggregate that reads a position other than the end, SeqAggFunc.pickNth, and nthValue, lagAt and leadAt are the same three queries over it.

def AggQueryIn.firstValue {T : Type} [ValueType T] {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (t : Term T n) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

first_value(t) over the frame w: the value of t on the first row of the frame in the clause's order.

Equations

• AggQueryIn.firstValue P O o w t q = AggQueryIn.Win P O o w t SeqAggFunc.pickFirst q ⋯

def AggQueryIn.lastValue {T : Type} [ValueType T] {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (t : Term T n) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

last_value(t): the same frame, read backwards. Only the reading order is reversed – the frame is an argument, so a frame the clause bounds is still bounded by the clause as it stands.

Equations

• AggQueryIn.lastValue P O o w t q = AggQueryIn.Win P O o.reverse w t SeqAggFunc.pickFirst q ⋯

def AggQueryIn.lag {T : Type} [ValueType T] {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (t : Term T n) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

lag(t): last_value over the rows strictly before the current row's peers.

Equations

• AggQueryIn.lag P O o t q = AggQueryIn.lastValue P O o (ValueFrame.rangeBefore o) t q

def AggQueryIn.lead {T : Type} [ValueType T] {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (t : Term T n) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

lead(t): first_value over the rows strictly after.

Equations

• AggQueryIn.lead P O o t q = AggQueryIn.firstValue P O o (ValueFrame.rangeAfter o) t q

def AggQueryIn.nthValue {T : Type} [ValueType T] {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (i : ℕ) (t : Term T n) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

nth_value(t, i+1) over the frame w: the value of t on the row at offset i of the frame in the clause's order, counting from 0. firstValue is the case i = 0.

Equations

• AggQueryIn.nthValue P O o w i t q = AggQueryIn.Win P O o w t (SeqAggFunc.pickNth i) q ⋯

def AggQueryIn.lagAt {T : Type} [ValueType T] {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (i : ℕ) (t : Term T n) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

lag(t, i+1): the value i + 1 rows before the current row's peers, the frame of lag read backwards from its end.

Equations

• AggQueryIn.lagAt P O o i t q = AggQueryIn.nthValue P O o.reverse (ValueFrame.rangeBefore o) i t q

def AggQueryIn.leadAt {T : Type} [ValueType T] {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (i : ℕ) (t : Term T n) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

lead(t, i+1): the value i + 1 rows after.

Equations

• AggQueryIn.leadAt P O o i t q = AggQueryIn.nthValue P O o (ValueFrame.rangeAfter o) i t q

Ranks

SQL's ranks are counts over the rows the clause sorts strictly before the current row's peers, plus one. The + 1 is a term over an aggregate column, so the rank column is an aggregate column too – the unary aggregate expression of Provenance.AggExpr, which ProjColIn.aggTerm names and AggValue.postcomp represents.

def AggQueryIn.carryCol {T : Type} {n : ℕ} (κ : Fin n → ColKind) (k : Fin n) : ProjCol T κ

The projection column that carries an input column through: a regular column as a term, an aggregate column as its token, a provenance column as its provenance term – so the output column has the kind the input column has. A projection over a window keeps every column of its input this way, aggregate columns included, which is what a second window of one SELECT needs.

Equations

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

def AggQueryIn.overWindow {T : Type} {n : ℕ} (κ : Fin n → ColKind) (gf : TermIn T 1 0) : Tuple (ProjCol T (Fin.snoc κ ColKind.agg)) (n + 1)

The projection that keeps a window's input columns and reads its added column through a term.

Equations

• AggQueryIn.overWindow κ gf = Fin.snoc (fun (i : Fin n) => AggQueryIn.carryCol (Fin.snoc κ ColKind.agg) i.castSucc) (ProjColIn.aggTermOf (Fin.last n) ⋯ gf)

@[simp]

theorem AggQueryIn.overWindow_kind {T : Type} {n : ℕ} (κ : Fin n → ColKind) (gf : TermIn T 1 0) (j : Fin (n + 1)) : ProjColIn.kind (overWindow κ gf j) = Fin.snoc κ ColKind.agg j

def AggQueryIn.rank {T : Type} {n m p : ℕ} [One T] (cnt : SeqAggFunc T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) {κ : Fin n → ColKind} (q : AggQuery T n κ) (hrr : WinReadsReg κ P O (TermIn.const 1)) : AggQuery T (n + 1) (Fin.snoc κ ColKind.agg)

rank(): one plus the count of the rows the clause sorts strictly before the current row's peers. cnt is the counting aggregate, read over the constant term – SQL's COUNT(*).

Equations

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

def AggQueryIn.denseRank {T : Type} {n m : ℕ} [One T] (cnt : SeqAggFunc T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) 1) (o : OrderSpec 1) {κ : Fin n → ColKind} (q : AggQuery T n κ) (hrr : WinReadsReg κ P O #(O 0)) : AggQuery T (n + 1) (Fin.snoc κ ColKind.agg)

dense_rank(): one plus the count of the distinct order values the clause sorts strictly before the current row's peers. A dense rank counts O read as a single row value, so that every class of peers counts once; here the order is a single column and that value is the column's, which is what Win's distinct reading merges by (AggValue.mergeByValue). A multi-column order needs a term whose value is the whole key, which the value domain does not have – TermIn builds no tuple – so this is the one-column case and not the general one.

Equations

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

The distribution functions

percent_rank, cume_dist and ntile are aggregate expressions over two frames of one partition, not aggregates: each reads the whole partition for its denominator and one other frame for its numerator, and the two families are nested. WinExpr is what reads them as one family, so the pair of values a world gives is a pair that some world of the partition actually produces – where reading the two aggregates separately would allow a rank of three beside a count of one.

The arithmetic is a parameter, as the counting aggregate is for rank: a ValueType has +, -, * and an order, and SQL's division and integer bucket arithmetic are not among them. Only the value of the combining function in each world is used, so any deterministic function of the domain can be one.

def AggQueryIn.percentRank {T : Type} [ValueType T] {n m p : ℕ} [One T] (cnt : SeqAggFunc T) (divide : T → T → T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

percent_rank(): (r-1)/(N-1), and 0 where N = 1, with r the rank and N the count over the whole partition. The numerator is read off the frame of the rows strictly before the current row's peers, which is r - 1 without needing a subtraction.

Equations

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

def AggQueryIn.cumeDist {T : Type} {n m p : ℕ} [One T] (cnt : SeqAggFunc T) (divide : T → T → T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

cume_dist(): c/N, with c the count over the default RANGE frame – the rows up to the current one and its peers – and N the count over the whole partition.

Equations

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

def AggQueryIn.ntile {T : Type} [ValueType T] {n m p : ℕ} [One T] (cnt : SeqAggFunc T) (bucket : T → T → T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (q : AggQuery T n (ColKind.allReg n)) : AggQuery T (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

ntile(k): the bucket SQL gives to the position the rank names, among N rows. bucket N r is SQL's integer arithmetic, left to the domain; the reading is the one of the ties-as-ranks principle, so a class of peers stays together where SQL's row numbering would split it between two buckets.

Equations

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

Truncation

λ^{P,O}_{m,c} keeps the occurrences with at least m and fewer than m + c rows ranked strictly before them in their partition: it filters the rank and drops the rank column again. Rows tied with the last one kept are kept too, the rank counting the rows strictly before a row's peers – SQL's FETCH FIRST c ROWS WITH TIES. An infinite count is truncateFrom, the same query with the upper bound dropped.

def AggQueryIn.dropRank {T : Type} {n : ℕ} (κ : Fin n → ColKind) : Tuple (ProjCol T (Fin.snoc κ ColKind.agg)) n

The projection that drops the rank column a truncation filters on, carrying every other column of the input through – an aggregate column of the input, such as an earlier window's, included (carryCol).

Equations

• AggQueryIn.dropRank κ i = AggQueryIn.carryCol (Fin.snoc κ ColKind.agg) i.castSucc

@[simp]

theorem AggQueryIn.dropRank_kind {T : Type} {n : ℕ} (κ : Fin n → ColKind) (i : Fin n) : ProjColIn.kind (dropRank κ i) = κ i

def AggQueryIn.rankRange {T : Type} {n : ℕ} (κ : Fin n → ColKind) (lo hi : T) : GenPred T (Fin.snoc κ ColKind.agg)

The range of ranks a truncation keeps: more than lo rows ranked strictly before the row's peers, and at most hi.

Equations

• AggQueryIn.rankRange κ lo hi = GenPredIn.aggRange (Fin.last n) ⋯ CompOp.gt (TermGIn.const lo) CompOp.le (TermGIn.const hi)

def AggQueryIn.truncate {T : Type} {n m p : ℕ} [One T] (cnt : SeqAggFunc T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (lo hi : T) {κ : Fin n → ColKind} (q : AggQuery T n κ) (hrr : WinReadsReg κ P O (TermIn.const 1)) : AggQuery T n κ

Truncation λ^{P,O}_{m,c}.

Equations

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

def AggQueryIn.rankFrom {T : Type} {n : ℕ} (κ : Fin n → ColKind) (lo : T) : GenPred T (Fin.snoc κ ColKind.agg)

The lower half of the range: at least lo rows ranked strictly before the row's peers. It is what an infinite count asks for – SQL's OFFSET with no LIMIT.

Equations

• AggQueryIn.rankFrom κ lo = GenPredIn.aggCmp (Fin.last n) ⋯ CompOp.gt (TermGIn.const lo)

def AggQueryIn.distinctOn {T : Type} [ValueType T] {n m p : ℕ} [One T] (cnt : SeqAggFunc T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) {κ : Fin n → ColKind} (q : AggQuery T n κ) (hrr : WinReadsReg κ P O (TermIn.const 1)) : AggQuery T n κ

SELECT DISTINCT ON (P) … ORDER BY P, O: one row per partition, the first in the clause's order, which is the truncation λ^{P,O}_{0,1} – and, with peers, the rows tied with it.

Equations

• AggQueryIn.distinctOn cnt P O o q hrr = AggQueryIn.truncate cnt P O o 0 1 q hrr

def AggQueryIn.truncateFrom {T : Type} {n m p : ℕ} [One T] (cnt : SeqAggFunc T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (lo : T) {κ : Fin n → ColKind} (q : AggQuery T n κ) (hrr : WinReadsReg κ P O (TermIn.const 1)) : AggQuery T n κ

Truncation with an infinite count, λ^{P,O}_{m,∞}.

Equations

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

Grouping sets

γ_𝒮[t₁:f₁,…,tₙ:fₙ](q) is the union, over the sets of the family, of the aggregation on the indices that set keeps, padded back onto the columns of the whole key: a key column a set drops is the null there. Each arm therefore has the same columns – the whole key, then the aggregates – and the union is a union of the algebra. It is what SQL's GROUPING SETS, ROLLUP and CUBE name.

@[reducible, inline]

abbrev AggQueryIn.gsPos {m : ℕ} (S : Finset (Fin m)) (a : Fin m) (ha : a ∈ S) : Fin S.card

The position of a grouping index inside a grouping set.

Equations

• AggQueryIn.gsPos S a ha = (S.orderIsoOfFin ⋯).symm ⟨a, ha⟩

def AggQueryIn.gsCol {T : Type} [ValueTypeNull T] {c m : ℕ} (S : Finset (Fin m)) (na : ℕ) (j : Fin (m + na)) : ProjColIn T c (Fin.append (fun (x : Fin S.card) => ColKind.reg) fun (x : Fin na) => ColKind.agg)

The projection that pads a grouping set's result back onto the columns of the whole key: a key column the set drops becomes the null, one it keeps is read where the aggregation put it, and the aggregate columns follow.

Equations

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

theorem AggQueryIn.gsCol_kind {T : Type} [ValueTypeNull T] {c m : ℕ} (S : Finset (Fin m)) (na : ℕ) (j : Fin (m + na)) : (gsCol S na j).kind = Fin.append (fun (x : Fin m) => ColKind.reg) (fun (x : Fin na) => ColKind.agg) j

def AggQueryIn.gammaSet {T : Type} [ValueTypeNull T] {c k m na : ℕ} (is : Tuple (Fin k) m) (ts : Tuple (TermIn T c k) na) (fs : Tuple (SeqAggFunc T) na) (S : Finset (Fin m)) (q : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c (m + na) (Fin.append (fun (x : Fin m) => ColKind.reg) fun (x : Fin na) => ColKind.agg)

One grouping set: the aggregation on the indices the set keeps, padded back onto the columns of the whole key.

Equations

• AggQueryIn.gammaSet is ts fs S q = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (AggQueryIn.gsCol S na) (AggQueryIn.Gamma (fun (a : Fin S.card) => is ↑((S.orderIsoOfFin ⋯) a)) ts fs q))

def AggQueryIn.gammaSets {T : Type} [ValueTypeNull T] {c k m na : ℕ} (is : Tuple (Fin k) m) (ts : Tuple (TermIn T c k) na) (fs : Tuple (SeqAggFunc T) na) (S₀ : Finset (Fin m)) (𝒮 : List (Finset (Fin m))) (q : AggQueryIn T c k (ColKind.allReg k)) : AggQueryIn T c (m + na) (Fin.append (fun (x : Fin m) => ColKind.reg) fun (x : Fin na) => ColKind.agg)

Grouping sets: the union of the aggregations over each set of the family, all padded onto the same columns.

Equations

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

def AggQueryIn.gsRow {T : Type} [ValueTypeNull T] {m : ℕ} (S : Finset (Fin m)) (na : ℕ) (v : Tuple T (S.card + na)) : Tuple T (m + na)

The row a grouping set's padding builds: the null where the set drops a key column, the aggregation's column where it keeps it, then the aggregates.

Equations

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

DISTINCT aggregates

γ_i[t:f^distinct](q) is the aggregate of the distinct values of t in each group. It is an abbreviation: deduplicate the key columns together with t, then aggregate the added column. Over annotated relations that is what gives each distinct value one occurrence, annotated by the ⊕ of the occurrences it stands for, and the group, its key and its existence factor are those of the deduplicated projection, which are those of the input.

The DISTINCT of a window aggregate is not this: the frame's occurrences would have to be merged by value in place, which the window operator does not do. Only the grouped and the scalar forms are here.

def AggQueryIn.distinctCols {T : Type} {m c n₁ : ℕ} (is : Tuple (Fin m) n₁) (t : TermIn T c m) : Tuple (ProjColIn T c (ColKind.allReg m)) (n₁ + 1)

The projection Π_{#i₁,…,#i_{n₁},t} that a DISTINCT aggregate deduplicates.

Equations

• AggQueryIn.distinctCols is t j = ProjColIn.term (Fin.snoc (fun (k : Fin n₁) => (#(is k)).toGen) t.toGen j)

@[simp]

theorem AggQueryIn.distinctCols_kind {T : Type} {m c n₁ : ℕ} (is : Tuple (Fin m) n₁) (t : TermIn T c m) (j : Fin (n₁ + 1)) : (distinctCols is t j).kind = ColKind.reg

def AggQueryIn.distinctRow {T : Type} {m : ℕ} [ValueType T] {c n₁ : ℕ} (is : Tuple (Fin m) n₁) (t : TermIn T c m) (γ : Fin c → T := fun (x : Fin c) => 0) (u : Tuple T m) : Tuple T (n₁ + 1)

The row that projection builds: the key columns followed by the value of the aggregated term.

Equations

• AggQueryIn.distinctRow is t γ u = Fin.snoc (fun (k : Fin n₁) => u (is k)) (t.eval u γ)

def AggQueryIn.gammaDistinct {T : Type} {m c n₁ : ℕ} (is : Tuple (Fin m) n₁) (t : TermIn T c m) (f : SeqAggFunc T) (q : AggQueryIn T c m (ColKind.allReg m)) : AggQueryIn T c (n₁ + 1) (Fin.append (fun (x : Fin n₁) => ColKind.reg) fun (x : Fin 1) => ColKind.agg)

A DISTINCT aggregate, γ_i[t:f^distinct](q): deduplicate the key columns together with the aggregated term, then aggregate the added column over each group.

Equations

• AggQueryIn.gammaDistinct is t f q = AggQueryIn.Gamma (fun (k : Fin n₁) => k.castSucc) ![#(Fin.last n₁)] ![f] (AggQueryIn.castKind ⋯ (AggQueryIn.Proj (AggQueryIn.distinctCols is t) q)).Dedup

def AggQueryIn.gammaScalarDistinct {T : Type} {m c : ℕ} (t : TermIn T c m) (f : SeqAggFunc T) (q : AggQueryIn T c m (ColKind.allReg m)) : AggQueryIn T c 1 fun (x : Fin 1) => ColKind.agg

A DISTINCT aggregate without grouping: the same abbreviation with no key column, so that the deduplication is that of the values of the term alone.

Equations

• AggQueryIn.gammaScalarDistinct t f q = AggQueryIn.GammaScalar ![#(Fin.last 0)] ![f] (AggQueryIn.castKind ⋯ (AggQueryIn.Proj (AggQueryIn.distinctCols (fun (k : Fin 0) => k.elim0) t) q)).Dedup

The FILTER clause

f(t) FILTER (WHERE φ) restricts what the aggregate reads. Over a null-skipping aggregate it is f over CASE WHEN φ THEN t END, and over a count it is the same term read through the counting policy: both policies drop the nulls, so nulling out the occurrences the clause rejects is exactly leaving them out of the sequence. The group, its key and its annotation are those of all the occurrences – a filtered-out occurrence still witnesses its group – which is why the clause belongs in the term and not in a selection under the aggregation.

A guard that is a Boolean combination of comparisons needs nothing more: a conjunction is a nested CASE, a disjunction a COALESCE of the two cases, and a negation CompOp.negate.

The third input policy is not here. A null-keeping aggregate reads every value, the null included, so it cannot tell an occurrence the clause rejects from one whose term is null; SQL removes the rejected ones from the sequence, which no term can do and which the aggregation operators would have to be told about.

def AggQueryIn.filterTerm {T : Type} [ValueTypeNull T] {c n : ℕ} (op : CompOp) (t₁ t₂ t : TermIn T c n) : TermIn T c n

The term a FILTER clause makes an aggregate read: the aggregated term where the clause holds, the null where it does not.

Equations

• AggQueryIn.filterTerm op t₁ t₂ t = TermIn.caseWhen op t₁ t₂ t (TermIn.const ValueTypeNull.null)

def AggQueryIn.filterHolds {T : Type} [ValueTypeNull T] {c n : ℕ} (op : CompOp) (t₁ t₂ : TermIn T c n) (γ : Fin c → T := fun (x : Fin c) => 0) (u : Tuple T n) : Bool

Whether a FILTER clause holds on a row.

Equations

• AggQueryIn.filterHolds op t₁ t₂ γ u = decide (op.eval3 (t₁.eval u γ) (t₂.eval u γ) = Kleene.true)

def AggQueryIn.gammaFilter {T : Type} [ValueTypeNull T] {c m n₁ : ℕ} (is : Tuple (Fin m) n₁) (op : CompOp) (t₁ t₂ t : TermIn T c m) (f : SeqAggFunc T) (q : AggQueryIn T c m (ColKind.allReg m)) : AggQueryIn T c (n₁ + 1) (Fin.append (fun (x : Fin n₁) => ColKind.reg) fun (x : Fin 1) => ColKind.agg)

An aggregation with a FILTER clause: the aggregate reads the term through the clause. The aggregate comes already read through its input policy – SeqAggFunc.sqlOf for a null-skipping aggregate, SeqAggFunc.counting for a count – and it is that policy which drops the occurrences the clause nulls out.

Equations

• AggQueryIn.gammaFilter is op t₁ t₂ t f q = AggQueryIn.Gamma is ![AggQueryIn.filterTerm op t₁ t₂ t] ![f] q

def AggQueryIn.winFilter {T : Type} [ValueTypeNull T] {c n mp p : ℕ} (P : Tuple (Fin n) mp) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (op : CompOp) (t₁ t₂ t : TermIn T c n) (f : SeqAggFunc T) (q : AggQueryIn T c n (ColKind.allReg n)) : AggQueryIn T c (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

A window aggregate with a FILTER clause.

Equations

• AggQueryIn.winFilter P O o w op t₁ t₂ t f q = AggQueryIn.Win P O o w (AggQueryIn.filterTerm op t₁ t₂ t) f q ⋯

The FILTER clause, for any input policy

AggQueryIn.Gamma carries a clause per aggregate, and the clause cuts the occurrence sequence rather than nulling a value out. That serves all three of SQL's input policies, the null-keeping one included, and it asks nothing of the value domain – there is no null in sight here, where gammaFilter needed one.

def AggQueryIn.gammaWhere {T : Type} {c m n₁ : ℕ} (is : Tuple (Fin m) n₁) (φ : Selection T m) (t : TermIn T c m) (f : SeqAggFunc T) (q : AggQueryIn T c m (ColKind.allReg m)) : AggQueryIn T c (n₁ + 1) (Fin.append (fun (x : Fin n₁) => ColKind.reg) fun (x : Fin 1) => ColKind.agg)

An aggregation with a FILTER clause. One group key, one aggregate, and the clause the aggregate reads its group through.

Equations

• AggQueryIn.gammaWhere is φ t f q = AggQueryIn.Gamma is ![t] ![f] q fun (x : Fin 1) => some φ

def AggQueryIn.winWhere {T : Type} {c n mp p : ℕ} (P : Tuple (Fin n) mp) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (φ : Selection T n) (t : TermIn T c n) (f : SeqAggFunc T) (q : AggQueryIn T c n (ColKind.allReg n)) (dist : Bool := false) : AggQueryIn T c (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

A window aggregate with a FILTER clause, for any input policy: PostgreSQL's agg(x) FILTER (WHERE φ) OVER (…). The clause cuts the frame down to the rows it keeps, so a null-keeping aggregate is served here too, and the token is read in the scalar convention – the kept part of a frame may be empty where the frame is not.

Equations

• AggQueryIn.winWhere P O o w φ t f q dist = AggQueryIn.Win P O o w t f q ⋯ dist (some φ)

Constant relations

AggQueryIn.Empty is the one leaf that belongs to the query rather than to the instance, and everything a query builds from nowhere is derived from it here: the unit relation is its scalar aggregation with no aggregate, and a constant relation is a union of projections of the unit onto constants. A constant relation therefore needs no leaf of its own, and the non-emptiness SQL asks of VALUES is a condition of this notation and not of the syntax.

def AggQueryIn.unit {T : Type} : AggQuery T 0 (ColKind.allReg 0)

The unit relation 𝟏: one empty tuple, annotated 𝟙. It is the scalar aggregation of the empty relation with no aggregate – PostgreSQL's SELECT; – and the row it emits exists on its own: no group, so no group-existence factor.

Equations

• AggQueryIn.unit = AggQueryIn.castKind AggQueryIn.unit._proof_1 (AggQueryIn.GammaScalar (fun (j : Fin 0) => j.elim0) (fun (j : Fin 0) => j.elim0) AggQueryIn.Empty)

def AggQueryIn.rowOf {T : Type} {k : ℕ} (u : Tuple T k) : AggQuery T k (ColKind.allReg k)

One row of constants: the unit projected onto the values of u.

Equations

• AggQueryIn.rowOf u = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (fun (j : Fin k) => ProjColIn.term (TermGIn.const (u j))) AggQueryIn.unit)

def AggQueryIn.values {T : Type} {k : ℕ} (us : List (Tuple T k)) (h : us ≠ []) : AggQuery T k (ColKind.allReg k)

VALUES: the constant relation holding the tuples of us, with duplicates kept, as the union of one row per entry. SQL's VALUES asks for at least one row, which is the hypothesis here; SELECT without FROM is the case of one tuple.

Equations

• AggQueryIn.values [] h_2 = absurd ⋯ h_2
• AggQueryIn.values (u :: rest) x = List.foldl (fun (q : AggQuery T k (ColKind.allReg k)) (v : Tuple T k) => AggQueryIn.Sum q (AggQueryIn.rowOf v)) (AggQueryIn.rowOf u) rest

Home · Documentation · Publications · Contributors · Source · Cite