Formal Foundations and Proofs

In the chapter on the algebra of regular time series I presented a set of operators together with the equations describing them. I deliberately omitted formal proofs there — I wanted to first show what the system does before explaining why it is allowed to do so. This page fills that gap. Here I gather the formal skeleton of the algebra: the connection between the stream operators and covering-system theory, along with proofs of the theorems underlying the correctness and optimization of query plans.

ℹ️ Info

The entire construction below stays within a single domain — the rational numbers. This is not a stylistic choice. It is the whole point. Beatty’s theorem needs irrational numbers, which a computer does not have. Fraenkel’s theorem lets us descend to rational numbers. The proofs on this page show that the interleaving and de-interleaving operations are a special case of Beatty sequences satisfying Fraenkel’s postulates — and are therefore realizable using rational numbers alone.

Covering systems as the foundation

The literature on covering systems [4] belongs to combinatorics and cryptanalysis within number theory. The problem under consideration is how to determine a partition of the set of positive natural numbers. We say that two sequences partition the set of positive natural numbers if the sets formed from the elements of these sequences have an empty intersection, and their union forms the set of positive natural numbers.

The basis for these considerations is the parameterized Beatty sequence. In its general form it is written using the floor function:

\[ \mathcal{B}(\alpha ,\alpha ^{\prime }) := \left( \left\lfloor \frac{n-\alpha ^{\prime }}{\alpha }\right\rfloor \right) _{n=1}^{\infty } \]

This single definition generates an entire family of sequences. Partition results always concern a pair of its instances with different parameters: we write the pair as B(α, α′) and B(β, β′), where the second notation denotes the complementary term.

The parameters of this sequence have a clear geometric interpretation:

• α denotes the density of the sequence,
• 1/α denotes the slope,
• α′ denotes the offset,
• −α′/α denotes the y-intercept (the point where it crosses the y-axis).

The Beatty theorem guarantees a partition of the set for irrational numbers. The Fraenkel theorem is a generalization that — crucially for us — also allows rational numbers, provided five postulates are satisfied (quoted in the introductory chapter). An accessible proof of Fraenkel’s theorem can be found in K. O’Bryant’s paper “Fraenkel’s partition and Brown’s decomposition” [23].

The remainder of this page boils down to a single idea: showing that the stream operators are, in essence, machines generating Beatty sequences that partition (cover) the set of natural numbers.

Tools: floor and ceiling properties

The proofs rely almost exclusively on the floor function (⌊x⌋ — the integer part) and the ceiling function (⌈x⌉ — the smallest integer not less than x). I therefore first present a set of identities that will be used repeatedly. Let x ∈ ℝ, and let C denote an integer:

\[ \left\lfloor x\right\rfloor = \left\lceil x\right\rceil \iff x \in \mathbb{Z} \]

\[ \left\lfloor x\right\rfloor + 1 = \left\lceil x\right\rceil \iff x \in \mathbb{R} \setminus \mathbb{Z} \]

\[ \left\lfloor x + C\right\rfloor = \left\lfloor x\right\rfloor + C \]

(the last identity holds for every C ∈ ℤ). Additionally, in analyzing the residue of the de-interleaving sequence we will use relationships tying the greatest common divisor (gcd) to the domain of the quotient a/b. For a, b ∈ ℕ_>0:

\[ \operatorname{gcd}(a,b) = b \iff \frac{a}{b} \in \mathbb{N} \]

and otherwise:

\[ 1 \leq \operatorname{gcd}(a,b) \leq \min(a,b) \]

These two cases disjointly cover the entire domain of interest to us — which will let us carry out a proof “by cases.”

Operators in formal notation

The operators introduced in the query language have their formal counterparts. The table below ties the formal notation (used in the proofs) to the symbols found in the query language:

For the proofs to be self-contained, I restate two definitions I will refer to directly.

Interleaving φ(A, B) produces an output stream whose successive tuples are determined by the rule:

\[ c_{n}= \left\{ \begin{array}{cc} b_{n-\left\lfloor n z \right\rfloor } & \left\lfloor n z \right\rfloor = \left\lfloor \left( n+1\right) z \right\rfloor \\ a_{\left\lfloor n z \right\rfloor } & \left\lfloor n z \right\rfloor \neq \left\lfloor \left( n+1\right) z \right\rfloor \end{array} \right. , \ z = \frac{\Delta _{b}}{\Delta _{a}+\Delta _{b}}, \ \Delta _{c}=\frac{\Delta _{a}\Delta _{b}}{\Delta _{a}+\Delta _{b}} \]

De-interleaving is defined by two complementary formulas — operator Θ, which recovers the original stream, and operator ∼Θ, which determines the “remainder” of the de-interleaving:

\[ a_{n} = c_{n+ \left\lceil \frac{(n+1)\Delta _{a}}{\Delta _{b}} \right\rceil },\ \Delta _{a}=\frac{\Delta _{c}\Delta _{b}}{\left\vert \Delta _{c}-\Delta _{b}\right\vert } \]

\[ b_{n} = c_{n+\left\lfloor \frac{n\Delta_{b}}{\Delta_{a}}\right\rfloor},\ \Delta_{b}=\frac{\Delta_{c}\Delta_{a}}{\left\vert \Delta_{c}-\Delta_{a}\right\vert } \]

Theorem 1: interleaving guarantees set coverage

✅ Note

Theorem. The interleaving operation guarantees sequential coverage of both index sets of the data streams that are its arguments: every element of stream A and every element of stream B is selected exactly once, in order, without gaps and without repetition.

Proof. Since 0 < z < 1, the increment

\[ d_{n} := \left\lfloor \left( n+1\right) z \right\rfloor - \left\lfloor n z \right\rfloor \]

equals 0 or 1 for every n ≥ 0. The interleaving equation selects an element of stream B exactly at those steps where d_n = 0 (the equality branch), and an element of stream A exactly at steps where d_n = 1.

Consider the selection index for sequence B: x_n = n − ⌊nz⌋. In a single step, x_n+1 − x_n = 1 − d_n: the index increases by exactly 1 at every step selecting from B, and otherwise remains unchanged. So if n < n′ are two consecutive steps selecting from B, then x_n′ = x_n + 1. The first step selecting from B is n = 0, since 0 < z < 1 implies ⌊0⌋ = ⌊z⌋ = 0, i.e. d₀ = 0, and x₀ = 0. Selections from sequence B therefore use indices 0, 1, 2, … in order, without gaps or repetitions.

Symmetrically: the selection index for sequence A, i.e. ⌊nz⌋, increases by exactly 1 at every step selecting from A (d_n = 1), and otherwise remains unchanged; at the first such step its value is 0 (all earlier steps have d = 0). The elements of sequence A are therefore also selected exactly once each, in order. ∎

Theorem 2: de-interleaving satisfies Fraenkel’s postulates

This is the central theorem of this page. It proves that the two sequences describing the de-interleaving operation are a special case of Beatty sequences satisfying the postulates of Fraenkel’s theorem for rational numbers. Without this theorem, the whole system remains merely a promise.

✅ Note

Theorem. Let a, b ∈ ℕ_>0 represent the rational ratio of the rates of the component streams, ∆_a/∆_b = a/b. Both tuple-selection sequences describing the de-interleaving operation are — up to the index alignment shown in the proof — a special case of Beatty sequences satisfying the postulates of Fraenkel’s theorem for rational parameters. Consequently they partition the set ℕ₀ := ℕ ∪ {0}, i.e. the index set of the interleaved stream, and de-interleaving exactly inverts interleaving using rational-number arithmetic alone.

Proof — part one (reduction to Beatty form). The tuple-selection sequence for the de-interleaving residue (operator ∼Θ) has the form:

\[ \left( n + \left\lfloor \frac{nb}{a} \right\rfloor \right) _{n=0}^{\infty } \]

Its initial term (n = 0) equals 0; the terms for n ≥ 1 form the Beatty part. For n ∈ ℕ, by the property ⌊x + C⌋ = ⌊x⌋ + C, we have n + ⌊nb/a⌋ = ⌊n + nb/a⌋, so we seek α, α′ such that:

\[ \left( \left\lfloor \frac{n-\alpha ^{\prime }}{\alpha }\right\rfloor \right) _{n=1}^{\infty } = \left( \left\lfloor n\frac{a + b}{a} \right\rfloor \right) _{n=1}^{\infty } \]

Reading off the slope and the offset: with a shift of α′ = 0 we obtain α = a/(a+b), and the selection sequence restricted to n ≥ 1 is exactly:

\[ \mathcal{B}\!\left( \frac{a}{a + b}, 0 \right) = \left( \left\lfloor n\frac{a + b}{a} \right\rfloor \right) _{n=1}^{\infty } \]

Proof — part two (verifying the five postulates and determining the residue). We check the postulates of Fraenkel’s theorem in turn for α = a/(a+b), α′ = 0:

1. The value α = a/(a+b) for a, b > 0 is greater than zero and less than one.
2. The condition α + β = 1 is satisfied for β = b/(a+b).
3. For α′ = 0 the postulate is equivalent to postulate 1.
4. The postulate is vacuous, since α is a rational number.
5. The smallest number q for which qα ∈ ℕ is q = (a+b)/gcd(a,b); then the condition 1/q ≤ α + α′ = α is satisfied, and the condition ⌈qα′⌉ + ⌈qβ′⌉ = 1 with α′ = 0 forces ⌈qβ′⌉ = 1, i.e. 0 < β′ ≤ gcd(a,b)/(a+b). Every admissible value generates the same sequence (the complement of the sequence B(a/(a+b), 0) in ℕ is unique); we take β′ = gcd(a,b)/(a+b).

The sequence complementing B(a/(a+b), 0) in the sense of Fraenkel’s postulates is therefore:

\[ \mathcal{B}\!\left( \frac{b}{a + b}, \frac{\operatorname{gcd}(a, b)}{a + b} \right) \]

After reindexing n ↦ n + 1, so that it runs from n = 0 — matching the selection sequences in the definition of de-interleaving — it takes the form:

\[ \left( \left\lfloor \frac{(n + 1) - \frac{\operatorname{gcd}(a,b)}{a+b}}{\frac{b}{a+b}} \right\rfloor \right) _{n=0}^{\infty } \]

Expanding the above expression:

\[ \left\lfloor \frac{(n + 1) - \frac{\operatorname{gcd}(a,b)}{a+b}}{\frac{b}{a+b}} \right\rfloor = \left\lfloor n\frac{a}{b} + n + \frac{a}{b} + 1 - \frac{\operatorname{gcd}(a, b)}{b} \right\rfloor \]

Comparing this — term by term for n ≥ 0 — with the tuple-selection sequence of the recovered stream (operator Θ):

\[ \left( n + \left\lceil \frac{(n + 1)a}{b} \right\rceil \right) _{n=0}^{\infty } \]

and factoring out the integer part n + 1 via the property ⌊x + C⌋ = ⌊x⌋ + C, the claim reduces (after substituting n for n + 1, so that n ranges over ℕ_>0) to the identity:

\[ \left\lfloor n\frac{a}{b} - \frac{\operatorname{gcd}(a, b)}{b} \right\rfloor + 1 = \left\lceil n\frac{a}{b} \right\rceil ,\quad n \in \mathbb{N}_{>0} \]

Proof — part three (case analysis). Using the properties of the coefficient gcd(a, b), we consider two disjoint cases covering the entire domain.

Case 1: gcd(a, b) = b, i.e. a/b ∈ ℕ. Then n·a/b ∈ ℕ, so by the identity ⌊x⌋ = ⌈x⌉ ⟺ x ∈ ℤ we have ⌈n·a/b⌉ = ⌊n·a/b⌋, and by ⌊x + C⌋ = ⌊x⌋ + C:

\[ \left\lfloor n\frac{a}{b} - 1 \right\rfloor + 1 = \left\lfloor n\frac{a}{b} \right\rfloor \]

Both sides of the identity being proved coincide.

Case 2: b ∤ a, i.e. 1 ≤ gcd(a, b) < b and 0 < gcd(a,b)/b < 1.

If n·a/b ∉ ℤ, then by ⌊x⌋ + 1 = ⌈x⌉ ⟺ x ∈ ℝ ∖ ℤ we have ⌈n·a/b⌉ = ⌊n·a/b⌋ + 1. The fractional part of n·a/b is a nonzero multiple of gcd(a,b)/b, and hence at least gcd(a,b)/b; subtracting gcd(a,b)/b from n·a/b therefore cannot drop below the integer ⌊n·a/b⌋, whence:

\[ \left\lfloor n\frac{a}{b} - \frac{\operatorname{gcd}(a, b)}{b} \right\rfloor = \left\lfloor n\frac{a}{b} \right\rfloor \]

and the identity being proved holds.

If n·a/b ∈ ℤ, then ⌈n·a/b⌉ = n·a/b, and since 0 < gcd(a,b)/b < 1:

\[ \left\lfloor n\frac{a}{b} - \frac{\operatorname{gcd}(a, b)}{b} \right\rfloor = n\frac{a}{b} - 1 \]

which again gives the identity being proved.

Both selection sequences describing the de-interleaving operation are therefore — up to the unit reindexing from part two — Beatty sequences satisfying Fraenkel’s postulates for rational parameters: the pair B(a/(a+b), 0) and B(b/(a+b), gcd(a,b)/(a+b)) partitions the set ℕ, and together with the initial residue term 0 from part one — the set ℕ₀, the full index set of the interleaved stream. The recovered stream and the residue are therefore exact. ∎

✅ Note

Corollary (exact invertibility over the rationals). For streams with rational rates, the operators Θ and ∼Θ recover the component streams of φ(A, B) exactly (bit for bit): no tuple is lost, duplicated, or reordered relative to its component stream. The pair (φ; Θ, ∼Θ) therefore behaves like multiplication and division, and the pair (Σ; δ) like addition and subtraction, on the set of regular time series.

⚠️ Warning

The practical takeaway from this proof: the implementation must never leave the domain of rational numbers, not even momentarily. An implicit cast of an intermediate result to a floating-point number breaks the assumptions of the theorem above. Materialization into floating-point form must be deferred until an explicit application of the floor or ceiling operation.

Operator properties used in optimization

Based on the algebra presented, a number of properties of data streams can be shown. They have direct application in the data-management system — during query-plan optimization and result interpretation.

Disruption of event ordering

✅ Note

Theorem. The order of elements in a stream does not reflect the actual order in which the elements occurred in the real world.

Proof (by counterexample). Consider two streams:

Alpha(char),2:   {1,2,3,4,5,6,...}
Epsilon(char),3: {a,b,c,d,e,f,...}

The expression φ(Epsilon, Alpha) produces the output stream:

Tau(char),6/5:   {1,2,a,3,b,4,5,c,6,d,...}

In stream Tau, the tuple labeled c occurs after the tuple labeled 5. Yet tuple c appears in stream Epsilon at second 9, while tuple 5 appears in stream Alpha at second 10. The natural order of events has been violated in the resulting stream. Conclusion: when analyzing time embedded in streams, applying the de-interleaving operation is necessary to recover the original form of the data streams. ∎

Commutativity of summation

✅ Note

Theorem. The stream-summation operation, disregarding attribute order, is commutative.

Proof. Assume ∆_a ≤ ∆_b; the opposite case is symmetric. The first case of the sum definition gives, as the n-th element of stream Σ(A, B), the tuple:

\[ c_{n} = \left( a_{n},\ b_{\left\lfloor n\Delta_{a}/\Delta_{b} \right\rfloor} \right) \]

whereas for Σ(B, A) the roles of the arguments are swapped, and its second case applies (or, at ∆_a = ∆_b, its first), giving as the n-th element:

\[ c_{n} = \left( b_{\left\lfloor n\Delta_{a}/\Delta_{b} \right\rfloor},\ a_{n} \right) \]

Both streams carry ∆_c = ∆_a. They therefore coincide up to the order of the joined attributes. ∎

Interleaving alignment method

The interleaving operation is not commutative in general: since 0 < z < 1, at n = 0 the equality branch of the interleaving definition always applies, so the stream φ(A, B) begins with element b₀, while the stream φ(B, A) begins with element a₀. Interleaving is, however, equivariant with respect to time shifts matched to the streams’ rates — which is valuable for query-plan optimization.

✅ Note

Theorem. If numbers i, k ∈ ℕ are chosen such that i·∆_a = k·∆_b (both arguments shifted by the same amount of time), then interleaving the shifted streams equals the interleaving of the original streams shifted by the sum of these numbers.

Formally:

\[ \varphi \left( \tau_{i}(A), \tau_{k}(B) \right) = \tau_{i+k}\left( \varphi (A, B) \right), \quad i\Delta_{a} = k\Delta_{b}, \quad i, k \in \mathbb{N} \]

Proof. Both sides carry the interval ∆_c from the definition of interleaving, so it suffices to compare the elements. From the assumption i·∆_a = k·∆_b:

\[ (i+k) z = (i+k) \frac{\Delta_{b}}{\Delta_{a}+\Delta_{b}} = \frac{i\Delta_{b} + i\Delta_{a}}{\Delta_{a}+\Delta_{b}} = i \in \mathbb{N} \]

and hence, by the property ⌊x + C⌋ = ⌊x⌋ + C, for every n ≥ 0 and m := n + i + k:

\[ \left\lfloor m z \right\rfloor = \left\lfloor n z + i \right\rfloor = \left\lfloor n z \right\rfloor + i \]

In particular ⌊mz⌋ = ⌊(m+1)z⌋ if and only if ⌊nz⌋ = ⌊(n+1)z⌋: position n on the left-hand side of the claim and position m of stream φ(A, B) select the same branch of the interleaving definition. On the equality branch the right-hand side selects the element:

\[ b_{m - \left\lfloor m z \right\rfloor} = b_{n+i+k - \left\lfloor n z \right\rfloor - i} = b_{(n - \left\lfloor n z \right\rfloor) + k} \]

which is exactly the element (τ_k(B))_n−⌊nz⌋ selected by the left-hand side; on the inequality branch it selects:

\[ a_{\left\lfloor m z \right\rfloor} = a_{\left\lfloor n z \right\rfloor + i} \]

which is the element (τ_i(A))_⌊nz⌋ — again matching the left-hand side. Both streams coincide element by element. ∎

Why this matters

The theorems presented are not formalism for its own sake. Each of them plays a concrete role in the working system:

• Theorems 1 and 2 guarantee that the pairs of operations interleaving/de-interleaving and sum/difference are complementary — data is neither lost nor duplicated in an uncontrolled way. They are what allow us to treat these operations like multiplication/division and addition/subtraction on the set of regular time series.
• Theorem 2 in particular proves that the entire construction can be realized using rational numbers alone — and thus deterministically and exactly on a computer. This is the condition without which RetractorDB could not exist.
• The theorems on operator properties (commutativity of summation, interleaving alignment, ordering disruption) provide rewrite rules for stream expressions. The query-plan optimizer uses them to transform plans into cheaper-to-execute forms without changing the result.

The branch of mathematics in which these equations are situated is the theory of covering systems [4] within number theory. I presented the full formalism along with a complete set of proofs in the paper A Deterministic Method for Processing Data Sequences [3].

ℹ️ Info

A numerical verification of the equations above — Python prototypes operating on rational numbers (the Fraction library) — can be found on the Model Implementation page and in the repository github.com/michalwidera/equations.