The successor relation of a finite relation, without a recursion

A relation of non-null rows, listed once each, is sorted by the lexicographic ascending order (ascLt). Its successor relation – the pairs of consecutive rows – its least row and its greatest row are written with products, selections, projections and the NOT IN difference: a pair of rows in increasing order with no row between them, a row with no row below it, a row with no row above it (Sym.evaluatePlain_succQ, Sym.evaluatePlain_leastQ, Sym.evaluatePlain_greatestQ). These are what a bounded recursion's counters and the gaps of a cut are read off.

Consecutive elements of a sorted list

The sorted listing of a relation

noncomputable def Sym.sortedRows {T : Type} [ValueType T] {p : ℕ} (R : Multiset (Tuple T p)) : List (Tuple T p)

The listing of a relation's rows in increasing order.

Equations

• Sym.sortedRows R = R.toFinset.sort (ascLe p)

The comparison as a predicate

def Sym.ltOn {T : Type} [ValueType T] {c N p : ℕ} (x y : Fin p → Fin N) : GenPredIn T c (ColKind.allReg N)

One block of a row below another, in the ascending lexicographic order.

Equations

• Sym.ltOn x y = (OrderSpec.asc p).ltPredOn (fun (k : Fin p) => TermGIn.index (x k) ⋯) (fun (k : Fin p) => TermGIn.index (y k) ⋯) (List.finRange p)

The two blocks of a row

def Sym.blockL' {T : Type} (a b : ℕ) (x : Tuple T (a + b)) : Tuple T a

The first block of a row.

Equations

• Sym.blockL' a b x i = x (Fin.castAdd b i)

def Sym.blockR' {T : Type} (a b : ℕ) (x : Tuple T (a + b)) : Tuple T b

The second block of a row.

Equations

• Sym.blockR' a b x i = x (Fin.natAdd a i)

Products and projections

def Sym.projQ {T : Type} {c N M : ℕ} {l : List (String × ℕ)} (F : Fin M → SA T c N) (q : AggQueryIn T c N (ColKind.allReg N) l) : AggQueryIn T c M (ColKind.allReg M) l

A projection onto arguments: columns, constants and context values.

Equations

• Sym.projQ F q = AggQueryIn.castKind ⋯ (AggQueryIn.Proj (Sym.projSA F) q)

The order queries

def Sym.ltQ {T : Type} [ValueType T] {c p : ℕ} (R : AggQueryIn T c p (ColKind.allReg p)) : AggQueryIn T c (p + p) (ColKind.allReg (p + p))

The pairs of rows in increasing order.

Equations

• Sym.ltQ R = AggQueryIn.Sel (Sym.ltOn (Fin.castAdd p) (Fin.natAdd p)) (Sym.prodR R R) trivial

def Sym.midQ {T : Type} [ValueType T] {c p : ℕ} (R : AggQueryIn T c p (ColKind.allReg p)) : AggQueryIn T c (p + p) (ColKind.allReg (p + p))

The pairs of rows with a row between them.

Equations

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

def Sym.aboveQ {T : Type} [ValueType T] {c p : ℕ} (R : AggQueryIn T c p (ColKind.allReg p)) : AggQueryIn T c p (ColKind.allReg p)

The rows with a row below them.

Equations

• Sym.aboveQ R = Sym.projQ (fun (k : Fin p) => Sym.SA.col (Fin.natAdd p k)) (Sym.ltQ R)

def Sym.belowQ {T : Type} [ValueType T] {c p : ℕ} (R : AggQueryIn T c p (ColKind.allReg p)) : AggQueryIn T c p (ColKind.allReg p)

The rows with a row above them.

Equations

• Sym.belowQ R = Sym.projQ (fun (k : Fin p) => Sym.SA.col (Fin.castAdd p k)) (Sym.ltQ R)

def Sym.succQ {T : Type} [ValueType T] {c p : ℕ} (s₁ s₂ : String) (cnt : SeqAggFunc T) (R : AggQueryIn T c p (ColKind.allReg p)) : AggQueryIn T c (p + p) (ColKind.allReg (p + p))

The successor relation.

Equations

• Sym.succQ s₁ s₂ cnt R = AggQueryIn.notInDiffX s₁ s₂ cnt (Sym.ltQ R) (Sym.midQ R)

def Sym.leastQ {T : Type} [ValueType T] {c p : ℕ} (s₁ s₂ : String) (cnt : SeqAggFunc T) (R : AggQueryIn T c p (ColKind.allReg p)) : AggQueryIn T c p (ColKind.allReg p)

The least row.

Equations

• Sym.leastQ s₁ s₂ cnt R = AggQueryIn.notInDiffX s₁ s₂ cnt R (Sym.aboveQ R)

def Sym.greatestQ {T : Type} [ValueType T] {c p : ℕ} (s₁ s₂ : String) (cnt : SeqAggFunc T) (R : AggQueryIn T c p (ColKind.allReg p)) : AggQueryIn T c p (ColKind.allReg p)

The greatest row.

Equations

• Sym.greatestQ s₁ s₂ cnt R = AggQueryIn.notInDiffX s₁ s₂ cnt R (Sym.belowQ R)

def Sym.NonNullRows {T : Type} [ValueType T] {c p : ℕ} (R : AggQueryIn T c p (ColKind.allReg p)) (D : Database T) (γ : Fin c → T) : Prop

What the relation's rows are asked: no null value.

Equations

• Sym.NonNullRows R D γ = ∀ (x : Tuple T p), Multiset.Mem (R.evaluatePlain D γ) x → ∀ (i : Fin p), ValueType.isNull (x i) = false

theorem Sym.evaluatePlain_succQ {T : Type} [ValueType T] {c p : ℕ} {R : AggQueryIn T c p (ColKind.allReg p)} {D : Database T} {γ : Fin c → T} (s₁ s₂ : String) {cnt : SeqAggFunc T} (hc : cnt.Counts) (h₁ : AggQueryIn.noMention s₁ R) (h₂ : AggQueryIn.noMention s₂ R) (hR : NonNullRows R D γ) (hnd : Multiset.Nodup (R.evaluatePlain D γ)) : (succQ s₁ s₂ cnt R).evaluatePlain D γ = succRel (sortedRows (R.evaluatePlain D γ))

The successor relation, as a query.

theorem Sym.evaluatePlain_leastQ {T : Type} [ValueType T] {c p : ℕ} {R : AggQueryIn T c p (ColKind.allReg p)} {D : Database T} {γ : Fin c → T} (s₁ s₂ : String) {cnt : SeqAggFunc T} (hc : cnt.Counts) (h₁ : AggQueryIn.noMention s₁ R) (h₂ : AggQueryIn.noMention s₂ R) (hR : NonNullRows R D γ) (hnd : Multiset.Nodup (R.evaluatePlain D γ)) (h0 : 0 < (sortedRows (R.evaluatePlain D γ)).length) : (leastQ s₁ s₂ cnt R).evaluatePlain D γ = {(sortedRows (R.evaluatePlain D γ))[0]}

The least row is the first of the sorted listing.

Home · Documentation · Publications · Contributors · Source · Cite