Batcher sorting on finite tuples

The algorithm sorts a power-of-two tuple of records by a separate key. Each layer compares corresponding records in two halves and moves whole records. Ascending comparisons retain ties; descending comparisons reverse the ascending result, including ties. The complete sorter is not a stable sorting algorithm.

Main definitions

• Cslib.BitonicSort.arity: the power-of-two number of records, with a definitional split.
• Cslib.BitonicSort.IsBitonic: the four-point lattice invariant used by bitonic merge.
• Cslib.BitonicSort.compareLayer: one layer of independent comparisons.
• Cslib.BitonicSort.merge: recursively merge a bitonic tuple.
• Cslib.BitonicSort.sort: Batcher's recursive sorter.

Main results

• Cslib.BitonicSort.compareLayer_perm, Cslib.BitonicSort.merge_perm, and Cslib.BitonicSort.sort_perm: each stage preserves the multiset of complete records.

References

• K. E. Batcher, Sorting Networks and Their Applications.
• Adapted from MassProduction/SortingSemantics/Defs.lean and MassProduction/SortingSemantics/Internal.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.BitonicSort.arity : ℕ → ℕ

The number of records at a given depth, with a definitional split into two equal halves.

@[simp]

theorem Cslib.BitonicSort.arity_eq_two_pow (depth : ℕ) : arity depth = 2 ^ depth

def Cslib.BitonicSort.IsBitonic {κ : Type u_2} [LinearOrder κ] {n : ℕ} (input : Fin n → κ) : Prop

Four-point lattice invariant for bitonic merge. The four indices are in cyclic order; the two inequalities exclude alternating high and low values.

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

Compare corresponding records in the two halves. Descending order reverses the ascending comparison, so descending ties are exchanged.

def Cslib.BitonicSort.compareLayer.source {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) {n : ℕ} (ascending : Bool) (input : Fin (n + n) → α) : Fin (n + n) → Fin (n + n)

The source position selected by a layer; corresponding positions are exchanged together.

def Cslib.BitonicSort.merge {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) : Bool → (Fin (arity depth) → α) → Fin (arity depth) → α

Merge a bitonic tuple by comparing corresponding halves and recursively merging each half.

def Cslib.BitonicSort.sort {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) : Bool → (Fin (arity depth) → α) → Fin (arity depth) → α

Sort each half in opposite directions, then merge the resulting bitonic tuple.

theorem Cslib.BitonicSort.compareLayer_perm {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) {n : ℕ} (ascending : Bool) (input : Fin (n + n) → α) : (List.ofFn (compareLayer key ascending input)).Perm (List.ofFn input)

A layer preserves the multiset of complete records, even when some keys agree.

theorem Cslib.BitonicSort.merge_perm {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (arity depth) → α) : (List.ofFn (merge key depth ascending input)).Perm (List.ofFn input)

Bitonic merge preserves the multiset of complete records on every input.

theorem Cslib.BitonicSort.sort_perm {α : Type u_1} {κ : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (arity depth) → α) : (List.ofFn (sort key depth ascending input)).Perm (List.ofFn input)

Batcher sorting preserves complete records, not merely their projected keys.