Element distinctness on a logarithmic-cost RAM

The bounded-universe direct-addressing algorithm Cormen et al., Section 11.1 uses only the additive-memory fragment of the word RAM. Compiling its fixed twelve-register program with Cslib.WordRAM.ToRAM.paddedProgram gives a natural-number RAM decider with logarithmic cost O((n + 1) (log(n + 1) + 1)).

The prepared program starts from five supplied zero scratch words, a length header and the input. It charges every relocation, clearing, compiler-initialization, simulation and output instruction. Installing this external convention remains uncharged. A second theorem starts directly from the larger padded workspace. The entries must be below the input length; unrestricted element distinctness is outside the statements. The target is the library's natural-number adaptation of Cook and Reckhow, not a Turing-machine theorem. The source word RAM adapts MIT–ULB CompGeom Group.

Main definitions

• Cslib.Algorithms.WordRAM.ElementDistinctness.paddedRamProgram: the fixed compiled decider.
• Cslib.Algorithms.WordRAM.ElementDistinctness.ramProgram: the fixed compiled decider with charged input preparation.

Main results

• Cslib.Algorithms.WordRAM.ElementDistinctness.program_isAdditive: the concrete source program belongs to the compiler's supported fragment.
• Cslib.Algorithms.WordRAM.ElementDistinctness.haltsWithResultInTime_nodup_padded: the compiled decider answers within 2448 (n + 1) (Nat.log 2 (n + 1) + 1) logarithmic cost.
• Cslib.Algorithms.WordRAM.ElementDistinctness.haltsWithResultInTime_nodup: including preparation, the bound is 2735 (n + 1) (Nat.log 2 (n + 1) + 1).

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms
• S. A. Cook and R. A. Reckhow, Time bounded random access machines
• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.program_isAdditive : (decider.program Reg.ans).IsAdditive

Every instruction of the compiled source decider is in the additive-memory fragment, because decider is the image of deciderAdditive under Basis.additiveHomStandard.

def Cslib.Algorithms.WordRAM.ElementDistinctness.paddedRamProgram : RAM.Program

The fixed twelve-register source decider compiled to the natural-number RAM. Its input convention is ToRAM.paddedInput 12, whose supplied zero prefix has length seventeen.

@[simp]

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.paddedRamProgram_eq : paddedRamProgram = WordRAM.ToRAM.paddedProgram (decider.program Reg.ans)

def Cslib.Algorithms.WordRAM.ElementDistinctness.ramProgram : RAM.Program

The fixed compiled decider preceded by charged input relocation and workspace clearing. Its external input convention is RAM.Input.encode 5.

@[simp]

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.ramProgram_eq : ramProgram = WordRAM.ToRAM.preparedProgram (decider.program Reg.ans)

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.haltsWithResultInTime_nodup_padded (a : Input) : RAM.HaltsWithResultInTime RAM.logCost paddedRamProgram (WordRAM.ToRAM.paddedInput 12 ↑a) (if (↑a).Nodup then 1 else 0) (2448 * ((↑a).length + 1) * (Nat.log 2 ((↑a).length + 1) + 1))

Bounded-universe element distinctness has logarithmic RAM cost 2448 (n + 1) (log₂(n + 1) + 1) from the supplied padded-input convention. The constant is not optimized. All source and compiler instructions are charged, but constructing the initial padded list is not included.

theorem Cslib.Algorithms.WordRAM.ElementDistinctness.haltsWithResultInTime_nodup (a : Input) : RAM.HaltsWithResultInTime RAM.logCost ramProgram (RAM.Input.encode 5 ↑a) (if (↑a).Nodup then 1 else 0) (2735 * ((↑a).length + 1) * (Nat.log 2 ((↑a).length + 1) + 1))

Bounded-universe element distinctness has logarithmic RAM cost 2735 (n + 1) (log₂(n + 1) + 1) including input relocation and workspace clearing. The same fixed program handles every input, whose entries must be below its length. Installing the external five-zero prefix, length header and words is uncharged; all instructions are charged.