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.Reg.zero, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.one, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.len, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.front, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.cnt, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.base, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.cur, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.idx, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.val, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.tmp, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.seen, Cslib.Algorithms.WordRAM.ElementDistinctness.Reg.ans: the twelve register names.
• Cslib.Algorithms.WordRAM.ElementDistinctness.setup, Cslib.Algorithms.WordRAM.ElementDistinctness.body, Cslib.Algorithms.WordRAM.ElementDistinctness.decider, Cslib.Algorithms.WordRAM.ElementDistinctness.setupAdditive, Cslib.Algorithms.WordRAM.ElementDistinctness.bodyAdditive, Cslib.Algorithms.WordRAM.ElementDistinctness.deciderAdditive: the structured decision procedure and its setup and loop body 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

Mapping additive-basis operations to the standard basis recovers decider.

@[reducible, inline]

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

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

Correctness

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.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.