Sorting networks and the zero-one principle

AbbreviationComparator network#✓fully proved

A comparator network on \(n\) wires is a finite list of pairs \((i, j)\) of wires \(i, j \in \{0, \dots, n - 1\}\), each pair standing for the comparator \((i, j)\); the comparators are applied in list order.

abbrev Network (n : ℕ) := List (Fin n × Fin n)

Used by 28

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 · Transported comparator lists agree with the original on Boolean inputs · Comparator count of Batcher's bitonic sorter · Restricting comparators to finitely many wires · Bubble sorting network · The bubble network sorts · Size of the bubble sorting network · Size of a bubble pass · Bubble pass · Effect of one bubble pass · Successive bubble passes · 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\) · Comparator list of a network · Running a comparator network · Networks commute with monotone maps · The output of a comparator network is a permutation of its input · Networks that sort · Boolean sorting test · The Boolean sorting test is correct · The 0-1 principle · A network that passes the Boolean sorting test sorts over every linear order · Sorting distinct inputs suffices · The permutation principle

DefinitionComparator#✓fully proved

Let \(\alpha\) be a linear order, let \(n\) be a natural number, and let \(v\) assign a value \(v(k) \in \alpha\) to each wire \(k \in \{0, \dots, n - 1\}\). For wires \(i\) and \(j\), the comparator \((i, j)\) sends \(v\) to the assignment that has \(\min(v(i), v(j))\) on wire \(i\), \(\max(v(i), v(j))\) on wire \(j\) when \(j \ne i\), and \(v(k)\) on every other wire \(k\).

def comparator (i j : Fin n) (v : Fin n → α) : Fin n → α :=
  fun k => if k = i then min (v i) (v j) else if k = j then max (v i) (v j) else v k

Used by 8

Used byTransported comparator lists agree with the original on Boolean inputs · The bubble network sorts · Effect of one bubble pass · Comparators commute with monotone maps · A comparator permutes its inputs · Running a comparator network · Networks commute with monotone maps · The output of a comparator network is a permutation of its input

DefinitionRunning a comparator network#✓fully proved

Let \(\alpha\) be a linear order. The output of a comparator network on an assignment \(v\) of a value in \(\alpha\) to each of its \(n\) wires is obtained by starting from \(v\) and applying the comparators of the network one after another, in list order.

def run (net : Network n) (v : Fin n → α) : Fin n → α :=
  net.foldl (fun w c => comparator c.1 c.2 w) v

Uses 2 · Used by 14

Statement usesComparator 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 · Transported comparator lists agree with the original on Boolean inputs · The bubble network sorts · Effect of one bubble pass · Every sorting network on \(n\) wires has depth at least \(\log_2 n\) · Networks commute with monotone maps · The output of a comparator network is a permutation of its input · Networks that sort · Boolean sorting test · The Boolean sorting test is correct · The 0-1 principle · Sorting distinct inputs suffices · The permutation principle

DefinitionNetworks that sort#✓fully proved

A comparator network on \(n\) wires sorts inputs over a linearly ordered type \(\alpha\) if, for every input \(v\) assigning a value in \(\alpha\) to each wire, the output of running the network on \(v\) is monotone in the wire order: for all wires \(i \le j\), the output value on wire \(i\) is at most the output value on wire \(j\).

def Sorts (net : Network n) (α : Type*) [LinearOrder α] : Prop :=
  ∀ v : Fin n → α, Monotone (run net v)

Uses 2 · Used by 9

Statement usesComparator network · Running a comparator network

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 · The bubble network sorts · Every sorting network on \(n\) wires has depth at least \(\log_2 n\) · The Boolean sorting test is correct · The 0-1 principle · A network that passes the Boolean sorting test sorts over every linear order · Sorting distinct inputs suffices · The permutation principle

TheoremComparators commute with monotone maps#✓fully proved

Let \(\alpha\) and \(\beta\) be linear orders, let \(f : \alpha \to \beta\) be monotone, and let \(n\) be a natural number. For all wires \(i, j \in \{0, \dots, n - 1\}\) and every assignment \(v\) of a value in \(\alpha\) to each wire, the comparator \((i, j)\) applied to \(f \circ v\) gives \(f \circ w\), where \(w\) is the output of the comparator \((i, j)\) on \(v\).

theorem comparator_comp {f : α → β} (hf : Monotone f) (i j : Fin n) (v : Fin n → α) :
    comparator i j (f ∘ v) = f ∘ comparator i j v

Uses 1 · Used by 1

Statement usesComparator

Used byNetworks commute with monotone maps

TheoremNetworks commute with monotone maps#✓fully proved

Let \(\alpha\) and \(\beta\) be linear orders and let \(f : \alpha \to \beta\) be monotone. For every comparator network on \(n\) wires and every assignment \(v\) of a value in \(\alpha\) to each wire, the output of the network on \(f \circ v\) is \(f \circ w\), where \(w\) is the output of the network on \(v\).

theorem run_comp {f : α → β} (hf : Monotone f) :
    ∀ (net : Network n) (v : Fin n → α), run net (f ∘ v) = f ∘ run net v

Sources

• CLRS, second edition, Lemma 27.1.

Uses 4 · Used by 3

Statement usesComparator network · Running a comparator network

Proof usesComparator · Comparators commute with monotone maps

Used byThe 0-1 principle · Sorting distinct inputs suffices · The permutation principle

TheoremA comparator permutes its inputs#✓fully proved

Let \(\alpha\) be a linear order and let \(n\) be a natural number. For all wires \(i, j \in \{0, \dots, n - 1\}\) and every assignment \(v\) of a value in \(\alpha\) to each wire, there is a permutation \(\sigma\) of the wires such that the output of the comparator \((i, j)\) on \(v\) is \(v \circ \sigma\).

theorem comparator_perm (i j : Fin n) (v : Fin n → α) :
    ∃ σ : Equiv.Perm (Fin n), comparator i j v = v ∘ σ

Uses 1 · Used by 1

Statement usesComparator

Used byThe output of a comparator network is a permutation of its input

TheoremThe output of a comparator network is a permutation of its input#✓fully proved

Let \(\alpha\) be a linear order. For every comparator network on \(n\) wires and every assignment \(v\) of a value in \(\alpha\) to each wire, there is a permutation \(\sigma\) of the wires such that the output of the network on \(v\) is \(v \circ \sigma\).

theorem run_perm : ∀ (net : Network n) (v : Fin n → α),
    ∃ σ : Equiv.Perm (Fin n), run net v = v ∘ σ

Uses 4

Statement usesComparator network · Running a comparator network

Proof usesComparator · A comparator permutes its inputs

TheoremThe 0-1 principle#✓fully proved

The 0-1 principle (CLRS Theorem 27.2): a network that sorts every Boolean input sorts every input over every linear order.

theorem sorts_of_sorts_bool {net : Network n} (h : Sorts net Bool) (α : Type*) [LinearOrder α] :
    Sorts net α

Uses 4 · Used by 4

Statement usesComparator network · Networks that sort

Proof usesRunning a comparator network · Networks commute with monotone maps

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 · A network that passes the Boolean sorting test sorts over every linear order · Sorting distinct inputs suffices

DefinitionBoolean sorting test#✓fully proved

The Boolean sorting test of a comparator network on \(n\) wires returns true exactly when, for every assignment \(v\) of a Boolean value to each wire, the output \(w\) of the network on \(v\) satisfies \(w(i) \le w(j)\) for all wires \(i \le j\), where \(\mathrm{false} < \mathrm{true}\).

It is computed by running the network on all \(2^n\) Boolean inputs.

def sortsBool (net : Network n) : Bool :=
  decide (∀ v : Fin n → Bool, ∀ i j : Fin n, i ≤ j → run net v i ≤ run net v j)

Uses 2 · Used by 2

Statement usesComparator network · Running a comparator network

Used byThe Boolean sorting test is correct · A network that passes the Boolean sorting test sorts over every linear order

TheoremThe Boolean sorting test is correct#✓fully proved

A comparator network passes the Boolean sorting test if and only if it sorts inputs over the Booleans, that is, for every assignment of a Boolean value to each wire, the output of the network is monotone in the wire order.

theorem sortsBool_eq_true_iff {net : Network n} : sortsBool net = true ↔ Sorts net Bool

Uses 4 · Used by 1

Statement usesComparator network · Networks that sort · Boolean sorting test

Proof usesRunning a comparator network

Used byA network that passes the Boolean sorting test sorts over every linear order

TheoremA network that passes the Boolean sorting test sorts over every linear order#✓fully proved

If a comparator network on \(n\) wires passes the Boolean sorting test, then for every linear order \(\alpha\) it sorts inputs over \(\alpha\): for every assignment \(v\) of a value in \(\alpha\) to each wire, the output of the network on \(v\) is monotone in the wire order.

theorem sorts_of_sortsBool {net : Network n} (h : sortsBool net = true) (α : Type*)
    [LinearOrder α] : Sorts net α

Uses 5

Statement usesComparator network · Networks that sort · Boolean sorting test

Proof usesThe Boolean sorting test is correct · The 0-1 principle

DefinitionSpread of a Boolean input#✓fully proved

For a Boolean input \(v\) on \(n\) wires, the spread of \(v\) is the input with natural-number values whose value on wire \(i < n\) is \(n + i\) if \(v(i)\) is true and \(i\) if \(v(i)\) is false.

The values of the spread are pairwise distinct.

def spread (v : Fin n → Bool) (i : Fin n) : ℕ := (if v i then n else 0) + i

Used by 2

Used byA Boolean input is a threshold of its spread · Sorting distinct inputs suffices

TheoremA Boolean input is a threshold of its spread#✓fully proved

For every Boolean input \(v\) on \(n\) wires, applying the threshold map that sends a natural number \(k\) to true if \(n \le k\) and to false otherwise to the spread of \(v\) gives back \(v\): for every wire \(i\), the spread of \(v\) at \(i\) is at least \(n\) exactly when \(v(i)\) is true.

Since the threshold map is monotone, \(v\) is a monotone image of its spread.

theorem decide_le_spread (v : Fin n → Bool) : (fun k => decide (n ≤ k)) ∘ spread v = v

Uses 1 · Used by 1

Statement usesSpread of a Boolean input

Used bySorting distinct inputs suffices

TheoremSorting distinct inputs suffices#✓fully proved

A network that sorts every input with distinct natural values sorts every input over every linear order.

theorem sorts_of_sorts_injective {net : Network n}
    (h : ∀ w : Fin n → ℕ, Function.Injective w → Monotone (run net w)) (α : Type*)
    [LinearOrder α] : Sorts net α

Uses 7 · Used by 1

Statement usesComparator network · Networks that sort · Running a comparator network

Proof usesA Boolean input is a threshold of its spread · Networks commute with monotone maps · The 0-1 principle · Spread of a Boolean input

Used byThe permutation principle

DefinitionRank among the values of an input#✓fully proved

For a map \(w\) from \(\{0, \dots, n-1\}\) to the natural numbers and an index \(i < n\), the rank of \(w(i)\) among the values of \(w\) is the number of indices \(j < n\) with \(w(j) < w(i)\). It is less than \(n\), so it is again an index in \(\{0, \dots, n-1\}\).

def rank (w : Fin n → ℕ) (i : Fin n) : Fin n :=
  ⟨(Finset.univ.filter fun j => w j < w i).card, by
    calc (Finset.univ.filter fun j => w j < w i).card
        < (Finset.univ : Finset (Fin n)).card :=
          Finset.card_lt_card ⟨Finset.filter_subset _ _, fun h => by
            have := Finset.mem_filter.1 (h (Finset.mem_univ i)); omega⟩
      _ = n := Finset.card_fin n⟩

Used by 2

Used byThe ranking permutation · The permutation principle

DefinitionThe ranking permutation#✓fully proved

For an injective map \(w\) from \(\{0, \dots, n-1\}\) to the natural numbers, the ranking permutation of \(w\) is the permutation of \(\{0, \dots, n-1\}\) that sends each \(i\) to the rank of \(w(i)\) among the values of \(w\), that is, to the number of indices \(j\) with \(w(j) < w(i)\). Since \(w\) is injective, this map is a bijection.

The ranking permutation has the same relative order as \(w\).

noncomputable def rankPerm {w : Fin n → ℕ} (hw : Function.Injective w) : Equiv.Perm (Fin n) :=
  Equiv.ofBijective (rank w) (Finite.injective_iff_bijective.1 (rank_injective hw))

Uses 1 · Used by 1

Statement usesRank among the values of an input

Used byThe permutation principle

TheoremThe permutation principle#✓fully proved

A comparator network on \(n\) wires that sorts each of the \(n!\) permutations \(\sigma\) of \(\{0, \dots, n-1\}\), viewed as the input whose value on wire \(i\) is \(\sigma(i)\), sorts every input over every linear order.

theorem sorts_of_sorts_perm {net : Network n}
    (h : ∀ σ : Equiv.Perm (Fin n), Monotone (run net σ)) (α : Type*) [LinearOrder α] :
    Sorts net α

Uses 7

Statement usesComparator network · Networks that sort · Running a comparator network

Proof usesRank among the values of an input · The ranking permutation · Networks commute with monotone maps · Sorting distinct inputs suffices

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.