Depth of sorting networks

23 fully proved

Levels

DefinitionComparator levels under earliest scheduling#✓fully proved

Given a list of comparators on \(\mathbb{N}\)-indexed wires, each a pair \((i, j)\) of wires, and a starting level \(\ell(x)\) for every wire \(x\), process the comparators in order, keeping a current level for each wire, initially \(\ell\): a comparator \((i, j)\) whose wires currently have levels \(a\) and \(b\) sets the current levels of both wires \(i\) and \(j\) to \(\max(a, b) + 1\) and leaves every other level unchanged. The result is the level of each wire after all the comparators, that is, when each comparator runs as early as possible, one level after the later of its two wires.

def levels : List (ℕ × ℕ) → (ℕ → ℕ) → ℕ → ℕ
  | [], lv => lv
  | c :: ps, lv => levels ps fun x =>
      if x = c.1 ∨ x = c.2 then max (lv c.1) (lv c.2) + 1 else lv x

Used by 20

Used byParallel composition of relabeled comparator lists · The final layer of the odd-even merger has depth at most one · Depth bound for Batcher's odd-even merger · Depth bound for Batcher's odd-even merge sort as a comparator list · Relabeling wires preserves a depth bound · Levels of a relabeled comparator list · Levels of a relabeled comparator list on the image wires · Relabeled comparator lists leave the other wires alone · Depth of sequential composition of comparator lists · Parallel composition of comparator lists on adjacent blocks · Influence sets grow at most exponentially with the level · Depth bound for a comparator list · The bitonic merger has depth at most \(k\) · Depth of the bitonic sorter's comparator list · The half-cleaner has depth at most \(1\) · Tabulated levels agree with levels · Sorting comparator lists on \(n\) wires have depth at least \(\log_2 n\) · Levels inside a block depend only on initial levels inside it · Comparators inside a block leave levels outside it unchanged · Swapping the wires of every comparator does not change levels

DefinitionDepth bound for a comparator list#✓fully proved

A list of comparators on wires indexed by \(\mathbb{N}\) has depth at most \(d\) when, starting with every wire at level \(0\) and scheduling each comparator one level after the later of its two wires, every wire ends at level at most \(d\).

def DepthLE (ps : List (ℕ × ℕ)) (d : ℕ) : Prop := ∀ x, levels ps (fun _ => 0) x ≤ d

Uses 1 · Used by 15

Statement usesComparator levels under earliest scheduling

Used byParallel composition of relabeled comparator lists · The final layer of the odd-even merger has depth at most one · Depth bound for Batcher's odd-even merger · Depth bound for Batcher's odd-even merge sort as a comparator list · Relabeling wires preserves a depth bound · Depth bound for Batcher's odd-even merge sorting network · Depth of sequential composition of comparator lists · Parallel composition of comparator lists on adjacent blocks · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · Depth bound for a comparator network · The bitonic merger has depth at most \(k\) · Depth of the bitonic sorter's comparator list · The half-cleaner has depth at most \(1\) · The bitonic sorting comparator list on \(2^k\) wires has depth at least \(k\) · Sorting comparator lists on \(n\) wires have depth at least \(\log_2 n\)

TheoremDepth of sequential composition of comparator lists#✓fully proved

If a list \(p\) of comparators on wires indexed by \(\mathbb{N}\) has depth at most \(d\) and a list \(q\) of comparators has depth at most \(e\), then the concatenation of \(p\) followed by \(q\) has depth at most \(d + e\).

theorem DepthLE.append {ps qs : List (ℕ × ℕ)} {d e : ℕ} (hp : DepthLE ps d) (hq : DepthLE qs e) :
    DepthLE (ps ++ qs) (d + e)

Uses 2 · Used by 4

Statement usesDepth bound for a comparator list

Proof usesComparator levels under earliest scheduling

Used byDepth bound for Batcher's odd-even merger · Depth bound for Batcher's odd-even merge sort as a comparator list · The bitonic merger has depth at most \(k\) · Depth of the bitonic sorter's comparator list

TheoremComparators inside a block leave levels outside it unchanged#✓fully proved

Let \(ps\) be a list of comparators all of whose wires lie in \([a, b)\). Then for all initial levels \(\ell : \mathbb{N} \to \mathbb{N}\) and every wire \(x\) with \(x < a\) or \(b \le x\), the level of \(x\) after \(ps\) starting from \(\ell\) is \(\ell(x)\).

theorem levels_of_not_mem : ∀ {ps : List (ℕ × ℕ)} {lo hi : ℕ}, Within ps lo hi →
    ∀ (lv : ℕ → ℕ) (x : ℕ), (x < lo ∨ hi ≤ x) → levels ps lv x = lv x

Uses 2 · Used by 1

Statement usesComparators within an interval · Comparator levels under earliest scheduling

Used byParallel composition of comparator lists on adjacent blocks

TheoremLevels inside a block depend only on initial levels inside it#✓fully proved

Let \(ps\) be a list of comparators all of whose wires lie in \([a, b)\), and let \(\ell, \ell' : \mathbb{N} \to \mathbb{N}\) be initial levels that agree on every wire in \([a, b)\). Then for every wire \(x\) in \([a, b)\), the level of \(x\) after \(ps\) starting from \(\ell\) equals the level of \(x\) after \(ps\) starting from \(\ell'\).

theorem levels_congr : ∀ {ps : List (ℕ × ℕ)} {lo hi : ℕ}, Within ps lo hi →
    ∀ (lv lv' : ℕ → ℕ), (∀ y, lo ≤ y → y < hi → lv y = lv' y) →
    ∀ x, lo ≤ x → x < hi → levels ps lv x = levels ps lv' x

Uses 2 · Used by 1

Statement usesComparators within an interval · Comparator levels under earliest scheduling

Used byParallel composition of comparator lists on adjacent blocks

TheoremParallel composition of comparator lists on adjacent blocks#✓fully proved

Let \(a\), \(m\), \(b\), \(d\) be natural numbers, and let \(p\) and \(q\) be lists of comparators on wires indexed by \(\mathbb{N}\), where every comparator of \(p\) joins two wires in \([a, m)\) and every comparator of \(q\) joins two wires in \([m, b)\). If \(p\) and \(q\) both have depth at most \(d\), then the concatenation of \(p\) followed by \(q\) also has depth at most \(d\): the two lists run in parallel.

theorem DepthLE.append_disjoint {ps qs : List (ℕ × ℕ)} {lo mid hi d : ℕ}
    (hpw : Within ps lo mid) (hqw : Within qs mid hi) (hp : DepthLE ps d) (hq : DepthLE qs d) :
    DepthLE (ps ++ qs) d

Uses 5 · Used by 3

Statement usesDepth bound for a comparator list · Comparators within an interval

Proof usesComparator levels under earliest scheduling · Levels inside a block depend only on initial levels inside it · Comparators inside a block leave levels outside it unchanged

Used byDepth bound for Batcher's odd-even merge sort as a comparator list · The bitonic merger has depth at most \(k\) · Depth of the bitonic sorter's comparator list

TheoremSwapping the wires of every comparator does not change levels#✓fully proved

For every list \(ps\) of comparators and all initial levels \(\ell : \mathbb{N} \to \mathbb{N}\), the levels after the list obtained from \(ps\) by replacing each comparator \((i, j)\) with \((j, i)\), starting from \(\ell\), equal the levels after \(ps\) starting from \(\ell\).

theorem levels_swap : ∀ (ps : List (ℕ × ℕ)) (lv : ℕ → ℕ),
    levels (ps.map Prod.swap) lv = levels ps lv

Uses 1 · Used by 1

Statement usesComparator levels under earliest scheduling

Used byDepth of the bitonic sorter's comparator list

Tabulated levels

DefinitionTabulated levels#✓fully proved

Given a list \(ps\) of comparators and a table \(t\) of natural numbers \(t_0, \dots, t_{N-1}\), the tabulated levels are computed by processing the comparators in order: a comparator \((i, j)\) sets both entries \(t_i\) and \(t_j\) to \(\max(t_i, t_j) + 1\), where an entry outside the table reads as \(0\) and a write outside the table is ignored.

Evaluating the levels directly re-reads both wires' earlier levels at every comparator, a cost exponential in the depth; this computes the same values in time proportional to the network size times \(N\).

def levelsTab : List (ℕ × ℕ) → List ℕ → List ℕ
  | [], t => t
  | c :: ps, t =>
      levelsTab ps ((t.set c.1 (max (t.getD c.1 0) (t.getD c.2 0) + 1)).set c.2
        (max (t.getD c.1 0) (t.getD c.2 0) + 1))

Used by 1

Used byTabulated levels agree with levels

TheoremTabulated levels agree with levels#✓fully proved

Let \(t\) be a list of natural numbers of length \(N\) and let \(ps\) be a list of comparators all of whose wires lie in \([0, N)\). Extend \(t\) to all wires by setting \(t_y = 0\) for \(y \ge N\). Then for every wire \(x\), the entry at position \(x\) of the tabulated levels of \(ps\) starting from the table \(t\) (read as \(0\) when \(x \ge N\)) equals the level of wire \(x\) after \(ps\), starting from the initial levels \(y \mapsto t_y\).

theorem getD_levelsTab : ∀ (ps : List (ℕ × ℕ)) (t : List ℕ), Within ps 0 t.length →
    ∀ x, (levelsTab ps t).getD x 0 = levels ps (fun y => t.getD y 0) x

Uses 3

Statement usesComparators within an interval · Comparator levels under earliest scheduling · Tabulated levels

The bitonic networks

TheoremThe half-cleaner has depth at most \(1\)#✓fully proved

For all natural numbers \(m\) and \(b\), the half-cleaner on the block of \(2m\) wires \(b, \dots, b + 2m - 1\) has depth at most \(1\): its comparators join pairwise disjoint pairs of wires.

theorem depthLE_halfCleaner (m b : ℕ) : DepthLE (halfCleaner m b) 1

Uses 3 · Used by 1

Statement usesDepth bound for a comparator list · Half-cleaner

Proof usesComparator levels under earliest scheduling

Used byThe bitonic merger has depth at most \(k\)

TheoremThe bitonic merger has depth at most \(k\)#✓fully proved

For all natural numbers \(k\) and \(b\), the bitonic merger on the block of \(2^k\) wires \(b, b + 1, \dots, b + 2^k - 1\) has depth at most \(k\).

theorem depthLE_bitonicMerge : ∀ k b, DepthLE (bitonicMerge k b) k

Uses 8 · Used by 1

Statement usesDepth bound for a comparator list · Bitonic merger

Proof usesDepth of sequential composition of comparator lists · Parallel composition of comparator lists on adjacent blocks · Comparators within an interval · The half-cleaner has depth at most \(1\) · Half-cleaner · Comparator levels under earliest scheduling

Used byDepth of the bitonic sorter's comparator list

TheoremDepth of the bitonic sorter's comparator list#✓fully proved

For all natural numbers \(k\) and \(b\), the comparator list of Batcher's bitonic sorter on the block of \(2^k\) wires \(b, b + 1, \dots, b + 2^k - 1\) has depth at most \(d\) for some natural number \(d\) with \(2d \le k(k+1)\); that is, its depth is at most \(k(k+1)/2\).

theorem depthLE_bitonicSortN : ∀ k b, ∃ d, DepthLE (bitonicSortN k b) d ∧ 2 * d ≤ k * (k + 1)

Uses 10 · Used by 1

Statement usesDepth bound for a comparator list · Batcher's bitonic sorter on a block of wires

Proof usesDepth of sequential composition of comparator lists · Parallel composition of comparator lists on adjacent blocks · Comparators within an interval · Bitonic merger · The bitonic merger has depth at most \(k\) · Half-cleaner · Comparator levels under earliest scheduling · Swapping the wires of every comparator does not change levels

Used byBatcher's bitonic sorting network has depth at most \(k(k+1)/2\)

Every sorting network on n wires has depth at least log₂ n

DefinitionInfluence sets of wires#✓fully proved

Given a list \(ps\) of comparators on wires indexed by \(\mathbb{N}\) and an assignment \(S\) of a finite set of natural numbers to each wire, the influence sets after \(ps\) are computed by processing the comparators in order: a comparator \((i, j)\) replaces the current sets of both wires \(i\) and \(j\) by their union, and leaves the sets of all other wires unchanged. Starting from \(S(x) = \{x\}\), the set of a wire tracks the inputs it can depend on.

Evaluating this definition directly re-reads both wires' earlier sets at every comparator, a cost exponential in the depth, so it serves as a proof device only.

def influence : List (ℕ × ℕ) → (ℕ → Finset ℕ) → ℕ → Finset ℕ
  | [], S => S
  | c :: ps, S => influence ps fun x => if x = c.1 ∨ x = c.2 then S c.1 ∪ S c.2 else S x

Used by 3

Used byInfluence sets grow at most exponentially with the level · Sorting comparator lists on \(n\) wires have depth at least \(\log_2 n\) · Outputs depend only on the influence set

TheoremInfluence sets grow at most exponentially with the level#✓fully proved

Let \(p\) be a list of comparators on wires indexed by \(\mathbb{N}\). Let \(S\) assign to each wire a finite set of natural numbers and let \(\ell\) assign to each wire a natural number, such that \(|S(x)| \le 2^{\ell(x)}\) for every wire \(x\). For each wire \(x\), let \(L(x)\) be the level of \(x\) after \(p\) starting from the levels \(\ell\). Then for every wire \(x\), the influence set of \(x\) after \(p\) starting from \(S\) has at most \(2^{L(x)}\) elements.

In particular, a wire at level \(l\) depends on at most \(2^l\) inputs.

theorem card_influence_le : ∀ (ps : List (ℕ × ℕ)) (S : ℕ → Finset ℕ) (lv : ℕ → ℕ),
    (∀ x, (S x).card ≤ 2 ^ lv x) → ∀ x, (influence ps S x).card ≤ 2 ^ levels ps lv x

Uses 2 · Used by 1

Statement usesInfluence sets of wires · Comparator levels under earliest scheduling

Used bySorting comparator lists on \(n\) wires have depth at least \(\log_2 n\)

TheoremOutputs depend only on the influence set#✓fully proved

Let \(f_0, g_0 : \mathbb{N} \to \alpha\) be two inputs with values in a linear order \(\alpha\), let \(S\) assign to each wire \(x\) a finite set \(S(x)\) of input positions, and let \(F, G : \mathbb{N} \to \alpha\) be wire values such that for every wire \(x\), if \(f_0\) and \(g_0\) agree on \(S(x)\), then \(F(x) = G(x)\). Then for every list of comparators and every wire \(x\), if \(f_0\) and \(g_0\) agree on the influence set of \(x\) obtained from \(S\) through the comparators, running the comparators on \(F\) and on \(G\) gives the same value at wire \(x\).

theorem runN_congr_influence {α : Type*} [LinearOrder α] (f₀ g₀ : ℕ → α) :
    ∀ (ps : List (ℕ × ℕ)) (S : ℕ → Finset ℕ) (F G : ℕ → α),
      (∀ x, (∀ y ∈ S x, f₀ y = g₀ y) → F x = G x) →
      ∀ x, (∀ y ∈ influence ps S x, f₀ y = g₀ y) → runN ps F x = runN ps G x

Uses 3 · Used by 1

Statement usesInfluence sets of wires · Running a comparator network on natural-number-indexed wires

Proof usesComparator on natural-number-indexed wires

Used bySorting comparator lists on \(n\) wires have depth at least \(\log_2 n\)

TheoremComparators inside \((0, n)\) keep a false value inside \((0, n)\)#✓fully proved

Let \(n\) be a natural number, let \(p\) be a list of comparators, each joining two wires in \([0, n)\), and let \(f\) assign a Boolean value to each wire in \(\mathbb{N}\). If \(f(y)\) is false for some \(y < n\), then after running \(p\) on \(f\) some wire \(y < n\) carries the value false.

The smaller value moves to the first wire of each comparator.

theorem exists_false_runN : ∀ {ps : List (ℕ × ℕ)} {n : ℕ}, Within ps 0 n →
    ∀ (f : ℕ → Bool), (∃ y < n, f y = false) → ∃ y < n, runN ps f y = false

Uses 3 · Used by 1

Statement usesComparators within an interval · Running a comparator network on natural-number-indexed wires

Proof usesComparator on natural-number-indexed wires

Used bySorting comparator lists on \(n\) wires have depth at least \(\log_2 n\)

TheoremSorting comparator lists on \(n\) wires have depth at least \(\log_2 n\)#✓fully proved

Let \(ps\) be a list of comparators on wires indexed by \(\mathbb{N}\), all of whose wires lie in \([0, n)\), and let \(d\) be a natural number. Suppose that for every Boolean input \(v\) on the wires \(0, \dots, n - 1\), extended by \(\mathrm{false}\) to the wires \(\ge n\), the output \(w\) of \(ps\) satisfies \(w_i \le w_j\) whenever \(i \le j < n\) (with \(\mathrm{false} < \mathrm{true}\)). If \(ps\) has depth at most \(d\), then \(n \le 2^d\).

The smallest output depends on every input, and a wire at level \(d\) depends on at most \(2^d\) inputs.

theorem le_two_pow_of_sorts {ps : List (ℕ × ℕ)} {n d : ℕ} (hw : Within ps 0 n)
    (hsort : ∀ (v : Fin n → Bool) (i j : ℕ), i ≤ j → j < n →
      runN ps (extendFalse v) i ≤ runN ps (extendFalse v) j)
    (hd : DepthLE ps d) : n ≤ 2 ^ d

Uses 10 · Used by 2

Statement usesDepth bound for a comparator list · Comparators within an interval · Extension of a Boolean vector by false · Running a comparator network on natural-number-indexed wires

Proof usesInfluence sets grow at most exponentially with the level · Comparators inside \((0, n)\) keep a false value inside \((0, n)\) · Influence sets of wires · Comparator levels under earliest scheduling · Outputs depend only on the influence set · Constant blocks stay constant

Used byThe bitonic sorting comparator list on \(2^k\) wires has depth at least \(k\) · Every sorting network on \(n\) wires has depth at least \(\log_2 n\)

TheoremThe bitonic sorting comparator list on \(2^k\) wires has depth at least \(k\)#✓fully proved

For all natural numbers \(k\) and \(d\), if the comparator list of Batcher's bitonic sorter on the wires \(0, \dots, 2^k - 1\) has depth at most \(d\), then \(k \le d\).

theorem le_of_depthLE_bitonicSortN {k d : ℕ} (hd : DepthLE (bitonicSortN k 0) d) : k ≤ d

Uses 9

Statement usesDepth bound for a comparator list · Batcher's bitonic sorter on a block of wires

Proof usesComparators within an interval · Bitonic merger · The bitonic sorter sorts every 0-1 input · Extension of a Boolean vector by false · Half-cleaner · Sorting comparator lists on \(n\) wires have depth at least \(\log_2 n\) · Running a comparator network on natural-number-indexed wires

Depth of Networks

DefinitionComparator list of a network#✓fully proved

The comparators of a network on \(n\) wires, in order, with each comparator \((i, j)\) written as the pair of natural numbers \((i, j)\), forgetting that \(i, j < n\).

def Network.toPairs (net : Network n) : List (ℕ × ℕ) := net.map fun c => (c.1.val, c.2.val)

Uses 1 · Used by 4

Statement usesComparator network

Used byDepth bound for Batcher's odd-even merge sorting network · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · Depth bound for a comparator network · Every sorting network on \(n\) wires has depth at least \(\log_2 n\)

DefinitionDepth bound for a comparator network#✓fully proved

A comparator network on \(n\) wires has depth at most \(d\) when its list of comparators, read as pairs of wire numbers in \(\mathbb{N}\), has depth at most \(d\): starting with every wire at level \(0\) and scheduling each comparator one level after the later of its two wires, every wire ends at level at most \(d\).

def Network.DepthLE (net : Network n) (d : ℕ) : Prop := Bitonic.DepthLE (Network.toPairs net) d

Uses 3 · Used by 5

Statement usesDepth bound for a comparator list · Comparator network · Comparator list of a network

Used byLower bound for the depth of Batcher's odd-even merge sorting network · Depth bound for Batcher's odd-even merge sorting network · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · Batcher's bitonic sorter on \(2^k\) wires has depth at least \(k\) · Every sorting network on \(n\) wires has depth at least \(\log_2 n\)

TheoremEvery sorting network on \(n\) wires has depth at least \(\log_2 n\)#✓fully proved

Let \(C\) be a comparator network on \(n\) wires and \(d\) a natural number. If \(C\) sorts every Boolean input (its output is monotone in the wire order for every input in \(\{\mathrm{false}, \mathrm{true}\}^n\), with \(\mathrm{false} < \mathrm{true}\)) and \(C\) has depth at most \(d\), then \(n \le 2^d\).

By the 0-1 principle, the hypothesis implies that \(C\) sorts every input over every linear order.

theorem Network.le_two_pow_of_sorts {net : Network n} {d : ℕ} (hs : Sorts net Bool)
    (hd : Network.DepthLE net d) : n ≤ 2 ^ d

Uses 11 · Used by 2

Statement usesComparator network · Depth bound for a comparator network · Networks that sort

Proof usesComparators within an interval · Transported comparator lists agree with the original on Boolean inputs · Extension of a Boolean vector by false · Sorting comparator lists on \(n\) wires have depth at least \(\log_2 n\) · Restricting comparators to finitely many wires · Running a comparator network on natural-number-indexed wires · Comparator list of a network · Running a comparator network

Used byLower bound for the depth of Batcher's odd-even merge sorting network · Batcher's bitonic sorter on \(2^k\) wires has depth at least \(k\)

TheoremBatcher's bitonic sorting network has depth at most \(k(k+1)/2\)#✓fully proved

For every natural number \(k\), Batcher's bitonic sorting network on \(2^k\) wires has depth at most \(d\) for some natural number \(d\) with \(2d \le k(k+1)\); that is, its depth is at most \(k(k+1)/2\).

theorem bitonicSorter_depthLE (k : ℕ) :
    ∃ d, Network.DepthLE (bitonicSorter k) d ∧ 2 * d ≤ k * (k + 1)

Uses 11

Statement usesBatcher's bitonic sorting network · Depth bound for a comparator network

Proof usesDepth bound for a comparator list · Comparators within an interval · Bitonic merger · Batcher's bitonic sorter on a block of wires · Depth of the bitonic sorter's comparator list · Half-cleaner · Restricting comparators to finitely many wires · Comparator network · Comparator list of a network

TheoremBatcher's bitonic sorter on \(2^k\) wires has depth at least \(k\)#✓fully proved

For all natural numbers \(k\) and \(d\), if Batcher's bitonic sorting network on \(2^k\) wires has depth at most \(d\), then \(k \le d\).

theorem le_of_bitonicSorter_depthLE {k d : ℕ} (hd : Network.DepthLE (bitonicSorter k) d) :
    k ≤ d

Uses 4

Statement usesBatcher's bitonic sorting network · Depth bound for a comparator network

Proof usesBatcher's bitonic sorter sorts every input over every linear order · Every sorting network on \(n\) wires has depth at least \(\log_2 n\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.