Batcher odd–even mergesort

DefinitionRelabeling the wires of a comparator list#✓fully proved

Given a map \(e : \mathbb{N} \to \mathbb{N}\) and a list of comparators, each a pair \((i, j)\) of wires in \(\mathbb{N}\), the relabeled list replaces every comparator \((i, j)\) by \((e(i), e(j))\) and keeps the order of the list.

def relabel (e : ℕ → ℕ) (ps : List (ℕ × ℕ)) : List (ℕ × ℕ) := ps.map fun q => (e q.1, e q.2)

Used by 18

Used byParallel composition of relabeled comparator lists · 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 · Size of the odd-even merger · Size of Batcher's odd-even merge sort · Levels of a relabeled comparator list · Levels of a relabeled comparator list on the image wires · Relabeled comparator lists leave the other wires alone · Batcher's odd-even merger · The odd-even merger merges · Batcher's odd-even merge sort · Odd-even merge sort sorts every \(0\)-\(1\) input · 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 · Running a relabeled network · Relabeled networks fix the wires outside the image

TheoremRunning a relabeled network#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(e : \mathbb{N} \to \mathbb{N}\) be injective. For every list of comparators, every \(f : \mathbb{N} \to \alpha\) and every wire \(j\), running the list relabeled by \(e\) on \(f\) gives at wire \(e(j)\) the same value as running the original list on the input \(i \mapsto f(e(i))\) gives at wire \(j\).

theorem runN_relabel {α : Type*} [LinearOrder α] {e : ℕ → ℕ} (he : Function.Injective e) :
    ∀ (ps : List (ℕ × ℕ)) (f : ℕ → α) (j : ℕ),
      runN (relabel e ps) f (e j) = runN ps (fun i => f (e i)) j

Uses 3 · Used by 2

Statement usesRunning a comparator network on natural-number-indexed wires · Relabeling the wires of a comparator list

Proof usesComparator on natural-number-indexed wires

Used byThe odd-even merger merges · Odd-even merge sort sorts every \(0\)-\(1\) input

TheoremRelabeled networks fix the wires outside the image#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(e : \mathbb{N} \to \mathbb{N}\) any map and \(f : \mathbb{N} \to \alpha\) an assignment of values to the wires. For every list of comparators and every wire \(x\) that is not of the form \(e(y)\), running the list relabeled by \(e\) on \(f\) gives the value \(f(x)\) at wire \(x\).

theorem runN_relabel_of_not_mem {α : Type*} [LinearOrder α] {e : ℕ → ℕ} :
    ∀ (ps : List (ℕ × ℕ)) (f : ℕ → α) (x : ℕ), (∀ y, x ≠ e y) → runN (relabel e ps) f x = f x

Uses 3 · Used by 2

Statement usesRunning a comparator network on natural-number-indexed wires · Relabeling the wires of a comparator list

Proof usesComparator on natural-number-indexed wires

Used byThe odd-even merger merges · Odd-even merge sort sorts every \(0\)-\(1\) input

DefinitionLast layer of the odd-even merger#✓fully proved

For \(k \in \mathbb{N}\), this is the list of comparators \((2i + 1, 2i + 2)\) for \(i = 0, 1, \dots, 2^{k+1} - 2\), in increasing order of \(i\). It compares the neighbouring wires \(2i + 1\) and \(2i + 2\) and is the last layer of the odd-even merger on \(2^{k+2}\) wires.

def finalLayer (k : ℕ) : List (ℕ × ℕ) :=
  (List.range (2 ^ (k + 1) - 1)).map fun i => (2 * i + 1, 2 * i + 2)

Used by 9

Used byThe 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 · Size of the odd-even merger · Batcher's odd-even merger · The odd-even merger merges · Depth bound for Batcher's odd-even merge sorting network · Batcher's odd-even merge sort sorts every input over every linear order · Output of the last layer of the odd-even merger

DefinitionBatcher's odd-even merger#✓fully proved

For \(k \in \mathbb{N}\), the odd-even merger on wires \(0, \dots, 2^{k+1} - 1\) is the comparator list defined by recursion on \(k\). For \(k = 0\) it is the single comparator \((0, 1)\). For \(k + 1\) it is the merger for \(k\) with each wire \(i\) renamed to \(2i\) (merging the even wires), followed by the merger for \(k\) with each wire \(i\) renamed to \(2i + 1\) (merging the odd wires), followed by the comparators \((2i + 1, 2i + 2)\) for \(i = 0, 1, \dots, 2^{k+1} - 2\) in increasing order of \(i\).

def oddEvenMerge : ℕ → List (ℕ × ℕ)
  | 0 => [(0, 1)]
  | k + 1 => relabel (fun i => 2 * i) (oddEvenMerge k) ++
      relabel (fun i => 2 * i + 1) (oddEvenMerge k) ++ finalLayer k

Uses 2 · Used by 9

Statement usesLast layer of the odd-even merger · Relabeling the wires of a comparator list

Used byDepth bound for Batcher's odd-even merger · Depth bound for Batcher's odd-even merge sort as a comparator list · Size of the odd-even merger · Size of Batcher's odd-even merge sort · The odd-even merger merges · Batcher's odd-even merge sort · Odd-even merge sort sorts every \(0\)-\(1\) input · Depth bound for Batcher's odd-even merge sorting network · Batcher's odd-even merge sort sorts every input over every linear order

DefinitionBatcher's odd-even merge sort#✓fully proved

For \(k \in \mathbb{N}\), odd-even merge sort on wires \(0, \dots, 2^k - 1\) is the comparator list defined by recursion on \(k\). For \(k = 0\) it is empty. For \(k + 1\) it is the sorter for \(k\) (sorting wires \(0, \dots, 2^k - 1\)), followed by the sorter for \(k\) with each wire \(i\) renamed to \(2^k + i\) (sorting wires \(2^k, \dots, 2^{k+1} - 1\)), followed by Batcher's odd-even merger on \(2^{k+1}\) wires.

def oddEvenSortN : ℕ → List (ℕ × ℕ)
  | 0 => []
  | k + 1 => oddEvenSortN k ++ relabel (fun i => 2 ^ k + i) (oddEvenSortN k) ++ oddEvenMerge k

Uses 2 · Used by 6

Statement usesBatcher's odd-even merger · Relabeling the wires of a comparator list

Used byDepth bound for Batcher's odd-even merge sort as a comparator list · Size of Batcher's odd-even merge sort · Odd-even merge sort sorts every \(0\)-\(1\) input · Batcher'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

TheoremOutput of the last layer of the odd-even merger#✓fully proved

Let \(\alpha\) be a linearly ordered type, \(k \in \mathbb{N}\) and \(f : \mathbb{N} \to \alpha\) an assignment of values to the wires. Running the final layer for \(k\) on \(f\) gives at a wire \(x\) the value \(\min(f(x), f(x + 1))\) if \(x\) is odd and \(\lfloor x / 2 \rfloor < 2^{k+1} - 1\); otherwise the value \(\max(f(x - 1), f(x))\) if \(x\) is even, \(x > 0\) and \((x - 2) / 2 < 2^{k+1} - 1\); and the value \(f(x)\) in all other cases. In other words, for each \(i < 2^{k+1} - 1\) wire \(2i + 1\) receives the minimum and wire \(2i + 2\) the maximum of the values of \(f\) on these two wires, and every other wire keeps its value.

theorem runN_finalLayer {α : Type*} [LinearOrder α] (k : ℕ) (f : ℕ → α) (x : ℕ) :
    runN (finalLayer k) f x =
      if x % 2 = 1 ∧ x / 2 < 2 ^ (k + 1) - 1 then min (f x) (f (x + 1))
      else if x % 2 = 0 ∧ 0 < x ∧ (x - 2) / 2 < 2 ^ (k + 1) - 1 then max (f (x - 1)) (f x)
      else f x

Uses 3 · Used by 1

Statement usesRunning a comparator network on natural-number-indexed wires · Last layer of the odd-even merger

Proof usesComparator on natural-number-indexed wires

Used byThe odd-even merger merges

TheoremThe odd-even merger merges#✓fully proved

Let \(k \in \mathbb{N}\) and let \(f\) assign a Boolean value to each wire \(0, 1, 2, \dots\), with false read as \(0\) and true as \(1\). Let \(a, c \le 2^k\) be such that wires \(0, \dots, 2^k - 1\) hold \(a\) zeros followed by ones (wire \(i < 2^k\) holds \(0\) exactly when \(i < a\)) and wires \(2^k, \dots, 2^{k+1} - 1\) hold \(c\) zeros followed by ones (wire \(2^k + i\), for \(i < 2^k\), holds \(0\) exactly when \(i < c\)). Then after Batcher's odd-even merger on \(2^{k+1}\) wires runs on \(f\), every wire \(j < 2^{k+1}\) holds \(0\) exactly when \(j < a + c\).

theorem oddEvenMerge_merges : ∀ (k : ℕ) (f : ℕ → Bool) (a c : ℕ), a ≤ 2 ^ k → c ≤ 2 ^ k →
    (∀ i < 2 ^ k, f i = decide (a ≤ i)) → (∀ i < 2 ^ k, f (2 ^ k + i) = decide (c ≤ i)) →
    ∀ j < 2 ^ (k + 1), runN (oddEvenMerge k) f j = decide (a + c ≤ j)

Uses 8 · Used by 1

Statement usesRunning a comparator network on natural-number-indexed wires · Batcher's odd-even merger

Proof usesComparator on natural-number-indexed wires · Last layer of the odd-even merger · Relabeling the wires of a comparator list · Output of the last layer of the odd-even merger · Running a relabeled network · Relabeled networks fix the wires outside the image

Used byOdd-even merge sort sorts every \(0\)-\(1\) input

TheoremOdd-even merge sort sorts every \(0\)-\(1\) input#✓fully proved

Let \(k \in \mathbb{N}\) and let \(f\) assign a Boolean value to each wire \(0, 1, 2, \dots\), with false read as \(0\) and true as \(1\). After Batcher's odd-even merge sort on \(2^k\) wires runs on \(f\), there is \(z \le 2^k\) such that every wire \(j < 2^k\) holds \(0\) exactly when \(j < z\): wires \(0, \dots, 2^k - 1\) hold \(z\) zeros followed by ones.

theorem oddEvenSortN_sorts : ∀ (k : ℕ) (f : ℕ → Bool),
    ∃ z ≤ 2 ^ k, ∀ j < 2 ^ k, runN (oddEvenSortN k) f j = decide (z ≤ j)

Uses 8 · Used by 1

Statement usesRunning a comparator network on natural-number-indexed wires · Batcher's odd-even merge sort

Proof usesComparator on natural-number-indexed wires · Batcher's odd-even merger · The odd-even merger merges · Relabeling the wires of a comparator list · Running a relabeled network · Relabeled networks fix the wires outside the image

Used byBatcher's odd-even merge sort sorts every input over every linear order

TheoremRelabeling keeps comparators within an interval#✓fully proved

Let \(ps\) be a list of comparators, each a pair of natural numbers, that lies within \([l, h)\), and let \(e : \mathbb{N} \to \mathbb{N}\) satisfy \(l' \le e(x) < h'\) for every \(x\) with \(l \le x < h\). Then the list obtained from \(ps\) by relabeling its wires by \(e\) lies within \([l', h')\).

theorem relabel_within {ps : List (ℕ × ℕ)} {lo hi : ℕ} (h : Within ps lo hi) (e : ℕ → ℕ)
    {lo' hi' : ℕ} (he : ∀ x, lo ≤ x → x < hi → lo' ≤ e x ∧ e x < hi') :
    Within (relabel e ps) lo' hi'

Uses 2 · Used by 3

Statement usesComparators within an interval · Relabeling the wires of a comparator list

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

TheoremSize of the odd-even merger#✓fully proved

For every \(k \in \mathbb{N}\), Batcher's odd-even merger on \(2^{k+1}\) wires consists of exactly \(k \cdot 2^k + 1\) comparators.

theorem length_oddEvenMerge : ∀ k, (oddEvenMerge k).length = k * 2 ^ k + 1

Uses 3 · Used by 1

Statement usesBatcher's odd-even merger

Proof usesLast layer of the odd-even merger · Relabeling the wires of a comparator list

Used bySize of Batcher's odd-even merge sort

TheoremSize of Batcher's odd-even merge sort#✓fully proved

For every \(k \in \mathbb{N}\), the number \(L\) of comparators of Batcher's odd-even merge sort on \(2^k\) wires satisfies \(4(L + 1) + k \cdot 2^k = (k^2 + 4) \cdot 2^k\), that is, \(L = (k^2 - k + 4) \cdot 2^k / 4 - 1\).

The identity is stated without subtraction or division, and is exact for every \(k\).

theorem length_oddEvenSortN : ∀ k,
    4 * ((oddEvenSortN k).length + 1) + k * 2 ^ k = (k * k + 4) * 2 ^ k

Uses 4

Statement usesBatcher's odd-even merge sort

Proof usesSize of the odd-even merger · Batcher's odd-even merger · Relabeling the wires of a comparator list

DefinitionBatcher's odd-even merge sorting network#✓fully proved

For \(k \in \mathbb{N}\), this is the comparator network on the \(2^k\) wires \(0, \dots, 2^k - 1\) given by the comparators of Batcher's odd-even merge sort on \(2^k\) wires, in the same order, with any comparator that touches a wire \(\ge 2^k\) dropped.

def oddEvenSorter (k : ℕ) : Network (2 ^ k) := ofPairs (2 ^ k) (oddEvenSortN k)

Uses 3 · Used by 3

Statement usesRestricting comparators to finitely many wires · Comparator network · Batcher's odd-even merge sort

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 odd-even merge sort sorts every input over every linear order

TheoremBatcher's odd-even merge sort sorts every input over every linear order#✓fully proved

For every \(k \in \mathbb{N}\) and every linearly ordered type \(\alpha\), Batcher's odd-even merge sorting network on \(2^k\) wires sorts every input over \(\alpha\): for every assignment \(v\) of elements of \(\alpha\) to the wires \(0, \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 oddEvenSorter_sorts (k : ℕ) (α : Type*) [LinearOrder α] :
    Sorts (oddEvenSorter k) α

Uses 16 · Used by 1

Statement usesBatcher's odd-even merge sorting 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 · Restricting comparators to finitely many wires · Running a comparator network on natural-number-indexed wires · Comparator network · Last layer of the odd-even merger · Batcher's odd-even merger · Batcher's odd-even merge sort · Odd-even merge sort sorts every \(0\)-\(1\) input · Relabeling the wires of a comparator list · Relabeling keeps comparators within an interval · Running a comparator network · The 0-1 principle

Used byLower bound for the depth of Batcher's odd-even merge sorting network

TheoremLevels of a relabeled comparator list#✓fully proved

Let \(e : \mathbb{N} \to \mathbb{N}\) be injective, let \(p\) be a comparator list and let \(\ell\) be an initial level assignment. For every wire \(j\), the level of wire \(e(j)\) after running \(p\) with its wires relabeled by \(e\), starting from \(\ell\), equals the level of wire \(j\) after running \(p\) starting from \(\ell \circ e\).

theorem levels_relabel {e : ℕ → ℕ} (he : Function.Injective e) :
    ∀ (ps : List (ℕ × ℕ)) (lv : ℕ → ℕ) (j : ℕ),
      levels (relabel e ps) lv (e j) = levels ps (fun i => lv (e i)) j

Uses 2 · Used by 2

Statement usesComparator levels under earliest scheduling · Relabeling the wires of a comparator list

Used byRelabeling wires preserves a depth bound · Levels of a relabeled comparator list on the image wires

TheoremRelabeled comparator lists leave the other wires alone#✓fully proved

Let \(p\) be a comparator list, let \(e : \mathbb{N} \to \mathbb{N}\) be any map and let \(\ell\) be an initial level assignment. For every wire \(x\) outside the image of \(e\), the level of \(x\) after running \(p\) with its wires relabeled by \(e\), starting from \(\ell\), is \(\ell(x)\).

theorem levels_relabel_of_not_mem {e : ℕ → ℕ} :
    ∀ (ps : List (ℕ × ℕ)) (lv : ℕ → ℕ) (x : ℕ), (∀ y, x ≠ e y) →
      levels (relabel e ps) lv x = lv x

Uses 2 · Used by 2

Statement usesComparator levels under earliest scheduling · Relabeling the wires of a comparator list

Used byParallel composition of relabeled comparator lists · Relabeling wires preserves a depth bound

TheoremRelabeling wires preserves a depth bound#✓fully proved

If a comparator list has depth at most \(d\) and \(e : \mathbb{N} \to \mathbb{N}\) is injective, then the comparator list obtained by relabeling its wires by \(e\) also has depth at most \(d\).

theorem depthLE_relabel {ps : List (ℕ × ℕ)} {d : ℕ} (h : DepthLE ps d) {e : ℕ → ℕ}
    (he : Function.Injective e) : DepthLE (relabel e ps) d

Uses 5 · Used by 2

Statement usesDepth bound for a comparator list · Relabeling the wires of a comparator list

Proof usesComparator levels under earliest scheduling · Levels of a relabeled comparator list · Relabeled comparator lists leave the other wires alone

Used byParallel composition of relabeled comparator lists · Depth bound for Batcher's odd-even merge sort as a comparator list

TheoremLevels of a relabeled comparator list on the image wires#✓fully proved

Let \(p\) be a comparator list and let \(e : \mathbb{N} \to \mathbb{N}\) be injective. If two initial level assignments \(\ell\) and \(\ell'\) agree on every wire \(e(y)\), then the levels after running \(p\) with its wires relabeled by \(e\), starting from \(\ell\) and from \(\ell'\), agree on every wire \(e(y)\).

theorem levels_relabel_congr {e : ℕ → ℕ} (he : Function.Injective e) (ps : List (ℕ × ℕ))
    {lv lv' : ℕ → ℕ} (h : ∀ y, lv (e y) = lv' (e y)) (y : ℕ) :
    levels (relabel e ps) lv (e y) = levels (relabel e ps) lv' (e y)

Uses 3 · Used by 1

Statement usesComparator levels under earliest scheduling · Relabeling the wires of a comparator list

Proof usesLevels of a relabeled comparator list

Used byParallel composition of relabeled comparator lists

TheoremParallel composition of relabeled comparator lists#✓fully proved

Let \(e\) and \(e'\) be injective maps \(\mathbb{N} \to \mathbb{N}\) with disjoint images, that is, \(e(y) \ne e'(y')\) for all \(y\) and \(y'\). If the comparator lists \(p\) and \(q\) both have depth at most \(d\), then \(p\) with its wires relabeled by \(e\), followed by \(q\) with its wires relabeled by \(e'\), has depth at most \(d\).

theorem depthLE_append_relabel {ps qs : List (ℕ × ℕ)} {d : ℕ} (hp : DepthLE ps d)
    (hq : DepthLE qs d) {e e' : ℕ → ℕ} (he : Function.Injective e) (he' : Function.Injective e')
    (hdis : ∀ y y', e y ≠ e' y') : DepthLE (relabel e ps ++ relabel e' qs) d

Uses 6 · Used by 1

Statement usesDepth bound for a comparator list · Relabeling the wires of a comparator list

Proof usesComparator levels under earliest scheduling · Relabeling wires preserves a depth bound · Levels of a relabeled comparator list on the image wires · Relabeled comparator lists leave the other wires alone

Used byDepth bound for Batcher's odd-even merger

TheoremThe final layer of the odd-even merger has depth at most one#✓fully proved

For every \(k\), the final layer of the odd-even merger on \(2^{k+2}\) wires, which compares wires \(2i + 1\) and \(2i + 2\) for each \(i < 2^{k+1} - 1\), has depth at most \(1\): its comparators are disjoint.

theorem depthLE_finalLayer (k : ℕ) : DepthLE (finalLayer k) 1

Uses 3 · Used by 1

Statement usesDepth bound for a comparator list · Last layer of the odd-even merger

Proof usesComparator levels under earliest scheduling

Used byDepth bound for Batcher's odd-even merger

TheoremDepth bound for Batcher's odd-even merger#✓fully proved

For every \(k\), Batcher's odd-even merger on \(2^{k+1}\) wires has depth at most \(k + 1\).

theorem depthLE_oddEvenMerge : ∀ k, DepthLE (oddEvenMerge k) (k + 1)

Uses 8 · Used by 1

Statement usesDepth bound for a comparator list · Batcher's odd-even merger

Proof usesDepth of sequential composition of comparator lists · Comparator levels under earliest scheduling · Parallel composition of relabeled comparator lists · The final layer of the odd-even merger has depth at most one · Last layer of the odd-even merger · Relabeling the wires of a comparator list

Used byDepth bound for Batcher's odd-even merge sort as a comparator list

TheoremDepth bound for Batcher's odd-even merge sort as a comparator list#✓fully proved

For every \(k\), there is a \(d\) with \(2d \le k(k+1)\) such that the comparator list of Batcher's odd-even merge sort on wires \(0, \dots, 2^k - 1\) has depth at most \(d\); that is, its depth is at most \(k(k+1)/2\).

theorem depthLE_oddEvenSortN : ∀ k, ∃ d, DepthLE (oddEvenSortN k) d ∧ 2 * d ≤ k * (k + 1)

Uses 12 · Used by 1

Statement usesDepth bound for a comparator list · Batcher's odd-even merge sort

Proof usesDepth of sequential composition of comparator lists · Parallel composition of comparator lists on adjacent blocks · Comparators within an interval · Comparator levels under earliest scheduling · Depth bound for Batcher's odd-even merger · Relabeling wires preserves a depth bound · Last layer of the odd-even merger · Batcher's odd-even merger · Relabeling the wires of a comparator list · Relabeling keeps comparators within an interval

Used byDepth bound for Batcher's odd-even merge sorting network

TheoremDepth bound for Batcher's odd-even merge sorting network#✓fully proved

For every \(k\), there is a \(d\) with \(2d \le k(k+1)\) such that Batcher's odd-even merge sorting network on \(2^k\) wires has depth at most \(d\); that is, its depth is at most \(k(k+1)/2\).

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

Uses 13

Statement usesDepth bound for a comparator network · Batcher's odd-even merge sorting network

Proof usesDepth bound for a comparator list · Comparators within an interval · Restricting comparators to finitely many wires · Comparator network · Comparator list of a network · Depth bound for Batcher's odd-even merge sort as a comparator list · Last layer of the odd-even merger · Batcher's odd-even merger · Batcher's odd-even merge sort · Relabeling the wires of a comparator list · Relabeling keeps comparators within an interval

TheoremLower bound for the depth of Batcher's odd-even merge sorting network#✓fully proved

For all \(k\) and \(d\), if Batcher's odd-even merge sorting network on \(2^k\) wires has depth at most \(d\), then \(k \le d\).

theorem le_of_oddEvenSorter_depthLE {k d : ℕ} (hd : Network.DepthLE (oddEvenSorter k) d) :
    k ≤ d

Uses 4

Statement usesDepth bound for a comparator network · Batcher's odd-even merge sorting network

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

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.