Window frames determined by values

A window function computes, for each row, an aggregate over a frame: some of the rows sharing its partition. Which rows, in general, depends on positions in a sorted partition – the previous row, the previous three – and a position is not something a row carries. In a world where some rows are absent the previous row is the previous present row, so a frame read positionally is not the restriction of the frame read on the whole relation, and the value a row gets cannot be computed world by world.

A frame is determined by values when membership depends only on the order values of the two rows and on whether they are the same occurrence: a relation ρ between order values decides the other rows, and a predicate s on its own order value decides whether the row is in its own frame. SQL's RANGE and GROUPS frames without offsets, the frames with EXCLUDE, and the frame of the rows strictly before the current one are all of this form; ROWS frames other than the whole partition are not.

For such a frame the restriction property holds (frame_inter): the frame of an occurrence among the present rows is its frame in the whole relation, intersected with them. That is what lets a window be read in every world, and it is the only property of frames the annotated semantics uses.

def Tuple.key {T : Type} {n p : ℕ} (is : Tuple (Fin n) p) (u : Tuple T n) : Tuple T p

The values a tuple has at a list of columns: its partition key, or its order value.

Equations

• is.key u k = u (is k)

def OccFam.ofSorted {α : Type} [LinearOrder α] (s : Multiset α) : OccFam α

The canonical indexing of a relation: its rows in sorted order. It is computable, where a choice through Multiset.toList is not, and canonical rather than arbitrary – though by OccFam.Congr_of_toMultiset_eq any indexing would give the same answer for an operator that respects re-indexing.

Equations

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

A frame is a condition on the order values

SQL names a frame by a condition on the order values: RANGE BETWEEN UNBOUNDED PRECEDING AND CURRENT ROW holds of an occurrence the clause sorts at or before the current row, EXCLUDE GROUP adds that it is not a peer, and the union of several frames holds where one of them does. That is what a frame is, and FrameCond says it: not an arbitrary relation on order values, but one of these.

This is what lets every frame of the syntax be read back as a predicate of the query language (FrameCond.exists_condPred), so that deriving a window from an aggregation through the apply, which spells the frame out as a selection against the current row, asks nothing of the frame beyond containing its current row.

inductive FrameCond (T : Type) (p : ℕ) : Type

The condition a frame names, as a condition on the order value of an occurrence (the first argument) against the current row's (the second). OrderSpec.lt being OrderSpec.le reversed and negated, the strict cases are not a negation of the language but conditions of their own.

• whole {T : Type} {p : ℕ} : FrameCond T p

  Every occurrence of the partition: RANGE BETWEEN UNBOUNDED PRECEDING AND UNBOUNDED FOLLOWING, and the default under no clause.

• le {T : Type} {p : ℕ} (o : OrderSpec p) : FrameCond T p

  The clause sorts the occurrence at or before the current row.

• lt {T : Type} {p : ℕ} (o : OrderSpec p) : FrameCond T p

  …strictly before it, so the current row's peers are out.

• ge {T : Type} {p : ℕ} (o : OrderSpec p) : FrameCond T p

  …at or after the current row.

• gt {T : Type} {p : ℕ} (o : OrderSpec p) : FrameCond T p

  …strictly after it.

• and {T : Type} {p : ℕ} : FrameCond T p → FrameCond T p → FrameCond T p

  Both conditions, which is what an EXCLUDE modifier builds.

• or {T : Type} {p : ℕ} : FrameCond T p → FrameCond T p → FrameCond T p

  Either condition.

• orAll {T : Type} {p q : ℕ} (cs : Fin q → FrameCond T p) : FrameCond T p

  Any of several, which is the union of the frames of a multi-frame window.

• geOff {T : Type} {p : ℕ} (o : OrderSpec p) (k : Fin p) (pre : Bool) (a : T) : FrameCond T p

  An offset start, RANGE with a PRECEDING (pre) or a FOLLOWING as its first bound: the occurrence sorts, in column k of the clause, at or after the current row's value moved by a (FrameCond.shift). Where the current row's value is null the bound is CURRENT ROW, which is PostgreSQL's reading.

• leOff {T : Type} {p : ℕ} (o : OrderSpec p) (k : Fin p) (pre : Bool) (a : T) : FrameCond T p

  An offset end, b PRECEDING or b FOLLOWING as the last bound: the occurrence sorts at or before the moved value.

def FrameCond.shift {T : Type} [ValueType T] (cl : OrderCol) (pre : Bool) (a v : T) : T

The current row's value v moved by the offset a of a bound: back (a PRECEDING, pre) or forward (a FOLLOWING) in the column's direction, so down for an ascending column and up for a descending one.

Equations

• FrameCond.shift cl pre a v = if (pre != cl.desc) = true then v - a else v + a

def FrameCond.noOff {T : Type} {p : ℕ} : FrameCond T p → Bool

Whether the condition names no offset bound: every comparison is of the two order values as they stand. A frame with an offset applies + or - to the current row's value, which is a function the minimal signature does not have.

Equations

• FrameCond.whole.noOff = true
• (FrameCond.le o).noOff = true
• (FrameCond.lt o).noOff = true
• (FrameCond.ge o).noOff = true
• (FrameCond.gt o).noOff = true
• (a.and b).noOff = (a.noOff && b.noOff)
• (a.or b).noOff = (a.noOff && b.noOff)
• (FrameCond.orAll cs).noOff = (List.finRange q).all fun (j : Fin q) => (cs j).noOff
• (FrameCond.geOff o k pre a).noOff = false
• (FrameCond.leOff o k pre a).noOff = false

def FrameCond.holds {T : Type} {p : ℕ} [ValueType T] : FrameCond T p → Tuple T p → Tuple T p → Bool

Whether an occurrence with order value o' satisfies the condition against a current row with order value ov.

Equations

• FrameCond.whole.holds x✝¹ x✝ = true
• (FrameCond.le o).holds x✝¹ x✝ = o.le x✝¹ x✝
• (FrameCond.lt o).holds x✝¹ x✝ = o.lt x✝¹ x✝
• (FrameCond.ge o).holds x✝¹ x✝ = o.le x✝ x✝¹
• (FrameCond.gt o).holds x✝¹ x✝ = o.lt x✝ x✝¹
• (a.and b).holds x✝¹ x✝ = (a.holds x✝¹ x✝ && b.holds x✝¹ x✝)
• (a.or b).holds x✝¹ x✝ = (a.holds x✝¹ x✝ || b.holds x✝¹ x✝)
• (FrameCond.orAll cs).holds x✝¹ x✝ = (List.finRange q).any fun (j : Fin q) => (cs j).holds x✝¹ x✝
• (FrameCond.geOff o k pre a).holds x✝¹ x✝ = if ValueType.isNull (x✝ k) = true then (o k).le (x✝ k) (x✝¹ k) else (o k).le (FrameCond.shift (o k) pre a (x✝ k)) (x✝¹ k)
• (FrameCond.leOff o k pre a).holds x✝¹ x✝ = if ValueType.isNull (x✝ k) = true then (o k).le (x✝¹ k) (x✝ k) else (o k).le (x✝¹ k) (FrameCond.shift (o k) pre a (x✝ k))

def FrameCond.peers {T : Type} {p : ℕ} (o : OrderSpec p) : FrameCond T p

The current row's peer group: neither sorts before the other.

Equations

• FrameCond.peers o = (FrameCond.le o).and (FrameCond.ge o)

def FrameCond.notPeers {T : Type} {p : ℕ} (o : OrderSpec p) : FrameCond T p

Everything outside the current row's peer group. The order being total, this is a condition of the language and not a negation: an occurrence is not a peer exactly when one of the two sorts strictly before the other.

Equations

• FrameCond.notPeers o = (FrameCond.lt o).or (FrameCond.gt o)

structure ValueFrame (T : Type) (p : ℕ) : Type

A frame determined by values: the condition cond decides which other occurrences of the partition belong, from the two order values, and the flag self decides whether an occurrence belongs to its own frame.

Carrying the two separately is what distinguishes EXCLUDE CURRENT ROW from its peers: the current row and a peer have the same order value, so no condition on order values alone could drop one and keep the other.

• cond : FrameCond T p

  The condition the frame names.

• self : Bool

  Whether an occurrence is in its own frame.

The frames of SQL

A window of the algebra takes the frames of SQL that are determined by values, and no other: a frame clause reads every bound in the window's own ORDER BY. Its bounds are UNBOUNDED PRECEDING or CURRENT ROW at the start and CURRENT ROW or UNBOUNDED FOLLOWING at the end (RANGE and GROUPS agree on these, and ROWS agrees on the whole partition), which gives four conditions on the order values, and under a clause of exactly one column a RANGE frame may also start a PRECEDING or end b FOLLOWING (FrameCond.SqlBase, which says why the other offset frames are left out). An EXCLUDE modifier takes out nothing, the current row, its peer group, or its peers.

The offset itself is any value: SQL refuses a null or negative offset when the query runs, which no condition here can see, the syntax not knowing the domain's null or its zero. ValueFrame.IsSQL o w says that w is one of these under the clause o.

The language of FrameCond is wider: it combines comparisons under any clauses by and and or, so it names frames no frame clause of SQL gives, such as one comparing two order columns each on its own. The windows of the syntax carry IsSQL as a field, which is what keeps them out.

inductive FrameCond.SqlBase {T : Type} {p : ℕ} (o : OrderSpec p) : FrameCond T p → Prop

The conditions SQL's frame bounds name under the clause o: UNBOUNDED PRECEDING to UNBOUNDED FOLLOWING, UNBOUNDED PRECEDING to CURRENT ROW, CURRENT ROW to UNBOUNDED FOLLOWING, CURRENT ROW to CURRENT ROW, and the RANGE frames with an offset bound, which SQL allows under a clause of exactly one column (hk), with an a PRECEDING start or a b FOLLOWING end.

SQL's other offset frames, those that start a FOLLOWING or end b PRECEDING, are not among them. Such a frame holds its current row or not according to the row's value – not for a value and an offset a > 0, yes for a null value, whose bound is CURRENT ROW – whereas a frame here decides it once for every row (ValueFrame.self). The frames admitted all hold the current row, as self says.

• whole {T : Type} {p : ℕ} {o : OrderSpec p} : SqlBase o FrameCond.whole
• upTo {T : Type} {p : ℕ} {o : OrderSpec p} : SqlBase o (le o)
• from_ {T : Type} {p : ℕ} {o : OrderSpec p} : SqlBase o (ge o)
• peers {T : Type} {p : ℕ} {o : OrderSpec p} : SqlBase o (FrameCond.peers o)
• offFrom {T : Type} {p : ℕ} {o : OrderSpec p} {k : Fin p} (hk : ∀ (j : Fin p), j = k) (a : T) : SqlBase o (geOff o k true a)

  a PRECEDING to UNBOUNDED FOLLOWING.

• offUpTo {T : Type} {p : ℕ} {o : OrderSpec p} {k : Fin p} (hk : ∀ (j : Fin p), j = k) (b : T) : SqlBase o (leOff o k false b)

  UNBOUNDED PRECEDING to b FOLLOWING.

• offBoth {T : Type} {p : ℕ} {o : OrderSpec p} {k : Fin p} (hk : ∀ (j : Fin p), j = k) (a b : T) : SqlBase o ((geOff o k true a).and (leOff o k false b))

  a PRECEDING to b FOLLOWING.

• offToCur {T : Type} {p : ℕ} {o : OrderSpec p} {k : Fin p} (hk : ∀ (j : Fin p), j = k) (a : T) : SqlBase o ((geOff o k true a).and (le o))

  a PRECEDING to CURRENT ROW.

• curToOff {T : Type} {p : ℕ} {o : OrderSpec p} {k : Fin p} (hk : ∀ (j : Fin p), j = k) (b : T) : SqlBase o ((ge o).and (leOff o k false b))

  CURRENT ROW to b FOLLOWING.

inductive ValueFrame.IsSQLUnder {T : Type} {p : ℕ} (o : OrderSpec p) : ValueFrame T p → Prop

The frame is one of SQL's, written under the clause o: one of the four bounds, with one of the four EXCLUDE modifiers (NO OTHERS, CURRENT ROW, GROUP, TIES). The last two constructors are the rows strictly before and strictly after the current row's peers, which are EXCLUDE GROUP of the frames up to and from the current row written as one comparison.

• noOthers {T : Type} {p : ℕ} {o : OrderSpec p} {c : FrameCond T p} : FrameCond.SqlBase o c → IsSQLUnder o { cond := c, self := true }
• current {T : Type} {p : ℕ} {o : OrderSpec p} {c : FrameCond T p} : FrameCond.SqlBase o c → IsSQLUnder o { cond := c, self := false }
• group {T : Type} {p : ℕ} {o : OrderSpec p} {c : FrameCond T p} : FrameCond.SqlBase o c → IsSQLUnder o { cond := c.and (FrameCond.notPeers o), self := false }
• ties {T : Type} {p : ℕ} {o : OrderSpec p} {c : FrameCond T p} : FrameCond.SqlBase o c → IsSQLUnder o { cond := c.and (FrameCond.notPeers o), self := true }
• before {T : Type} {p : ℕ} {o : OrderSpec p} : IsSQLUnder o { cond := FrameCond.lt o, self := false }
• after {T : Type} {p : ℕ} {o : OrderSpec p} : IsSQLUnder o { cond := FrameCond.gt o, self := false }

def ValueFrame.IsSQL {T : Type} {p : ℕ} (o : OrderSpec p) (w : ValueFrame T p) : Prop

The frame is one of SQL's under the clause o: written under o, or under the reversed clause o.reverse. The second spelling names the same frames with their bounds mirrored, since o.reverse sorts a at or before b exactly when o sorts b at or before a (OrderSpec.le_reverse); it is what last_value and lag need, which read a frame of the clause backwards.

Equations

• ValueFrame.IsSQL o w = (ValueFrame.IsSQLUnder o w ∨ ValueFrame.IsSQLUnder o.reverse w)

theorem ValueFrame.IsSQL.of_reverse {T : Type} {p : ℕ} {o : OrderSpec p} {w : ValueFrame T p} (h : IsSQL o w) : IsSQL o.reverse w

A frame of SQL under a clause is one under the reversed clause.

def ValueFrame.ρ {T : Type} {p : ℕ} [ValueType T] (w : ValueFrame T p) : Tuple T p → Tuple T p → Bool

Whether an occurrence with order value o' is in the frame of one with order value o.

Equations

• w.ρ = w.cond.holds

def ValueFrame.s {T : Type} {p : ℕ} (w : ValueFrame T p) : Tuple T p → Bool

Whether an occurrence with order value o is in its own frame.

Equations

• w.s x✝ = w.self

def ValueFrame.ContainsSelf {T : Type} {p : ℕ} [ValueType T] (w : ValueFrame T p) : Prop

The frame contains its current row exactly when it contains its peers. Under this condition the frame of an occurrence depends only on its tuple, so a window over it does not need the occurrences told apart; EXCLUDE CURRENT ROW and EXCLUDE TIES are the frames that fail it.

Equations

• w.ContainsSelf = ∀ (o : Tuple T p), w.s o = w.ρ o o

def ValueFrame.mem {T : Type} {n m p : ℕ} [ValueType T] {α : Type} (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (w : ValueFrame T p) (r : OccFam α) (i j : Fin r.size) : Bool

Whether occurrence j is in the frame of occurrence i: same partition, and then s on itself or ρ on the order values.

Equations

• ValueFrame.mem val P O w r i j = (decide (P.key (val (r.row j)) = P.key (val (r.row i))) && if j = i then w.s (O.key (val (r.row i))) else w.ρ (O.key (val (r.row j))) (O.key (val (r.row i))))

def ValueFrame.frameIn {T : Type} {n m p : ℕ} [ValueType T] {α : Type} (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (w : ValueFrame T p) (r : OccFam α) (W : Finset (Fin r.size)) (i : Fin r.size) : Finset (Fin r.size)

The frame of an occurrence, among a set of present occurrences.

Equations

• ValueFrame.frameIn val P O w r W i = {j ∈ W | ValueFrame.mem val P O w r i j = true}

def ValueFrame.frame {T : Type} {n m p : ℕ} [ValueType T] {α : Type} (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (w : ValueFrame T p) (r : OccFam α) (i : Fin r.size) : Finset (Fin r.size)

The frame of an occurrence in the whole relation.

Equations

• ValueFrame.frame val P O w r i = ValueFrame.frameIn val P O w r Finset.univ i

def ValueFrame.ContainsCurrent {T : Type} {p : ℕ} (w : ValueFrame T p) : Prop

The frame contains its current row: s holds everywhere. A frame that does is read like a group – in a world where the row is present its frame has at least that row, so it is never empty. One that may exclude it can be empty while the row exists, and its aggregate then ranges over nothing.

The operator below decides this per row rather than per frame, by asking s of the row's own order value, which is decidable where this is not. The two agree wherever s is constant, which is every frame of SQL: true for the defaults, false for EXCLUDE CURRENT ROW and for the frame of the rows strictly before, and ρ o o for EXCLUDE TIES.

Equations

• w.ContainsCurrent = ∀ (o : Tuple T p), w.s o = true

The frames of SQL

The frames a WINDOW clause can name that are determined by values: the whole partition, the rows up to and including the current row's peers, the rows strictly before them, and the EXCLUDE variants of each. The ROWS frames with offsets – the previous row, the previous three – are not among them, and cannot be: which row is the previous one depends on which rows are present, so no relation on order values decides it.

def ValueFrame.whole {T : Type} {p : ℕ} : ValueFrame T p

The whole partition: SQL's default frame under no ORDER BY, and RANGE BETWEEN UNBOUNDED PRECEDING AND UNBOUNDED FOLLOWING.

Equations

• ValueFrame.whole = { cond := FrameCond.whole, self := true }

def ValueFrame.upTo {T : Type} {p : ℕ} : ValueFrame T p

RANGE BETWEEN UNBOUNDED PRECEDING AND CURRENT ROW read against the domain's own order on the order values: the current row, its peers, and everything that order puts before them.

A clause that names a direction and a null placement orders by its own reading, not by the domain's; the frame it determines is ValueFrame.rangeUpTo in Provenance.OrderSpec, and the two agree where every column is ASC and nothing is null.

Equations

• ValueFrame.upTo = { cond := FrameCond.le (OrderSpec.asc p), self := true }

def ValueFrame.before {T : Type} {p : ℕ} : ValueFrame T p

The rows the domain's own order puts strictly before the current row's peers: the frame a running total that must not read the row it annotates needs. It contains neither the row nor its peers, so it can be empty in a world where the row is present – which is why a window over it reads its token in the scalar convention. Its clause-determined counterpart is ValueFrame.rangeBefore in Provenance.OrderSpec.

Equations

• ValueFrame.before = { cond := FrameCond.lt (OrderSpec.asc p), self := false }

def ValueFrame.excludeCurrent {T : Type} {p : ℕ} (w : ValueFrame T p) : ValueFrame T p

EXCLUDE CURRENT ROW: the same frame with the current occurrence taken out, its peers left in. It is the modifier no relation on order values can express, which is why s is a field of its own.

Equations

• w.excludeCurrent = { cond := w.cond, self := false }

def ValueFrame.frameSeq {T : Type} {n m p : ℕ} [ValueType T] {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (w : ValueFrame T p) (r : OccFam α) (i : Fin r.size) : List α

The occurrence sequence of a frame: its occurrences with their annotations, in the canonical order of annotated tuples, as a group's are.

The order matters only to order-dependent aggregates, and the tie-break between occurrences carrying equal tuples is invisible to every reading of the token that is built from it.

Equations

• ValueFrame.frameSeq val P O w r i = ↑(Multiset.foldr sortedInsert ⟨[], ⋯⟩ (Multiset.map r.row (ValueFrame.frame val P O w r i).val))

def ValueFrame.frameSeqOn {T : Type} {n m p : ℕ} [ValueType T] {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) (r : OccFam α) (i : Fin r.size) : List α

The occurrence sequence of a frame, in the order its clause reads it: the frame's occurrences sorted by the clause on the order columns, with the canonical order on rows breaking the clause's ties. The tie-break is invisible to every symmetric aggregate, and it leaves two occurrences tied exactly when they carry the same row.

Equations

• ValueFrame.frameSeqOn val P O o w r i = OrderSpec.sortSeq O.key val o (ValueFrame.frameSeq val P O w r i)

def ValueFrame.frameSeqIn {T : Type} {n m p : ℕ} [ValueType T] {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (w : ValueFrame T p) (r : OccFam α) (W : Finset (Fin r.size)) (i : Fin r.size) : List α

The occurrence sequence of a frame among a set of present occurrences, canonically ordered. frameSeq is the case where every occurrence is present.

Equations

• ValueFrame.frameSeqIn val P O w r W i = ↑(Multiset.foldr sortedInsert ⟨[], ⋯⟩ (Multiset.map r.row (ValueFrame.frameIn val P O w r W i).val))

def ValueFrame.frameSeqOnIn {T : Type} {n m p : ℕ} [ValueType T] {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) (r : OccFam α) (W : Finset (Fin r.size)) (i : Fin r.size) : List α

The same read in the clause's order: what a window over a frame reads when only the occurrences of W are present.

Equations

• ValueFrame.frameSeqOnIn val P O o w r W i = OrderSpec.sortSeq O.key val o (ValueFrame.frameSeqIn val P O w r W i)

@[instance_reducible]

instance ValueFrame.annotatedTupleLinearOrder {T K : Type} {n : ℕ} [ValueType T] [HasAltLinearOrder K] : LinearOrder (AnnotatedTuple T K n)

The order in which a group or a frame reads its occurrences: the canonical one on annotated tuples, with the semiring's auxiliary order breaking ties between equal tuples. The tie-break is invisible to every reading of the token built from the sequence.

Equations

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

def OccFam.plain {T K : Type} {n : ℕ} (r : OccFam (AnnotatedTuple T K n)) : OccFam (Tuple T n)

The plain reading of a family of annotated occurrences: the same occurrences in the same order, their annotations forgotten.

Equations

• r.plain = { size := r.size, row := fun (i : Fin r.size) => (r.row i).1 }

theorem ValueFrame.sorted_map_fst {T K : Type} {n : ℕ} [ValueType T] [HasAltLinearOrder K] (s : Multiset (AnnotatedTuple T K n)) : List.map Prod.fst ↑(Multiset.foldr sortedInsert ⟨[], ⋯⟩ s) = ↑(Multiset.foldr sortedInsert ⟨[], ⋯⟩ (Multiset.map Prod.fst s))

Sorting annotated tuples and projecting is sorting the tuples. The canonical order reads the tuple first, so the tie-break between equal tuples is invisible after projection: the two lists are sorted and have the same elements.

def ValueFrame.token {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {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 : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (γ : Fin c → T := fun (x : Fin c) => 0) : AggValue T K

The token a window gives an occurrence: the aggregate over its frame, read in the convention that occurrence's frame warrants.

Whether the row is in its own frame is decided by s of its own order value. A row that is reads its aggregate as a group's, never over nothing; a row that is not may have an empty frame in a world where it is itself present, and its aggregate then ranges over no occurrence at all.

Equations

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

def ValueFrame.tokenDist {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] [AddCommMonoid K] {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) (dist : Bool) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (γ : Fin c → T := fun (x : Fin c) => 0) : AggValue T K

An occurrence's token, read over the frame's distinct values when the window asks for it: the same token with the occurrences of equal value merged, one per class in the domain's order and annotated by the ⊕ of its members.

Equations

• ValueFrame.tokenDist P O o w t f dist r i γ = if dist = true then (ValueFrame.token P O o w t f r i γ).mergeByValue else ValueFrame.token P O o w t f r i γ

The frame read off the relation

An occurrence's frame is a set of occurrences, but what it aggregates is a multiset of rows, and that multiset depends only on the relation and on the row the frame is computed for: the rows of the partition that the frame's relation accepts, with the occurrence's own row taken out and put back exactly as s says. Reading it this way is what lets a window be compared across a change of semiring or a restriction to a world, neither of which preserves an indexing.

def ValueFrame.frameOf {T : Type} {n m p : ℕ} [ValueType T] {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (w : ValueFrame T p) (X : Multiset α) (x : α) : Multiset α

The rows an occurrence's frame aggregates, read off the relation: the rows the frame's relation accepts, with one copy of the occurrence's own row removed and put back exactly when s holds.

Equations

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

def ValueFrame.frameListOf {T : Type} {n m p : ℕ} [ValueType T] {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) (X : Multiset α) (x : α) : List α

A frame's occurrence sequence in the clause's order, read off the relation.

Equations

• ValueFrame.frameListOf val P O o w X x = OrderSpec.sortSeq O.key val o (sortList (ValueFrame.frameOf val P O w X x))

theorem ValueFrame.frameListOf_of_peer {T : Type} {n m p : ℕ} [ValueType T] {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) (X : Multiset α) (x : α) (ho : ∀ (y z : Tuple T p), o.peer y z = true) (hval : ∀ (a b : α), a ≤ b → val a ≤ val b) : frameListOf val P O o w X x = sortList (frameOf val P O w X x)

A window with no ORDER BY reads its frame as a group is read. Where the clause separates nothing, every pair of order values is a peer, the reading order is the library's own order on rows, and a sequence already sorted that way is left alone.

def ValueFrame.tokenOf {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {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) (X : AnnotatedRelation T K n) (x : AnnotatedTuple T K n) (γ : Fin c → T := fun (x : Fin c) => 0) : AggValue T K

The token read off the relation. A window's token depends on the relation and on the row it is computed for, and on nothing else: which occurrence of an equal row it is decides nothing beyond what s decides for every one of them.

Equations

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

def ValueFrame.tokenOfDist {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] [AddCommMonoid K] {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) (dist : Bool) (X : AnnotatedRelation T K n) (x : AnnotatedTuple T K n) (γ : Fin c → T := fun (x : Fin c) => 0) : AggValue T K

The relation-level counterpart of ValueFrame.tokenDist.

Equations

• ValueFrame.tokenOfDist P O o w t f dist X x γ = if dist = true then (ValueFrame.tokenOf P O o w t f X x γ).mergeByValue else ValueFrame.tokenOf P O o w t f X x γ

A window aggregate under a FILTER clause

The operator's clause is read by exprWhen below, which keeps the frame whole and cuts what the leaf reads of it. The token here – the frame cut down to the occurrences the clause keeps, read in the scalar convention – is the cut-family reading that chain_count_zero_when_ne (in HavingQueryCounterexamples) refutes: with the family cut, the world holding only rejected rows is gone, and then a clause that keeps everything does not read as no clause. It remains as the machinery the expression's readings run on – the frame restriction (tokenOfWhen_filter_agg) and the merge (tokenOfDistWhen_specialize) are proved of it – and no operator builds one.

def ValueFrame.tokenOfWhen {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {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) (keep : Tuple T n → Bool) (X : AnnotatedRelation T K n) (x : AnnotatedTuple T K n) (γ : Fin c → T := fun (x : Fin c) => 0) : AggValue T K

The filtered token of a row of a relation: the aggregate over the occurrences of its frame the clause keeps, in the scalar convention. No operator builds one; it is the reading the clause had before the family was kept whole, and it survives as the carrier of the frame-restriction and merge arguments the expression's readings use.

Equations

• ValueFrame.tokenOfWhen P O o w t f keep X x γ = AggValue.ofScalarGroup f t (List.filter (fun (q : AnnotatedTuple T K n) => keep q.1) (ValueFrame.frameListOf Prod.fst P O o w X x)) γ

def ValueFrame.exprWhen {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] [AddCommMonoid K] {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) (dist : Bool) (keep : Tuple T n → Bool) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (γ : Fin c → T := fun (x : Fin c) => 0) : AggExpr T K

The column an occurrence's filtered window builds: one leaf over its frame – the whole frame, so the worlds are the frame's and a world holding only rejected rows is one of them – reading the occurrences the clause keeps, in the convention the row's membership of its own frame decides. Under DISTINCT the kept part is merged by value and the rejected occurrences stay unmerged and unread (AggExpr.ofSeqDistWhen).

Equations

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

def ValueFrame.exprWhenOf {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] [AddCommMonoid K] {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) (dist : Bool) (keep : Tuple T n → Bool) (X : AnnotatedRelation T K n) (x : AnnotatedTuple T K n) (γ : Fin c → T := fun (x : Fin c) => 0) : AggExpr T K

The relation-level counterpart, as tokenOf is for token.

Equations

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

def ValueFrame.tokenOfDistWhen {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] [AddCommMonoid K] {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) (dist : Bool) (keep : Tuple T n → Bool) (X : AnnotatedRelation T K n) (x : AnnotatedTuple T K n) (γ : Fin c → T := fun (x : Fin c) => 0) : AggValue T K

The cut-family window token of tokenOfWhen, merged by value under DISTINCT.

Equations

• ValueFrame.tokenOfDistWhen P O o w t f dist keep X x γ = if dist = true then (ValueFrame.tokenOfWhen P O o w t f keep X x γ).mergeByValue else ValueFrame.tokenOfWhen P O o w t f keep X x γ

theorem ValueFrame.collapse_token {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {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 : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) {γ : Fin c → T} : (token P O o w t f r i γ).collapse = f (List.map (fun (v : Tuple T n) => t.eval v γ) (frameSeqOn id P O o w r.plain i))

The token's deterministic reading is the plain aggregate over the frame – whichever convention the token is read in, since the convention decides what the worlds of a comparison are and not what the aggregate is over the whole relation.

theorem ValueFrame.collapse_tokenDist {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] [AddCommMonoid K] {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) (dist : Bool) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) {γ : Fin c → T} : (tokenDist P O o w t f dist r i γ).collapse = (if dist = true then f.distinct else f) (List.map (fun (v : Tuple T n) => t.eval v γ) (frameSeqOn id P O o w r.plain i))

The same for a token read over the frame's distinct values: its deterministic reading is the distinct aggregate of the frame.

The frames the clause determines

ρ o' o reads “an occurrence with order value o' is in the frame of one with order value o”, so the current row's value is the second argument.

def ValueFrame.rangeUpTo {T : Type} {p : ℕ} (o : OrderSpec p) : ValueFrame T p

RANGE BETWEEN UNBOUNDED PRECEDING AND CURRENT ROW under the clause o, SQL's default frame when a window names an ORDER BY: the current row, its peers, and everything the clause sorts before them.

Equations

• ValueFrame.rangeUpTo o = { cond := FrameCond.le o, self := true }

def ValueFrame.rangeBefore {T : Type} {p : ℕ} (o : OrderSpec p) : ValueFrame T p

The rows the clause sorts strictly before the current row's peers: RANGE BETWEEN UNBOUNDED PRECEDING AND CURRENT ROW EXCLUDE GROUP. It is the frame a running total that must not read the row it annotates needs, and it can be empty in a world where that row is present.

Equations

• ValueFrame.rangeBefore o = { cond := FrameCond.lt o, self := false }

def ValueFrame.rangeFrom {T : Type} {p : ℕ} (o : OrderSpec p) : ValueFrame T p

RANGE BETWEEN CURRENT ROW AND UNBOUNDED FOLLOWING: the current row, its peers, and everything the clause sorts after them. It is rangeUpTo under the reversed clause.

Equations

• ValueFrame.rangeFrom o = { cond := FrameCond.ge o, self := true }

def ValueFrame.rangeAfter {T : Type} {p : ℕ} (o : OrderSpec p) : ValueFrame T p

The rows the clause sorts strictly after the current row's peers: the frame lead reads.

Equations

• ValueFrame.rangeAfter o = { cond := FrameCond.gt o, self := false }

def ValueFrame.peerGroup {T : Type} {p : ℕ} (o : OrderSpec p) : ValueFrame T p

GROUPS BETWEEN CURRENT ROW AND CURRENT ROW: the current row's peer group, and nothing else.

Equations

• ValueFrame.peerGroup o = { cond := FrameCond.peers o, self := true }

def ValueFrame.excludeGroup {T : Type} {p : ℕ} (o : OrderSpec p) (w : ValueFrame T p) : ValueFrame T p

EXCLUDE GROUP: the frame with the current row and its peers taken out.

Equations

• ValueFrame.excludeGroup o w = { cond := w.cond.and (FrameCond.notPeers o), self := false }

def ValueFrame.excludeTies {T : Type} {p : ℕ} (o : OrderSpec p) (w : ValueFrame T p) : ValueFrame T p

EXCLUDE TIES: the frame with the current row's peers taken out, the row itself left in.

Equations

• ValueFrame.excludeTies o w = { cond := w.cond.and (FrameCond.notPeers o), self := w.self }

Which named frames are SQL's

def ValueFrame.tacticSql_frame : Lean.ParserDescr

Prove that a frame is one of SQL's: from a hypothesis, or from the shape of the frame, unfolding a named one; under a ∀ l, leaf by leaf.

Equations

• ValueFrame.tacticSql_frame = Lean.ParserDescr.node `ValueFrame.tacticSql_frame 1024 (Lean.ParserDescr.nonReservedSymbol "sql_frame" false)

def ValueFrame.tacticSql_frame_under : Lean.ParserDescr

sql_frame for one spelling of the clause (ValueFrame.IsSQLUnder).

Equations

• ValueFrame.tacticSql_frame_under = Lean.ParserDescr.node `ValueFrame.tacticSql_frame_under 1024 (Lean.ParserDescr.nonReservedSymbol "sql_frame_under" false)

def ValueFrame.«termSql_frame%» : Lean.ParserDescr

sql_frame run at once, as a term: unlike by sql_frame, which is postponed to the end of the enclosing term, it leaves no metavariable in the query it builds, so a goal about that query unfolds while the term is still being elaborated. Where the frame itself is not known yet, it is postponed like by sql_frame.

Equations

• ValueFrame.«termSql_frame%» = Lean.ParserDescr.node `ValueFrame.«termSql_frame%» 1024 (Lean.ParserDescr.symbol "sql_frame%")

Several frames of one partition: the expression a window computes

A distribution function reads two families: percent_rank and ntile the rows strictly before the current one and the whole partition, cume_dist the default RANGE frame and the whole partition. They are aggregate expressions and not aggregates, and the two families are nested, so reading the two aggregates separately would let a world of one disagree with a world of the other – a rank of three beside a count of one, which no world produces.

The operator is what can avoid that, because it is what knows the occurrences: it reads the union of its frames as one family and records, per leaf, which of those occurrences that leaf reads. Everything here is at the level of occurrence indices, so an EXCLUDE CURRENT ROW frame is as exact as any other: two occurrences carrying the same row are different indices.

def ValueFrame.unionFrame {T : Type} {p q : ℕ} (ws : Fin q → ValueFrame T p) : ValueFrame T p

The frame that is the union of several: an occurrence is in it when it is in one of them. Membership of the union is membership of one (mem_unionFrame).

Equations

• ValueFrame.unionFrame ws = { cond := FrameCond.orAll fun (j : Fin q) => (ws j).cond, self := (List.finRange q).any fun (j : Fin q) => (ws j).self }

def ValueFrame.exprIdx {T : Type} {n m p : ℕ} [ValueType T] {q : ℕ} {α : Type} [LinearOrder α] (val : α → Tuple T n) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ws : Fin q → ValueFrame T p) (r : OccFam α) (i : Fin r.size) : List (Fin r.size)

The occurrences a window's leaves read, in the clause's order: the union of the frames, as indices into the occurrence family.

Equations

• ValueFrame.exprIdx val P O o ws r i = ValueFrame.frameSeqOn (fun (j : Fin r.size) => val (r.row j)) P O o (ValueFrame.unionFrame ws) { size := r.size, row := id } (Fin.cast ⋯ i)

def ValueFrame.exprOfVals {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {q : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ws : Fin q → ValueFrame T p) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (vals : Fin q → Fin r.size → T) (fs : Fin q → SeqAggFunc T) (g : (Fin q → T) → T) : AggExpr T K

The aggregate expression a multi-frame window computes for one occurrence. The shared family is the union of the frames, read in the clause's order; leaf l reads the occurrences of its own frame ws l, aggregates them with fs l over the term ts l, and the expression's own function g combines the leaves' values world by world. Leaf l is read in the scalar convention exactly where the occurrence is not in its own frame ws l, which is the convention ValueFrame.token gives a single-frame window.

Equations

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

def ValueFrame.exprOfValsWhen {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {q : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ws : Fin q → ValueFrame T p) (keeps : Fin q → Option (Selection T n)) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (vals : Fin q → Fin r.size → T) (fs : Fin q → SeqAggFunc T) (g : (Fin q → T) → T) : AggExpr T K

The same with a FILTER clause on each leaf: the family and the frames are the ones exprOfVals builds – a clause changes neither – and what a clause cuts is its own leaf's reads, the second flag family of Provenance.AggExpr.

So the worlds are the window's own, a filtered-out occurrence still carrying its annotation to them, and what the clause changes is what the leaf aggregates there. The conventions are the unfiltered ones: a clause does not make a leaf scalar, since the world in which only rejected rows are present is a world of the frame, and the leaf reads f [] in it. Cutting the family instead loses that world, and then no convention is right (chain_count_zero_when_ne, in HavingQueryCounterexamples).

Equations

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

def ValueFrame.exprOf {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {q c : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ws : Fin q → ValueFrame T p) (ts : Fin q → TermIn T c n) (fs : Fin q → SeqAggFunc T) (g : (Fin q → T) → T) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (γ : Fin c → T := fun (x : Fin c) => 0) : AggExpr T K

The same, reading each leaf's value off its term: what the operator builds. Separating the values from the terms is what lets a lemma vary them, since the expression's later fields depend on the occurrence list and so on the values (exprOfVals_congr).

Equations

• ValueFrame.exprOf P O o ws ts fs g r i γ = ValueFrame.exprOfVals P O o ws r i (fun (l : Fin q) (j : Fin r.size) => (ts l).eval (r.row j).1 γ) fs g

def ValueFrame.exprOfWhen {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {q c : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ws : Fin q → ValueFrame T p) (ts : Fin q → TermIn T c n) (fs : Fin q → SeqAggFunc T) (g : (Fin q → T) → T) (keeps : Fin q → Option (Selection T n)) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (γ : Fin c → T := fun (x : Fin c) => 0) : AggExpr T K

The same with a FILTER clause on each leaf, reading each clause against the occurrence's own tuple: what the operator builds. See exprOfValsWhen for what a clause cuts and what it leaves.

Equations

• ValueFrame.exprOfWhen P O o ws ts fs g keeps r i γ = ValueFrame.exprOfValsWhen P O o ws keeps r i (fun (l : Fin q) (j : Fin r.size) => (ts l).eval (r.row j).1 γ) fs g

theorem ValueFrame.collapse_exprOfWhen {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {q c : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (ws : Fin q → ValueFrame T p) (ts : Fin q → TermIn T c n) (fs : Fin q → SeqAggFunc T) (g : (Fin q → T) → T) (keeps : Fin q → Option (Selection T n)) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (γ : Fin c → T) : (exprOfWhen P O o ws ts fs g keeps r i γ).collapse = g fun (l : Fin q) => fs l (List.map (fun (v : Tuple T n) => (ts l).eval v γ) (match keeps l with | none => frameSeqOn id P O o (ws l) r.plain i | some φ => List.filter φ.keeps (frameSeqOn id P O o (ws l) r.plain i)))

The deterministic reading of a filtered multi-frame window: each leaf's plain aggregate over the part of its own frame its own clause keeps, combined by g.

The shared family read off the relation

The family is listed by occurrence index, but under ContainsSelf the indices drop out of every reading: membership is the frame's own test on the tuples (mem_of_containsSelf), so the family is the rows the union frame selects, in the clause's order. That is what lets two indexings of one relation – or one relation over two annotation semirings – be compared.

theorem ValueFrame.occs_exprOfWhen {T K : Type} {n m p : ℕ} [ValueType T] [HasAltLinearOrder K] {q c : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) {ws : Fin q → ValueFrame T p} (hcs : ∀ (l : Fin q), (ws l).ContainsSelf) (ts : Fin q → TermIn T c n) (fs : Fin q → SeqAggFunc T) (g : (Fin q → T) → T) (keeps : Fin q → Option (Selection T n)) (r : OccFam (AnnotatedTuple T K n)) (i : Fin r.size) (γ : Fin c → T) : (exprOfWhen P O o ws ts fs g keeps r i γ).occs = List.map (fun (y : AnnotatedTuple T K n) => (fun (l : Fin q) => (ts l).eval y.1 γ, y.2, fun (l : Fin q) => decide (P.key y.1 = P.key (r.row i).1) && (ws l).ρ (O.key y.1) (O.key (r.row i).1), fun (l : Fin q) => match keeps l with | none => true | some φ => φ.keeps y.1)) (List.map r.row (exprIdx Prod.fst P O o ws r i))

The same for a filtered window: a clause tests the occurrence's own tuple, so the family is still a function of the rows and of the tuple the column is computed for.

Home · Documentation · Publications · Contributors · Source · Cite