Bitonic sorter

25 fully proved

Comparators on ℕ-indexed wires

DefinitionComparator on natural-number-indexed wires#✓fully proved

Let \(\alpha\) be a linear order. For wires \(i, j \in \mathbb{N}\) and an assignment \(f\) of values in \(\alpha\) to the wires \(x \in \mathbb{N}\), the comparator \((i, j)\) applied to \(f\) puts \(\min(f(i), f(j))\) on wire \(i\), puts \(\max(f(i), f(j))\) on wire \(j\) when \(j \ne i\), and leaves every other wire unchanged.

def cmp (i j : ℕ) (f : ℕ → α) : ℕ → α :=
  fun x => if x = i then min (f i) (f j) else if x = j then max (f i) (f j) else f x

Used by 15

Used byThe odd-even merger merges · Odd-even merge sort sorts every \(0\)-\(1\) input · Output of the last layer of the odd-even merger · Running a relabeled network · Relabeled networks fix the wires outside the image · The bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input · Transported comparator lists agree with the original on Boolean inputs · Running a comparator network on natural-number-indexed wires · Constant blocks stay constant · Output of the half-cleaner · Locality of comparator networks · Reversing the comparators conjugates the network by complement on Booleans · Comparators inside \((0, n)\) keep a false value inside \((0, n)\) · Outputs depend only on the influence set

DefinitionRunning a comparator network on natural-number-indexed wires#✓fully proved

Let \(\alpha\) be a linear order. Given a list \(ps\) of comparators, each a pair \((i, j)\) of natural numbers, and an input \(f : \mathbb{N} \to \alpha\) giving the value on each wire, running \(ps\) on \(f\) applies the comparators of \(ps\) to the wire values one after another, from first to last. The comparator \((i, j)\) puts the minimum of the values on wires \(i\) and \(j\) on wire \(i\) and their maximum on wire \(j\), and leaves the other wires unchanged.

def runN (ps : List (ℕ × ℕ)) (f : ℕ → α) : ℕ → α :=
  ps.foldl (fun g c => cmp c.1 c.2 g) f

Uses 1 · Used by 19

Statement usesComparator on natural-number-indexed wires

Used byThe odd-even merger merges · Odd-even merge sort sorts every \(0\)-\(1\) input · Batcher's odd-even merge sort sorts every input over every linear order · Output of the last layer of the odd-even merger · Running a relabeled network · Relabeled networks fix the wires outside the image · The bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input · Batcher's bitonic sorter sorts every input over every linear order · Transported comparator lists agree with the original on Boolean inputs · Constant blocks stay constant · Output of the half-cleaner · Locality of comparator networks · Reversing the comparators conjugates the network by complement on Booleans · Comparators inside \((0, n)\) keep a false value inside \((0, n)\) · 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\) · Every sorting network on \(n\) wires has depth at least \(\log_2 n\) · Outputs depend only on the influence set

DefinitionComparators within an interval#✓fully proved

A list \(ps\) of comparators, each a pair \((i, j)\) of natural numbers, lies within \([l, h)\) if every comparator \((i, j)\) in \(ps\) satisfies \(l \le i < h\) and \(l \le j < h\).

def Within (ps : List (ℕ × ℕ)) (lo hi : ℕ) : Prop :=
  ∀ p ∈ ps, lo ≤ p.1 ∧ p.1 < hi ∧ lo ≤ p.2 ∧ p.2 < hi

Used by 22

Used byDepth bound for Batcher's odd-even merge sort as a comparator list · Depth bound for Batcher's odd-even merge sorting network · Batcher's odd-even merge sort sorts every input over every linear order · Relabeling keeps comparators within an interval · The bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input · Batcher's bitonic sorter sorts every input over every linear order · Transported comparator lists agree with the original on Boolean inputs · Comparator count of Batcher's bitonic sorter · Constant blocks stay constant · Locality of comparator networks · Parallel composition of comparator lists on adjacent blocks · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · The bitonic merger has depth at most \(k\) · Depth of the bitonic sorter's comparator list · Comparators inside \((0, n)\) keep a false value inside \((0, n)\) · Tabulated levels agree with levels · 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\) · Every sorting network on \(n\) wires has 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

TheoremLocality of comparator networks#✓fully proved

Let \(\alpha\) be a linear order and let \(ps\) be a list of comparators \((i, j)\) on \(\mathbb{N}\)-indexed wires that all lie within \([l, h)\), that is, \(l \le i < h\) and \(l \le j < h\) for every \((i, j)\) in \(ps\). Then for every input \(f : \mathbb{N} \to \alpha\) and every wire \(x\) with \(x < l\) or \(h \le x\), the value of wire \(x\) after running \(ps\) on \(f\) is \(f(x)\).

theorem runN_of_not_mem : ∀ {ps : List (ℕ × ℕ)} {lo hi : ℕ}, Within ps lo hi →
    ∀ (f : ℕ → α) (x : ℕ), (x < lo ∨ hi ≤ x) → runN ps f x = f x

Uses 3 · Used by 2

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

Proof usesComparator on natural-number-indexed wires

Used byThe bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input

TheoremConstant blocks stay constant#✓fully proved

Let \(\alpha\) be a linear order, let \(l, h \in \mathbb{N}\), and let \(c\) be a list of comparators on \(\mathbb{N}\)-indexed wires each of which joins two wires \(x\) with \(l \le x < h\). If an input \(f : \mathbb{N} \to \alpha\) takes the same value \(a\) on every wire \(x\) with \(l \le x < h\), then running \(c\) on \(f\) gives an output that also takes the value \(a\) on every such wire.

theorem runN_const : ∀ {ps : List (ℕ × ℕ)} {lo hi : ℕ}, Within ps lo hi →
    ∀ (f : ℕ → α) (a : α), (∀ x, lo ≤ x → x < hi → f x = a) →
    ∀ x, lo ≤ x → x < hi → runN ps f x = a

Uses 3 · Used by 2

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

Proof usesComparator on natural-number-indexed wires

Used byThe bitonic merger sorts every bitonic 0-1 input · Sorting comparator lists on \(n\) wires have depth at least \(\log_2 n\)

The half-cleaner

DefinitionHalf-cleaner#✓fully proved

For natural numbers \(m\) and \(b\), the half-cleaner on the block of wires \([b, b + 2m)\) is the list of comparators \((b + i, b + m + i)\) for \(i = 0, 1, \dots, m - 1\), in this order: it compares wire \(b + i\) with wire \(b + m + i\).

def halfCleaner (m b : ℕ) : List (ℕ × ℕ) := (List.range m).map fun i => (b + i, b + m + i)

Used by 13

Used byBitonic merger · The bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input · Batcher's bitonic sorter sorts every input over every linear order · Size of the bitonic merger · Comparator count of Batcher's bitonic sorter · Size of the half-cleaner · Output of the half-cleaner · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · 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\)

TheoremOutput of the half-cleaner#✓fully proved

Let \(\alpha\) be a linear order, let \(m, b \in \mathbb{N}\), and let \(f : \mathbb{N} \to \alpha\) be an input on \(\mathbb{N}\)-indexed wires. Running the half-cleaner on \([b, b + 2m)\) on \(f\) puts \(\min(f(b + i), f(b + m + i))\) on wire \(b + i\) and \(\max(f(b + i), f(b + m + i))\) on wire \(b + m + i\) for every \(i < m\), and leaves the value \(f(x)\) on every wire \(x\) outside \([b, b + 2m)\) unchanged.

theorem runN_halfCleaner (m b : ℕ) (f : ℕ → α) (x : ℕ) :
    runN (halfCleaner m b) f x =
      if b ≤ x ∧ x < b + m then min (f x) (f (x + m))
      else if b + m ≤ x ∧ x < b + m + m then max (f (x - m)) (f x) else f x

Uses 3 · Used by 1

Statement usesHalf-cleaner · Running a comparator network on natural-number-indexed wires

Proof usesComparator on natural-number-indexed wires

Used byThe bitonic merger sorts every bitonic 0-1 input

Bitonic 0-1 sequences

DefinitionInterval indicators#✓fully proved

A sequence \(s : \mathbb{N} \to \{0, 1\}\) is an interval indicator of length \(L\) if there are natural numbers \(a \le e \le L\) such that for every \(i < L\), \(s(i) = 1\) exactly when \(a \le i < e\).

def IsInterval (s : ℕ → Bool) (L : ℕ) : Prop :=
  ∃ a e, a ≤ e ∧ e ≤ L ∧ ∀ i < L, s i = decide (a ≤ i ∧ i < e)

Used by 4

Used byThe bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input · The half-cleaner lemma · Bitonic 0-1 sequences

DefinitionBitonic 0-1 sequences#✓fully proved

A sequence \(s : \mathbb{N} \to \{0, 1\}\) is bitonic of length \(L\) if either \(s\) or its complement \(1 - s\) is an interval indicator of length \(L\); that is, on the positions \(0, \dots, L - 1\) it has the form \(0^a 1^b 0^c\) or \(1^a 0^b 1^c\). Values of \(s\) at positions \(i \ge L\) are unconstrained.

def IsBitonic (s : ℕ → Bool) (L : ℕ) : Prop :=
  IsInterval s L ∨ IsInterval (fun i => !s i) L

Uses 1 · Used by 3

Statement usesInterval indicators

Used byThe bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input · The half-cleaner lemma

TheoremThe half-cleaner lemma#✓fully proved

Let \(m \in \mathbb{N}\) and let \(s_0, s_1, \dots, s_{2m-1}\) be a bitonic sequence of Booleans, ordered by \(\mathrm{false} < \mathrm{true}\). For \(i < m\) put \(\ell_i = \min(s_i, s_{i+m})\) and \(u_i = \max(s_i, s_{i+m})\). Then either \(\ell_i = \mathrm{false}\) for every \(i < m\) and \(u_0, \dots, u_{m-1}\) is bitonic, or \(u_i = \mathrm{true}\) for every \(i < m\) and \(\ell_0, \dots, \ell_{m-1}\) is bitonic.

The \(\ell_i\) and \(u_i\) are the outputs of the half-cleaner on \(2m\) wires. This is CLRS Lemma 27.3 for bitonic \(0\)-\(1\) sequences.

theorem halfClean_bitonic {s : ℕ → Bool} {m : ℕ} (h : IsBitonic s (2 * m)) :
    ((∀ i < m, (s i && s (i + m)) = false) ∧ IsBitonic (fun i => s i || s (i + m)) m) ∨
    ((∀ i < m, (s i || s (i + m)) = true) ∧ IsBitonic (fun i => s i && s (i + m)) m)

Uses 2 · Used by 1

Statement usesBitonic 0-1 sequences

Proof usesInterval indicators

Used byThe bitonic merger sorts every bitonic 0-1 input

The bitonic merger

DefinitionSorted on a block#✓fully proved

A Boolean sequence \(g : \mathbb{N} \to \mathrm{Bool}\) is sorted on the block \([b, b + L)\) if \(g(b + i) \le g(b + j)\) for all \(i \le j < L\), where Booleans are ordered by \(\mathrm{false} < \mathrm{true}\).

def SortedOn (g : ℕ → Bool) (b L : ℕ) : Prop := ∀ i j, i ≤ j → j < L → g (b + i) ≤ g (b + j)

Used by 2

Used byThe bitonic merger sorts every bitonic 0-1 input · The bitonic sorter sorts every 0-1 input

DefinitionBitonic merger#✓fully proved

The bitonic merger on the block of wires \([b, b + 2^k)\) is the list of comparators defined by recursion on \(k\). For \(k = 0\) it is empty. On the block \([b, b + 2^{k+1})\) it is the half-cleaner on \([b, b + 2^{k+1})\), followed by the bitonic merger on \([b, b + 2^k)\), followed by the bitonic merger on \([b + 2^k, b + 2^{k+1})\).

This is CLRS's BITONIC-SORTER.

def bitonicMerge : ℕ → ℕ → List (ℕ × ℕ)
  | 0, _ => []
  | k + 1, b => halfCleaner (2 ^ k) b ++ bitonicMerge k b ++ bitonicMerge k (b + 2 ^ k)

Uses 1 · Used by 11

Statement usesHalf-cleaner

Used byThe bitonic merger sorts every bitonic 0-1 input · Batcher's bitonic sorter on a block of wires · The bitonic sorter sorts every 0-1 input · Batcher's bitonic sorter sorts every input over every linear order · Size of the bitonic merger · Size of the bitonic sorter on a block of wires · Comparator count of Batcher's bitonic sorter · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · The bitonic merger has depth at most \(k\) · Depth of the bitonic sorter's comparator list · The bitonic sorting comparator list on \(2^k\) wires has depth at least \(k\)

TheoremThe bitonic merger sorts every bitonic 0-1 input#✓fully proved

Let \(k, b \in \mathbb{N}\) and let \(f\) assign a Boolean value to each wire \(x \in \mathbb{N}\), with Booleans ordered by \(\mathrm{false} < \mathrm{true}\). If the sequence \(f(b), f(b + 1), \dots, f(b + 2^k - 1)\) is bitonic, then running the bitonic merger on the block \([b, b + 2^k)\) on \(f\) gives an assignment \(g\) that is sorted on that block: \(g(b + i) \le g(b + j)\) whenever \(i \le j < 2^k\).

This is the correctness of CLRS's BITONIC-SORTER, proved by recursion on the half-cleaner lemma.

theorem bitonicMerge_sorts : ∀ (k b : ℕ) (f : ℕ → Bool), IsBitonic (fun i => f (b + i)) (2 ^ k) →
    SortedOn (runN (bitonicMerge k b) f) b (2 ^ k)

Uses 12 · Used by 1

Statement usesBitonic 0-1 sequences · Sorted on a block · Bitonic merger · Running a comparator network on natural-number-indexed wires

Proof usesInterval indicators · Comparators within an interval · Comparator on natural-number-indexed wires · The half-cleaner lemma · Half-cleaner · Constant blocks stay constant · Output of the half-cleaner · Locality of comparator networks

Used byThe bitonic sorter sorts every 0-1 input

The bitonic sorter

TheoremReversing the comparators conjugates the network by complement on Booleans#✓fully proved

Let \(ps\) be a list of comparators on \(\mathbb{N}\)-indexed wires and let \(ps'\) be obtained by replacing each comparator \((i, j)\) in \(ps\) by \((j, i)\). For every input \(f : \mathbb{N} \to \mathrm{Bool}\) and every wire \(x\), the value of wire \(x\) after running \(ps'\) on \(f\) is the negation of the value of wire \(x\) after running \(ps\) on the complemented input \(y \mapsto \lnot f(y)\).

theorem runN_swap : ∀ (ps : List (ℕ × ℕ)) (f : ℕ → Bool) (x : ℕ),
    runN (ps.map Prod.swap) f x = !runN ps (fun y => !f y) x

Uses 2 · Used by 1

Statement usesRunning a comparator network on natural-number-indexed wires

Proof usesComparator on natural-number-indexed wires

Used byThe bitonic sorter sorts every 0-1 input

DefinitionBatcher's bitonic sorter on a block of wires#✓fully proved

A comparator \((i, j)\) puts the minimum of the values on wires \(i\) and \(j\) on wire \(i\) and the maximum on wire \(j\). Batcher's bitonic sorter on the block of wires \([b, b + 2^k)\) is the list of comparators defined by recursion on \(k\). For \(k = 0\) it is empty. On the block \([b, b + 2^{k+1})\) it is Batcher's bitonic sorter on \([b, b + 2^k)\), followed by Batcher's bitonic sorter on \([b + 2^k, b + 2^{k+1})\) with every comparator \((i, j)\) replaced by \((j, i)\), followed by the bitonic merger on \([b, b + 2^{k+1})\).

Reversing the comparators makes the second half sort downwards, so the merger receives a bitonic sequence. (CLRS's SORTER instead sorts both halves up and uses MERGER.)

def bitonicSortN : ℕ → ℕ → List (ℕ × ℕ)
  | 0, _ => []
  | k + 1, b => bitonicSortN k b ++ (bitonicSortN k (b + 2 ^ k)).map Prod.swap ++
      bitonicMerge (k + 1) b

Uses 1 · Used by 8

Statement usesBitonic merger

Used byThe bitonic sorter sorts every 0-1 input · Batcher's bitonic sorting network · Batcher's bitonic sorter sorts every input over every linear order · Size of the bitonic sorter on a block of wires · Comparator count of Batcher's bitonic sorter · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · Depth of the bitonic sorter's comparator list · The bitonic sorting comparator list on \(2^k\) wires has depth at least \(k\)

TheoremThe bitonic sorter sorts every 0-1 input#✓fully proved

Let \(k, b \in \mathbb{N}\) and let \(f\) assign a Boolean value to each wire \(x \in \mathbb{N}\), with Booleans ordered by \(\mathrm{false} < \mathrm{true}\). Running Batcher's bitonic sorter on the block \([b, b + 2^k)\) on \(f\) gives an assignment \(g\) that is sorted on that block: \(g(b + i) \le g(b + j)\) whenever \(i \le j < 2^k\).

theorem bitonicSortN_sorts : ∀ (k b : ℕ) (f : ℕ → Bool),
    SortedOn (runN (bitonicSortN k b) f) b (2 ^ k)

Uses 12 · Used by 2

Statement usesSorted on a block · Batcher's bitonic sorter on a block of wires · Running a comparator network on natural-number-indexed wires

Proof usesBitonic 0-1 sequences · Interval indicators · Comparators within an interval · Bitonic merger · The bitonic merger sorts every bitonic 0-1 input · Comparator on natural-number-indexed wires · Half-cleaner · Locality of comparator networks · Reversing the comparators conjugates the network by complement on Booleans

Used byBatcher's bitonic sorter sorts every input over every linear order · The bitonic sorting comparator list on \(2^k\) wires has depth at least \(k\)

Sizes

TheoremSize of the half-cleaner#✓fully proved

For all natural numbers \(m\) and \(b\), the half-cleaner on the block of wires \([b, b + 2m)\) has exactly \(m\) comparators.

theorem length_halfCleaner (m b : ℕ) : (halfCleaner m b).length = m

Uses 1 · Used by 1

Statement usesHalf-cleaner

Used bySize of the bitonic merger

TheoremSize of the bitonic merger#✓fully proved

For all natural numbers \(k\) and \(b\), the bitonic merger on the block of wires \([b, b + 2^k)\) has \(k \cdot 2^{k-1}\) comparators; precisely, twice its number of comparators equals \(k \cdot 2^k\).

theorem length_bitonicMerge : ∀ k b, 2 * (bitonicMerge k b).length = k * 2 ^ k

Uses 3 · Used by 1

Statement usesBitonic merger

Proof usesHalf-cleaner · Size of the half-cleaner

Used bySize of the bitonic sorter on a block of wires

TheoremSize of the bitonic sorter on a block of wires#✓fully proved

For all natural numbers \(k\) and \(b\), the bitonic sorter on the block of \(\mathbb{N}\)-indexed wires \([b, b + 2^k)\) has \(k(k+1)2^k/4\) comparators; precisely, four times its number of comparators equals \(k(k+1)2^k\).

theorem length_bitonicSortN : ∀ k b, 4 * (bitonicSortN k b).length = k * (k + 1) * 2 ^ k

Uses 3 · Used by 1

Statement usesBatcher's bitonic sorter on a block of wires

Proof usesBitonic merger · Size of the bitonic merger

Used byComparator count of Batcher's bitonic sorter

The network on 2 ^ k wires

DefinitionRestricting comparators to finitely many wires#✓fully proved

For a natural number \(N\) and a list of comparators on wires indexed by \(\mathbb{N}\), this is the network on the \(N\) wires \(0, \dots, N - 1\) that keeps, in their original order, the comparators \((i, j)\) with \(i < N\) and \(j < N\), and drops all the others.

def ofPairs (N : ℕ) (ps : List (ℕ × ℕ)) : Network N :=
  ps.filterMap fun p => if h : p.1 < N ∧ p.2 < N then some (⟨p.1, h.1⟩, ⟨p.2, h.2⟩) else none

Uses 1 · Used by 9

Statement usesComparator network

Used byBatcher's odd-even merge sorting network · Depth bound for Batcher's odd-even merge sorting network · Batcher's odd-even merge sort sorts every input over every linear order · Batcher's bitonic sorting network · Batcher's bitonic sorter sorts every input over every linear order · Transported comparator lists agree with the original on Boolean inputs · Comparator count of Batcher's bitonic sorter · Batcher's bitonic sorting network has depth at most \(k(k+1)/2\) · Every sorting network on \(n\) wires has depth at least \(\log_2 n\)

DefinitionExtension of a Boolean vector by false#✓fully proved

For \(N \in \mathbb{N}\) and a Boolean vector \(v = (v_0, \dots, v_{N-1})\), its extension by \(\mathrm{false}\) is the function on \(\mathbb{N}\) that takes the value \(v_j\) at each \(j < N\) and the value \(\mathrm{false}\) at each \(j \ge N\).

def extendFalse {N : ℕ} (v : Fin N → Bool) : ℕ → Bool :=
  fun j => if h : j < N then v ⟨j, h⟩ else false

Used by 6

Used byBatcher's odd-even merge sort sorts every input over every linear order · Batcher's bitonic sorter sorts every input over every linear order · Transported comparator lists agree with the original on Boolean inputs · 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\) · Every sorting network on \(n\) wires has depth at least \(\log_2 n\)

TheoremTransported comparator lists agree with the original on Boolean inputs#✓fully proved

Let \(N \in \mathbb{N}\) and let \(P\) be a list of comparators on natural-number-indexed wires, each of which joins two wires below \(N\). For every Boolean input \(v\) on the wires \(0, \dots, N - 1\), run the network on \(N\) wires obtained from \(P\) on \(v\) and extend its output by \(\mathrm{false}\) to all wires in \(\mathbb{N}\); the result equals the result of running \(P\) on the extension of \(v\) by \(\mathrm{false}\).

theorem ext_run_ofPairs {N : ℕ} : ∀ (ps : List (ℕ × ℕ)), Within ps 0 N →
    ∀ v : Fin N → Bool, extendFalse (run (ofPairs N ps) v) = runN ps (extendFalse v)

Uses 8 · Used by 3

Statement usesComparators within an interval · Extension of a Boolean vector by false · Restricting comparators to finitely many wires · Running a comparator network on natural-number-indexed wires · Running a comparator network

Proof usesComparator on natural-number-indexed wires · Comparator network · Comparator

Used byBatcher's odd-even merge sort sorts every input over every linear order · Batcher's bitonic sorter sorts every input over every linear order · Every sorting network on \(n\) wires has depth at least \(\log_2 n\)

DefinitionBatcher's bitonic sorting network#✓fully proved

For \(k \in \mathbb{N}\), Batcher's bitonic sorting network on \(2^k\) wires is the comparator network on the wires \(0, 1, \dots, 2^k - 1\) made of the comparators of Batcher's bitonic sorter on the block \([0, 2^k)\) that join two wires below \(2^k\) (in fact all of them), applied in the same order.

def bitonicSorter (k : ℕ) : Network (2 ^ k) := ofPairs (2 ^ k) (bitonicSortN k 0)

Uses 3 · Used by 4

Statement usesBatcher's bitonic sorter on a block of wires · Restricting comparators to finitely many wires · Comparator network

Used byBatcher's bitonic sorter sorts every input over every linear order · Comparator count of Batcher's bitonic sorter · 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\)

TheoremBatcher's bitonic sorter sorts every input over every linear order#✓fully proved

For every \(k \in \mathbb{N}\) and every linearly ordered type \(\alpha\), Batcher's bitonic sorting network on \(2^k\) wires sorts inputs over \(\alpha\): for every assignment \(v\) of elements of \(\alpha\) to the wires \(0, 1, \dots, 2^k - 1\), the output of the network on \(v\) is monotone in the wire order.

The proof goes through the 0-1 principle.

theorem bitonicSorter_sorts (k : ℕ) (α : Type*) [LinearOrder α] : Sorts (bitonicSorter k) α

Uses 13 · Used by 1

Statement usesBatcher's bitonic sorting network · Networks that sort

Proof usesComparators within an interval · Bitonic merger · Batcher's bitonic sorter on a block of wires · The bitonic sorter sorts every 0-1 input · Transported comparator lists agree with the original on Boolean inputs · Extension of a Boolean vector by false · Half-cleaner · Restricting comparators to finitely many wires · Running a comparator network on natural-number-indexed wires · Running a comparator network · The 0-1 principle

Used byBatcher's bitonic sorter on \(2^k\) wires has depth at least \(k\)

TheoremComparator count of Batcher's bitonic sorter#✓fully proved

For every natural number \(k\), Batcher's bitonic sorting network on \(2^k\) wires has \(k(k+1)2^k/4\) comparators; precisely, four times its number of comparators equals \(k(k+1)2^k\).

theorem length_bitonicSorter (k : ℕ) : 4 * (bitonicSorter k).length = k * (k + 1) * 2 ^ k

Uses 8

Statement usesBatcher's bitonic sorting network

Proof usesComparators within an interval · Bitonic merger · Batcher's bitonic sorter on a block of wires · Half-cleaner · Size of the bitonic sorter on a block of wires · Restricting comparators to finitely many wires · Comparator network

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.