Element distinctness in linear time on the word RAM

In the comparison model, deciding whether n numbers are pairwise distinct needs Ω(n log n) comparisons, but on the word RAM numbers are also addresses. When the numbers are below n, a table of n flags decides distinctness in linear time by direct addressing Cormen et al., Section 11.1: allocate the table zeroed, then for each number check its flag, answering no if it is set and setting it otherwise.

Cslib.Algorithms.WordRAM.ElementDistinctness.decidesInTime_nodup formalizes this: on lists of naturals whose entries are below their length n, the compiled decider decides List.Nodup within 16 (n + 1) instructions, the final halt included, at every word size of at least 2 (⌊log₂ n⌋ + 1), with one binary digit at zero. Every instance fits at this threshold (Cslib.Algorithms.WordRAM.ElementDistinctness.inputFits). The decider allocates its table with Cslib.WordRAM.alloc and reads and writes it with Cslib.WordRAM.readAt and Cslib.WordRAM.writeAt; its correctness rests on the loop rule Cslib.WordRAM.ExecWithin.loop_invariant.

Main definitions

• Cslib.Algorithms.WordRAM.ElementDistinctness.decider, Cslib.Algorithms.WordRAM.ElementDistinctness.deciderAdditive: the structured decision procedure over Basis.standard and Basis.additive.
• Cslib.Algorithms.WordRAM.ElementDistinctness.Input: lists whose entries are below their length.

Main results

• Cslib.Algorithms.WordRAM.ElementDistinctness.answers: the decider answers whether its input list has no duplicates within 14 n + 15 instructions.
• Cslib.Algorithms.WordRAM.ElementDistinctness.inputFits: every instance fits at the advertised logarithmic word-size threshold.
• Cslib.Algorithms.WordRAM.ElementDistinctness.decidesInTime_nodup, Cslib.Algorithms.WordRAM.ElementDistinctness.decidesInTime_nodup_additive: the compiled decider decides element distinctness within 16 (n + 1) instructions at every word size of at least 2 (⌊log₂ n⌋ + 1).
• Cslib.Algorithms.WordRAM.ElementDistinctness.uniformLinearTime_nodup, Cslib.Algorithms.WordRAM.ElementDistinctness.uniformLinearTime_nodup_additive: element distinctness for entries below the length is uniformly in linear time over Basis.standard and Basis.additive.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

The program

Register names

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.zero : Fin 12

Register holding 0, as all registers do initially.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.one : Fin 12

Register holding 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.len : Fin 12

Register holding the length n of the input.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.front : Fin 12

The allocation frontier.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.cnt : Fin 12

The number of cells to allocate.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.base : Fin 12

The address n + 1 of the table of flags, just past the input.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.cur : Fin 12

Scratch register of the allocator.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.idx : Fin 12

The address i + 1 of the next input entry l[i].

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.val : Fin 12

The current input entry.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.tmp : Fin 12

Scratch register for table accesses.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.seen : Fin 12

The flag of the current entry.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.ans : Fin 12

The answer.

def Cslib.Algorithms.WordRAM.ElementDistinctness.setup : WordRAM.Code WordRAM.Basis.standard 12

Read the length, allocate a zeroed table of n flags just past the input, and start at the first entry with answer 1.

def Cslib.Algorithms.WordRAM.ElementDistinctness.body : WordRAM.Code WordRAM.Basis.standard 12

Process one entry: if its flag is set, answer 0 and stop; otherwise set its flag and advance.

def Cslib.Algorithms.WordRAM.ElementDistinctness.decider : WordRAM.Code WordRAM.Basis.standard 12

The decision procedure for element distinctness: the answer is left in register ans.

def Cslib.Algorithms.WordRAM.ElementDistinctness.setupAdditive : WordRAM.Code WordRAM.Basis.additive 12

Additive-basis version of setup.

def Cslib.Algorithms.WordRAM.ElementDistinctness.bodyAdditive : WordRAM.Code WordRAM.Basis.additive 12

Additive-basis version of body.

def Cslib.Algorithms.WordRAM.ElementDistinctness.deciderAdditive : WordRAM.Code WordRAM.Basis.additive 12

Additive-basis decision procedure for element distinctness.

@[simp]

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.deciderAdditive_mapOp : WordRAM.Code.mapOp WordRAM.Basis.additiveHomStandard deciderAdditive = decider

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ElementDistinctness.Input : Type

The instances: lists of naturals whose entries are below their length.

Correctness

structure Cslib.Algorithms.WordRAM.ElementDistinctness.Invariant (l : List ℕ) (y : WordRAM.Data 12) : Prop

The loop invariant, after the first t = idx - 1 entries: the input is intact; either no duplicate has been found, the first t entries are distinct and the table flags exactly them, or a duplicate has been found, the answer is 0 and the loop is about to stop.

• one_eq : y.regs Reg.one = 1
• base_eq : y.regs Reg.base = l.length + 1
• idx_pos : 1 ≤ y.regs Reg.idx
• idx_le : y.regs Reg.idx ≤ l.length + 1
• input (j : ℕ) (hj : j < l.length) : y.mem (j + 1) = l[j]
• state : (y.regs Reg.ans = 1 ∧ (List.take (y.regs Reg.idx - 1) l).Nodup ∧ ∀ v < l.length, y.mem (l.length + 1 + v) = if v ∈ List.take (y.regs Reg.idx - 1) l then 1 else 0) ∨ y.regs Reg.ans = 0 ∧ ¬l.Nodup ∧ y.regs Reg.idx = l.length + 1

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.fits_two_mul_add_one {w n : ℕ} (hw : WordRAM.logWidth 2 n ≤ w) : WordRAM.Fits w (2 * n + 1)

Words of twice the number of binary digits of n hold 2 n + 1.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.inputFits {w : ℕ} (a : Input) (hw : WordRAM.logWidth 2 (↑a).length ≤ w) : WordRAM.InputFits w ↑a

Every instance fits at the logarithmic threshold used by the decider, and at every larger word size. Thus the input-fit premise in its uniform decision theorem is always satisfied.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.setup_spec {l : List ℕ} {w : ℕ} (hw : WordRAM.Fits w (2 * l.length + 1)) : ∃ (y : WordRAM.Data 12), WordRAM.ExecWithin w setup (WordRAM.Data.init l) y (4 * l.length + 13) ∧ Invariant l y

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.body_spec {l : List ℕ} {w : ℕ} (hl : ∀ v ∈ l, v < l.length) (hw : WordRAM.Fits w (2 * l.length + 1)) {y : WordRAM.Data 12} (hy : Invariant l y) (hc : (WordRAM.Cond.lt Reg.idx Reg.base).Holds y) : ∃ (y' : WordRAM.Data 12), WordRAM.ExecWithin w body y y' 8 ∧ Invariant l y' ∧ l.length + 1 - y'.regs Reg.idx < l.length + 1 - y.regs Reg.idx

One iteration of the loop takes at most 8 instructions, preserves the invariant, and either processes the next entry or stops.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.exit_spec {l : List ℕ} {y : WordRAM.Data 12} (hy : Invariant l y) (hc : ¬(WordRAM.Cond.lt Reg.idx Reg.base).Holds y) : y.regs Reg.ans ≤ 1 ∧ (y.regs Reg.ans = 1 ↔ l.Nodup)

When the loop stops, the answer is 1 exactly if the input has no duplicates.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.answers {l : List ℕ} {w : ℕ} (hl : ∀ v ∈ l, v < l.length) (hw : WordRAM.Fits w (2 * l.length + 1)) : decider.Answers Reg.ans w l l.Nodup (14 * l.length + 15)

Correctness and running time. On a list whose entries are below its length, at a word size that holds 2 n + 1, the decider leaves in register ans the answer to whether the list has no duplicates, within 14 n + 15 instructions.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.decidesInTime_nodup : (decider.program Reg.ans).DecidesInTime (fun (x : ℕ) (l : Input) => ↑l) {l : Input | (↑l).Nodup} (fun (l : Input) (x : ℕ) => 16 * ((↑l).length + 1)) fun (l : Input) (w : ℕ) => WordRAM.logWidth 2 (↑l).length ≤ w

Element distinctness in linear time. On lists of naturals whose entries are below their length n, the compiled decider decides whether there are no duplicates within 16 (n + 1) instructions, the final halt included, at every word size of at least 2 (⌊log₂ n⌋ + 1).

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.uniformLinearTime_nodup : WordRAM.UniformLinearTime WordRAM.Basis.standard {l : Input | (↑l).Nodup} (fun (x : ℕ) (l : Input) => ↑l) fun (l : Input) => (↑l).length

Element distinctness is uniformly in linear time on the word RAM, for lists whose entries are below their length.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.linearTime_nodup : WordRAM.LinearTime WordRAM.Basis.standard {l : Input | (↑l).Nodup} (fun (x : ℕ) (l : Input) => ↑l) fun (l : Input) => (↑l).length

Element distinctness also has a bounded nonuniform linear-time family.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.decidesInTime_nodup_additive : (deciderAdditive.program Reg.ans).DecidesInTime (fun (x : ℕ) (l : Input) => ↑l) {l : Input | (↑l).Nodup} (fun (l : Input) (x : ℕ) => 16 * ((↑l).length + 1)) fun (l : Input) (w : ℕ) => WordRAM.logWidth 2 (↑l).length ≤ w

Element distinctness in linear time over Basis.additive.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.uniformLinearTime_nodup_additive : WordRAM.UniformLinearTime WordRAM.Basis.additive {l : Input | (↑l).Nodup} (fun (x : ℕ) (l : Input) => ↑l) fun (l : Input) => (↑l).length

Element distinctness is uniformly in linear time over Basis.additive, for lists whose entries are below their length.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.linearTime_nodup_additive : WordRAM.LinearTime WordRAM.Basis.additive {l : Input | (↑l).Nodup} (fun (x : ℕ) (l : Input) => ↑l) fun (l : Input) => (↑l).length

Element distinctness also has a bounded nonuniform linear-time family over Basis.additive.