Bubble sorting network

DefinitionAdjacent comparator#✓fully proved

For \(n\) wires and an index \(i\), this is the comparator on wires \(i\) and \(i + 1\) when \(i + 1 < n\), and nothing when wire \(i + 1\) does not exist.

def adjacent (n i : ℕ) : Option (Fin n × Fin n) :=
  if h : i + 1 < n then some (⟨i, by omega⟩, ⟨i + 1, h⟩) else none

Used by 3

Used bySize of a bubble pass · Bubble pass · Effect of one bubble pass

DefinitionBubble pass#✓fully proved

On \(n\) wires, the bubble pass ending at wire \(m\) is the comparator network \((0, 1), (1, 2), \ldots, (m - 1, m)\), applied in this order, where a comparator \((i, i + 1)\) is left out when wire \(i + 1\) does not exist (that is, when \(i + 1 \ge n\)).

def pass (n m : ℕ) : Network n := (List.range m).filterMap (adjacent n)

Uses 2 · Used by 5

Statement usesAdjacent comparator · Comparator network

Used byThe bubble network sorts · Size of the bubble sorting network · Size of a bubble pass · Effect of one bubble pass · Successive bubble passes

DefinitionSuccessive bubble passes#✓fully proved

On \(n\) wires and for a number \(m\), this is the comparator network obtained by concatenating the bubble passes ending at wires \(m - 1, m - 2, \ldots, 0\), in this order; for \(m = 0\) it is empty.

def passes (n : ℕ) : ℕ → Network n
  | 0 => []
  | m + 1 => pass n m ++ passes n m

Uses 2 · Used by 3

Statement usesBubble pass · Comparator network

Used byBubble sorting network · The bubble network sorts · Size of the bubble sorting network

DefinitionBubble sorting network#✓fully proved

The bubble sorting network on \(n\) wires is the comparator network obtained by concatenating the bubble passes ending at wires \(n - 1, n - 2, \ldots, 0\), in this order, where the bubble pass ending at wire \(k\) consists of the comparators \((0, 1), (1, 2), \ldots, (k - 1, k)\).

def bubble (n : ℕ) : Network n := passes n n

Uses 2 · Used by 2

Statement usesSuccessive bubble passes · Comparator network

Used byThe bubble network sorts · Size of the bubble sorting network

TheoremEffect of one bubble pass#✓fully proved

Let \(w\) be an input on \(n\) wires with values in a linearly ordered type, let \(m < n\), and let \(w'\) be the output of the bubble pass ending at wire \(m\) (the comparators \((0, 1), \ldots, (m - 1, m)\)) run on \(w\). Then \(w'_i = w_i\) for every wire \(i > m\); \(w'_i \le w'_m\) for every wire \(i \le m\); and for every wire \(i \le m\) there is a wire \(j \le m\) with \(w'_i = w_j\).

theorem pass_spec : ∀ (m : ℕ) (hm : m < n) (w : Fin n → α),
    (∀ i : Fin n, m < i.val → run (pass n m) w i = w i) ∧
    (∀ i : Fin n, i.val ≤ m → run (pass n m) w i ≤ run (pass n m) w ⟨m, hm⟩) ∧
    (∀ i : Fin n, i.val ≤ m → ∃ j : Fin n, j.val ≤ m ∧ run (pass n m) w i = w j)

Uses 5 · Used by 1

Statement usesBubble pass · Running a comparator network

Proof usesAdjacent comparator · Comparator network · Comparator

Used byThe bubble network sorts

DefinitionSettled top wires#✓fully proved

Let \(w\) assign to each of \(n\) wires a value in a linearly ordered type, and let \(m\) be a natural number. Then \(w\) is settled from \(m\) when \(w_i \le w_j\) for all wires \(m \le i \le j\) (the wires \(m, \ldots, n - 1\) are sorted) and \(w_i \le w_j\) for all wires \(i < m \le j\) (they hold the largest values). This is the invariant before the bubble pass ending at wire \(m - 1\).

def Settled (m : ℕ) (w : Fin n → α) : Prop :=
  (∀ i j : Fin n, m ≤ i.val → i ≤ j → w i ≤ w j) ∧
    (∀ i j : Fin n, i.val < m → m ≤ j.val → w i ≤ w j)

Used by 1

Used byThe bubble network sorts

TheoremThe bubble network sorts#✓fully proved

The bubble network sorts every input over every linear order.

theorem bubble_sorts : Sorts (bubble n) α

Uses 9

Statement usesBubble sorting network · Networks that sort

Proof usesSettled top wires · Bubble pass · Effect of one bubble pass · Successive bubble passes · Comparator network · Comparator · Running a comparator network

TheoremSize of a bubble pass#✓fully proved

On \(n\) wires, for every \(m < n\) the bubble pass ending at wire \(m\) has exactly \(m\) comparators.

theorem length_pass {m : ℕ} (hm : m < n) : (pass n m).length = m

Uses 3 · Used by 1

Statement usesBubble pass

Proof usesAdjacent comparator · Comparator network

Used bySize of the bubble sorting network

TheoremSize of the bubble sorting network#✓fully proved

For every \(n\), the bubble sorting network on \(n\) wires has \(n(n - 1)/2\) comparators: twice its number of comparators is \(n(n - 1)\).

theorem length_bubble : 2 * (bubble n).length = n * (n - 1)

Uses 5

Statement usesBubble sorting network

Proof usesSize of a bubble pass · Bubble pass · Successive bubble passes · Comparator network

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.