Replaying and reversing bitonic sorting decisions

Record one Boolean for each comparison in the existing bitonic algorithm. These decisions route arbitrary payloads and can be replayed in reverse to recover their original positions. In particular, a pointwise transformation of sorted records can be restored without sorting again or attaching unique identifiers. Equal keys need no special hypothesis: the trace records this sorter's actual choices, including the reversal of descending ties.

The trace definitions specify the decisions; they are not an optimized implementation of sorting with a trace. Circuit realizations must share comparisons and account for retained controls separately. The exact trace lengths below count Boolean decisions, not execution time.

Main definitions

• Cslib.BitonicSort.mergeTrace, Cslib.BitonicSort.sortTrace: record comparison decisions.
• Cslib.BitonicSort.routeSort: replay saved decisions on arbitrary payloads.
• Cslib.BitonicSort.unrouteSort: reverse those decisions.

Main results

• Cslib.BitonicSort.unrouteSort_routeSort, Cslib.BitonicSort.routeSort_unrouteSort: replay and reversal are mutually inverse for every trace, even one not obtained by sorting.
• Cslib.BitonicSort.routeSort_sortTrace: replay agrees with the existing bitonic algorithm.
• Cslib.BitonicSort.unrouteSort_comp_sort: restore pointwise transformed sorted records.
• Cslib.BitonicSort.four_mul_sortTraceSize: exact number of retained comparison decisions.

References

• K. E. Batcher, Sorting Networks and Their Applications.

def Cslib.BitonicSort.routeLayer {α : Type u_1} {n : ℕ} (flags : Fin n → Bool) (x : Fin (n + n) → α) : Fin (n + n) → α

Exchange corresponding entries between two halves according to saved flags.

@[simp]

theorem Cslib.BitonicSort.routeLayer_routeLayer {α : Type u_1} {n : ℕ} (flags : Fin n → Bool) (x : Fin (n + n) → α) : routeLayer flags (routeLayer flags x) = x

A layer's flags route any payload back when applied twice.

def Cslib.BitonicSort.layerFlags {α : Type u_1} {κ : Type u_3} [LinearOrder κ] (key : α → κ) {n : ℕ} (ascending : Bool) (x : Fin (n + n) → α) : Fin n → Bool

The comparison flags used by the existing ascending or descending layer.

theorem Cslib.BitonicSort.routeLayer_layerFlags {α : Type u_1} {κ : Type u_3} [LinearOrder κ] (key : α → κ) {n : ℕ} (ascending : Bool) (x : Fin (n + n) → α) : routeLayer (layerFlags key ascending x) x = compareLayer key ascending x

def Cslib.BitonicSort.mergeTraceSize : ℕ → ℕ

Number of decisions retained by bitonic merge.

def Cslib.BitonicSort.sortTraceSize : ℕ → ℕ

Number of decisions retained by bitonic sorting.

def Cslib.BitonicSort.mergeTrace {α : Type u_1} {κ : Type u_3} [LinearOrder κ] (key : α → κ) (d : ℕ) : Bool → (Fin (arity d) → α) → Fin (mergeTraceSize d) → Bool

Extract merge controls in the order: current layer, left child, right child.

def Cslib.BitonicSort.sortTrace {α : Type u_1} {κ : Type u_3} [LinearOrder κ] (key : α → κ) (d : ℕ) : Bool → (Fin (arity d) → α) → Fin (sortTraceSize d) → Bool

Extract sort controls in the order: left sort, right sort, final merge.

def Cslib.BitonicSort.routeMerge {α : Type u_1} (d : ℕ) : (Fin (mergeTraceSize d) → Bool) → (Fin (arity d) → α) → Fin (arity d) → α

Route payloads through a merge using its saved decisions, without comparing them.

def Cslib.BitonicSort.unrouteMerge {α : Type u_1} (d : ℕ) : (Fin (mergeTraceSize d) → Bool) → (Fin (arity d) → α) → Fin (arity d) → α

Reverse a merge by undoing its children before its current layer.

def Cslib.BitonicSort.routeSort {α : Type u_1} (d : ℕ) : (Fin (sortTraceSize d) → Bool) → (Fin (arity d) → α) → Fin (arity d) → α

Route payloads through a sort using its saved decisions.

def Cslib.BitonicSort.unrouteSort {α : Type u_1} (d : ℕ) : (Fin (sortTraceSize d) → Bool) → (Fin (arity d) → α) → Fin (arity d) → α

Reverse the final merge before undoing the two child sorts.

@[simp]

theorem Cslib.BitonicSort.unrouteMerge_routeMerge {α : Type u_1} (d : ℕ) (flags : Fin (mergeTraceSize d) → Bool) (x : Fin (arity d) → α) : unrouteMerge d flags (routeMerge d flags x) = x

@[simp]

theorem Cslib.BitonicSort.routeMerge_unrouteMerge {α : Type u_1} (d : ℕ) (flags : Fin (mergeTraceSize d) → Bool) (x : Fin (arity d) → α) : routeMerge d flags (unrouteMerge d flags x) = x

@[simp]

theorem Cslib.BitonicSort.unrouteSort_routeSort {α : Type u_1} (d : ℕ) (flags : Fin (sortTraceSize d) → Bool) (x : Fin (arity d) → α) : unrouteSort d flags (routeSort d flags x) = x

@[simp]

theorem Cslib.BitonicSort.routeSort_unrouteSort {α : Type u_1} (d : ℕ) (flags : Fin (sortTraceSize d) → Bool) (x : Fin (arity d) → α) : routeSort d flags (unrouteSort d flags x) = x

theorem Cslib.BitonicSort.routeMerge_mergeTrace {α : Type u_1} {κ : Type u_3} [LinearOrder κ] (key : α → κ) (d : ℕ) (ascending : Bool) (x : Fin (arity d) → α) : routeMerge d (mergeTrace key d ascending x) x = merge key d ascending x

theorem Cslib.BitonicSort.routeSort_sortTrace {α : Type u_1} {κ : Type u_3} [LinearOrder κ] (key : α → κ) (d : ℕ) (ascending : Bool) (x : Fin (arity d) → α) : routeSort d (sortTrace key d ascending x) x = sort key d ascending x

theorem Cslib.BitonicSort.unrouteSort_sort {α : Type u_1} {κ : Type u_3} [LinearOrder κ] (key : α → κ) (d : ℕ) (ascending : Bool) (x : Fin (arity d) → α) : unrouteSort d (sortTrace key d ascending x) (sort key d ascending x) = x

theorem Cslib.BitonicSort.routeLayer_comp {α : Type u_1} {β : Type u_2} {n : ℕ} (flags : Fin n → Bool) (f : α → β) (x : Fin (n + n) → α) : routeLayer flags (f ∘ x) = f ∘ routeLayer flags x

Moving a payload and then transforming it is the same as transforming before moving.

theorem Cslib.BitonicSort.routeMerge_comp {α : Type u_1} {β : Type u_2} (d : ℕ) (flags : Fin (mergeTraceSize d) → Bool) (f : α → β) (x : Fin (arity d) → α) : routeMerge d flags (f ∘ x) = f ∘ routeMerge d flags x

Saved merge decisions do not inspect the payload.

theorem Cslib.BitonicSort.routeSort_comp {α : Type u_1} {β : Type u_2} (d : ℕ) (flags : Fin (sortTraceSize d) → Bool) (f : α → β) (x : Fin (arity d) → α) : routeSort d flags (f ∘ x) = f ∘ routeSort d flags x

Saved sort decisions do not inspect the payload.

theorem Cslib.BitonicSort.unrouteSort_comp_sort {α : Type u_1} {β : Type u_2} {κ : Type u_3} [LinearOrder κ] (key : α → κ) (d : ℕ) (ascending : Bool) (f : α → β) (x : Fin (arity d) → α) : unrouteSort d (sortTrace key d ascending x) (f ∘ sort key d ascending x) = f ∘ x

Reverse a sort's saved decisions after a pointwise transformation. Neither keys nor payloads need be distinct, and the transformed payload may have a different type.

theorem Cslib.BitonicSort.unrouteSort_comp {α : Type u_1} {β : Type u_2} (d : ℕ) (flags : Fin (sortTraceSize d) → Bool) (f : α → β) (x : Fin (arity d) → α) : unrouteSort d flags (f ∘ x) = f ∘ unrouteSort d flags x

Reversing saved decisions commutes with arbitrary pointwise transformations.

theorem Cslib.BitonicSort.unrouteSort_apply {α : Type u_1} (d : ℕ) (flags : Fin (sortTraceSize d) → Bool) (x : Fin (arity d) → α) (i : Fin (arity d)) : unrouteSort d flags x i = x (unrouteSort d flags id i)

Reversal reads the same original position for every payload type. This is deliberately not a simp lemma: rewriting the identity payload would expand the right-hand side again.

theorem Cslib.BitonicSort.unrouteSort_rel {α : Type u_1} {β : Type u_2} (d : ℕ) (flags : Fin (sortTraceSize d) → Bool) (x : Fin (arity d) → α) (y : Fin (arity d) → β) (R : α → β → Prop) (h : ∀ (i : Fin (arity d)), R (x i) (y i)) (i : Fin (arity d)) : R (unrouteSort d flags x i) (unrouteSort d flags y i)

Pointwise relations between two payload arrays survive reversal by the same saved trace.

theorem Cslib.BitonicSort.unrouteSort_rel_sort {α : Type u_1} {β : Type u_2} {κ : Type u_3} [LinearOrder κ] (key : α → κ) (d : ℕ) (ascending : Bool) (x : Fin (arity d) → α) (y : Fin (arity d) → β) (R : α → β → Prop) (h : ∀ (i : Fin (arity d)), R (sort key d ascending x i) (y i)) (i : Fin (arity d)) : R (x i) (unrouteSort d (sortTrace key d ascending x) y i)

Transfer specifications from sorted positions to literal original positions.

theorem Cslib.BitonicSort.two_mul_mergeTraceSize (d : ℕ) : 2 * mergeTraceSize d = d * 2 ^ d

A merge retains one decision for each comparator, or d * 2^d / 2 decisions.

theorem Cslib.BitonicSort.four_mul_sortTraceSize (d : ℕ) : 4 * sortTraceSize d = d * (d + 1) * 2 ^ d

A sort retains d * (d + 1) * 2^d / 4 decisions.