Time-bounded decision on the word RAM

Time bounds and input encodings may depend on word size. A predicate allowed : α → ℕ → Prop selects admissible input/width pairs. WordSizeDependentProgram selects code using only width, with a fixed register count. DecidableInTime requires one instruction-list length bound for all widths. Literal values may depend on width. Code selection and the input encoding are uncharged. UniformDecidableInTime uses one fixed program, which may read the width, branch on it, and have width-dependent execution time.

All contracts are conditional on InputFits. Empty conditions or inputs that never fit can make them vacuous. A logarithmic lower threshold is not an input-fit certificate: word-count size alone does not bound input words. An input-dependent width schedule can communicate advice. No effective code/encoding selection or identification with Turing-machine complexity is asserted.

Main definitions

• WordSizeDependentProgram: code selected by word size, with a fixed register count.
• WordSizeDependentProgram.BoundedCode: one instruction-list length bound for every word size.
• DecidableInTime, UniformDecidableInTime: nonuniform and uniform instruction bounds.
• DecidableInTimeLogWord, UniformDecidableInTimeLogWord: transdichotomous word-size conventions.
• DecidableInO, UniformDecidableInO: asymptotic time with constants shared by all widths.
• LinearTime, PolynomialTime, UniformLinearTime, UniformPolynomialTime: size-based classes.

Main results

• UniformDecidableInTime.decidableInTime: constant families give nonuniform certificates.
• WordSizeDependentProgram.DecidesInTime.mono: increase time and restrict admissible widths.
• WordSizeDependentProgram.DecidesInTime.of_inputFits: discharge input fitting with a certificate.
• LinearTime.polynomialTime, UniformLinearTime.polynomialTime: linear time is polynomial.
• fits_of_lt_pow: polynomially bounded values fit logarithmic words.

References

• T. H. Cormen et al., Introduction to Algorithms
• M. L. Fredman and D. E. Willard, Surpassing the information theoretic bound with fusion trees
• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino; the fixed-program decision predicate is adapted from its accompanying Lean formalization.

Answering a question

def Cslib.WordRAM.Program.Answers {B : Basis} {r : ℕ} (p : Program B r) (w : ℕ) (input : List ℕ) (b : Prop) (time : ℕ) : Prop

p.Answers w input b time: run at word size w on input, the program p halts after at most time instructions with output 1 if b holds and 0 otherwise.

theorem Cslib.WordRAM.Program.Answers.mono {B : Basis} {r : ℕ} {p : Program B r} {w : ℕ} {input : List ℕ} {b : Prop} {time time' : ℕ} (h : p.Answers w input b time) (ht : time ≤ time') : p.Answers w input b time'

A time bound can be increased.

theorem Cslib.WordRAM.Program.Answers.congr {B : Basis} {r : ℕ} {p : Program B r} {w : ℕ} {input : List ℕ} {b b' : Prop} {time : ℕ} (h : p.Answers w input b time) (hb : b ↔ b') : p.Answers w input b' time

theorem Cslib.WordRAM.Program.Answers.mono_width {B : Basis} {r : ℕ} {p : Program B r} {w : ℕ} {input : List ℕ} {b : Prop} {time : ℕ} (hp : ¬p.ReadsWidth) (h : p.Answers w input b time) {w' : ℕ} (hw : w ≤ w') : p.Answers w' input b time

A program that does not read the word size answers in the same way at every larger word size.

Word sizes and program families

def Cslib.WordRAM.logWidth (k n : ℕ) : ℕ

The word size k (⌊log₂ n⌋ + 1), taking one digit at zero.

theorem Cslib.WordRAM.fits_of_lt_pow {k n v : ℕ} (hv : v < (n + 1) ^ k) : Fits (logWidth k n) v

A number below (n + 1) ^ k fits a word of logWidth k n bits.

theorem Cslib.WordRAM.logWidth_mono {k k' n n' : ℕ} (hk : k ≤ k') (hn : n ≤ n') : logWidth k n ≤ logWidth k' n'

theorem Cslib.WordRAM.isBigO_natCast_iff_eventually_le_mul (width bound : ℕ → ℕ) : ((fun (n : ℕ) => ↑(width n)) =O[Filter.atTop] fun (n : ℕ) => ↑(bound n)) ↔ ∃ (k : ℕ), 0 < k ∧ ∀ᶠ (n : ℕ) in Filter.atTop, width n ≤ k * bound n

A big-O bound on a natural-valued width schedule is an eventual upper-width condition with a fixed positive natural multiplier. Swapping width and bound expresses a big-Omega bound, as bound n ≤ k * width n; the reciprocal lower constant need not be integral.

@[reducible, inline]

abbrev Cslib.WordRAM.WordSizeDependentProgram (B : Basis) (r : ℕ) : Type

Code selected using only word size, with a fixed finite register file.

def Cslib.WordRAM.WordSizeDependentProgram.BoundedCode {B : Basis} {r : ℕ} (P : WordSizeDependentProgram B r) : Prop

One instruction-list length bound works at every width. Literal values may depend on width; no computability or construction cost for selecting code is asserted.

def Cslib.WordRAM.WordSizeDependentProgram.const {B : Basis} {r : ℕ} (p : Program B r) : WordSizeDependentProgram B r

The constant family associated to a uniform program.

theorem Cslib.WordRAM.WordSizeDependentProgram.const_boundedCode {B : Basis} {r : ℕ} (p : Program B r) : (const p).BoundedCode

Constant families have bounded code.

def Cslib.WordRAM.WordSizeDependentProgram.DecidesInTime {B : Basis} {r : ℕ} {α : Type u_1} (P : WordSizeDependentProgram B r) (encode : ℕ → α → List ℕ) (A : Set α) (time : α → ℕ → ℕ) (allowed : α → ℕ → Prop) : Prop

A family answers correctly within a width-dependent bound on every admitted fitting input. The raw contract does not impose a code-length bound.

theorem Cslib.WordRAM.WordSizeDependentProgram.DecidesInTime.mono {B : Basis} {r : ℕ} {α : Type u_1} {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {A : Set α} {time time' : α → ℕ → ℕ} {allowed allowed' : α → ℕ → Prop} (h : P.DecidesInTime encode A time allowed) (ht : ∀ (a : α) (w : ℕ), time a w ≤ time' a w) (hw : ∀ (a : α) (w : ℕ), allowed' a w → allowed a w) : P.DecidesInTime encode A time' allowed'

Increase time and restrict admitted input/width pairs.

theorem Cslib.WordRAM.WordSizeDependentProgram.DecidesInTime.of_inputFits {B : Basis} {r : ℕ} {α : Type u_1} {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (h : P.DecidesInTime encode A time allowed) (hi : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a)) (a : α) (w : ℕ) : allowed a w → (P w).Answers w (encode w a) (a ∈ A) (time a w)

A fit certificate removes the conditional input-fit premise.

theorem Cslib.WordRAM.WordSizeDependentProgram.DecidesInTime.at_width {B : Basis} {r : ℕ} {α : Type u_1} {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (h : P.DecidesInTime encode A time allowed) (width : α → ℕ) (hw : ∀ (a : α), allowed a (width a)) (a : α) : InputFits (width a) (encode (width a) a) → (P (width a)).Answers (width a) (encode (width a) a) (a ∈ A) (time a (width a))

Evaluate a family contract along any admitted width schedule.

theorem Cslib.WordRAM.WordSizeDependentProgram.DecidesInTime.recode {B : Basis} {r : ℕ} {α : Type u_1} {β : Type u_2} {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {encode' : ℕ → β → List ℕ} {A' : Set β} {timeB : β → ℕ → ℕ} {allowedB : β → ℕ → Prop} (f : α → β) (hf : ∀ (w : ℕ) (a : α), encode w a = encode' w (f a)) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A') (ht : ∀ (a : α) (w : ℕ), timeB (f a) w ≤ time a w) (hw : ∀ (a : α) (w : ℕ), allowed a w → allowedB (f a) w) (h : P.DecidesInTime encode' A' timeB allowedB) : P.DecidesInTime encode A time allowed

Transfer without a charged conversion when the encoded input words agree.

def Cslib.WordRAM.Program.DecidesInTime {B : Basis} {r : ℕ} {α : Type u_1} (p : Program B r) (encode : ℕ → α → List ℕ) (A : Set α) (time : α → ℕ → ℕ) (allowed : α → ℕ → Prop) : Prop

One fixed program answers correctly at every admitted fitting width. Reading word size is allowed; uniformity concerns code selection, not the runtime or execution path.

def Cslib.WordRAM.DecidableInTime {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (time : α → ℕ → ℕ) (allowed : α → ℕ → Prop) : Prop

Nonuniform decision: width selects code, with one register count and one code-length bound shared by every width. The time bound and encoding may depend on width.

def Cslib.WordRAM.UniformDecidableInTime {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (time : α → ℕ → ℕ) (allowed : α → ℕ → Prop) : Prop

Uniform decision by one fixed program, possibly reading word size.

theorem Cslib.WordRAM.Program.DecidesInTime.mono {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time time' : α → ℕ → ℕ} {allowed allowed' : α → ℕ → Prop} {p : Program B r} (h : p.DecidesInTime encode A time allowed) (ht : ∀ (a : α) (w : ℕ), time a w ≤ time' a w) (hw : ∀ (a : α) (w : ℕ), allowed' a w → allowed a w) : p.DecidesInTime encode A time' allowed'

Increase time and restrict admissible widths for a fixed program.

theorem Cslib.WordRAM.UniformDecidableInTime.decidableInTime {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} (h : UniformDecidableInTime B A encode time allowed) : DecidableInTime B A encode time allowed

A fixed program gives a bounded nonuniform family.

theorem Cslib.WordRAM.DecidableInTime.mono {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time time' : α → ℕ → ℕ} {allowed allowed' : α → ℕ → Prop} (h : DecidableInTime B A encode time allowed) (ht : ∀ (a : α) (w : ℕ), time a w ≤ time' a w) (hw : ∀ (a : α) (w : ℕ), allowed' a w → allowed a w) : DecidableInTime B A encode time' allowed'

Increase time and restrict admitted widths without changing code.

theorem Cslib.WordRAM.UniformDecidableInTime.mono {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time time' : α → ℕ → ℕ} {allowed allowed' : α → ℕ → Prop} (h : UniformDecidableInTime B A encode time allowed) (ht : ∀ (a : α) (w : ℕ), time a w ≤ time' a w) (hw : ∀ (a : α) (w : ℕ), allowed' a w → allowed a w) : UniformDecidableInTime B A encode time' allowed'

Increase time and restrict admitted widths for a uniform certificate.

theorem Cslib.WordRAM.DecidableInTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {encode' : ℕ → β → List ℕ} {A' : Set β} {timeB : β → ℕ → ℕ} {allowedB : β → ℕ → Prop} (f : α → β) (hf : ∀ (w : ℕ) (a : α), encode w a = encode' w (f a)) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A') (ht : ∀ (a : α) (w : ℕ), timeB (f a) w ≤ time a w) (hw : ∀ (a : α) (w : ℕ), allowed a w → allowedB (f a) w) (h : DecidableInTime B A' encode' timeB allowedB) : DecidableInTime B A encode time allowed

Transfer nonuniform decision along a map preserving encoded words.

theorem Cslib.WordRAM.UniformDecidableInTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {encode' : ℕ → β → List ℕ} {A' : Set β} {timeB : β → ℕ → ℕ} {allowedB : β → ℕ → Prop} (f : α → β) (hf : ∀ (w : ℕ) (a : α), encode w a = encode' w (f a)) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A') (ht : ∀ (a : α) (w : ℕ), timeB (f a) w ≤ time a w) (hw : ∀ (a : α) (w : ℕ), allowed a w → allowedB (f a) w) (h : UniformDecidableInTime B A' encode' timeB allowedB) : UniformDecidableInTime B A encode time allowed

Transfer uniform decision along a map preserving encoded words.

The transdichotomous word-size assumption and asymptotic time

def Cslib.WordRAM.DecidableInTimeLogWord {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) (time : α → ℕ → ℕ) : Prop

Nonuniform decision under the transdichotomous word-size assumption: every fitting width above some positive multiple of the logarithmic input size is admitted. This lower threshold is not an input-fit guarantee.

def Cslib.WordRAM.UniformDecidableInTimeLogWord {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) (time : α → ℕ → ℕ) : Prop

Uniform decision under the transdichotomous word-size assumption. The fixed program may read the width and have width-dependent execution time.

theorem Cslib.WordRAM.UniformDecidableInTimeLogWord.decidableInTimeLogWord {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {time : α → ℕ → ℕ} {size : α → ℕ} (h : UniformDecidableInTimeLogWord B A encode size time) : DecidableInTimeLogWord B A encode size time

A uniform logarithmic-threshold certificate is nonuniform as well.

def Cslib.WordRAM.DecidableInO {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) (T : ℕ → ℕ → ℕ) (allowed : α → ℕ → Prop) : Prop

Asymptotic nonuniform time T n w. Correctness holds on every admitted fitting input; one positive constant and one size threshold bound the runtime at all admitted widths.

def Cslib.WordRAM.UniformDecidableInO {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) (T : ℕ → ℕ → ℕ) (allowed : α → ℕ → Prop) : Prop

Uniform asymptotic time, with correctness on all admitted fitting inputs and one eventual runtime estimate shared by every width.

theorem Cslib.WordRAM.UniformDecidableInO.decidableInO {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {allowed : α → ℕ → Prop} {size : α → ℕ} {T : ℕ → ℕ → ℕ} (h : UniformDecidableInO B A encode size T allowed) : DecidableInO B A encode size T allowed

Uniform asymptotic decision implies nonuniform asymptotic decision.

Linear and polynomial time

def Cslib.WordRAM.LinearTime {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) : Prop

Nonuniform linear instruction time above a logarithmic lower threshold. Code length and the time and threshold constants are bounded independently of width.

def Cslib.WordRAM.UniformLinearTime {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) : Prop

Uniform linear instruction time above a logarithmic lower threshold.

def Cslib.WordRAM.PolynomialTime {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) : Prop

Nonuniform polynomial instruction time in size above a logarithmic lower threshold. This does not assert effective code selection or Turing-machine computability.

def Cslib.WordRAM.UniformPolynomialTime {α : Type u_1} (B : Basis) (A : Set α) (encode : ℕ → α → List ℕ) (size : α → ℕ) : Prop

Uniform polynomial instruction time in size above a logarithmic lower threshold.

theorem Cslib.WordRAM.UniformLinearTime.linearTime {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (h : UniformLinearTime B A encode size) : LinearTime B A encode size

Uniform linear time implies nonuniform linear time.

theorem Cslib.WordRAM.UniformPolynomialTime.polynomialTime {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (h : UniformPolynomialTime B A encode size) : PolynomialTime B A encode size

Uniform polynomial time implies nonuniform polynomial time.

theorem Cslib.WordRAM.LinearTime.polynomialTime {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (h : LinearTime B A encode size) : PolynomialTime B A encode size

Linear time is polynomial time, using the same family.

theorem Cslib.WordRAM.UniformLinearTime.polynomialTime {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {A : Set α} {size : α → ℕ} (h : UniformLinearTime B A encode size) : UniformPolynomialTime B A encode size

Uniform linear time is uniform polynomial time, using the same program.

theorem Cslib.WordRAM.LinearTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {A : Set α} {encode' : ℕ → β → List ℕ} {A' : Set β} {size : α → ℕ} {size' : β → ℕ} (f : α → β) (hf : ∀ (w : ℕ) (a : α), encode w a = encode' w (f a)) (hs : ∀ (a : α), size a = size' (f a)) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A') (h : LinearTime B A' encode' size') : LinearTime B A encode size

Linear time transfers without charged conversion when words and sizes agree.

theorem Cslib.WordRAM.UniformLinearTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {A : Set α} {encode' : ℕ → β → List ℕ} {A' : Set β} {size : α → ℕ} {size' : β → ℕ} (f : α → β) (hf : ∀ (w : ℕ) (a : α), encode w a = encode' w (f a)) (hs : ∀ (a : α), size a = size' (f a)) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A') (h : UniformLinearTime B A' encode' size') : UniformLinearTime B A encode size

Uniform linear time transfers when words and sizes agree.

theorem Cslib.WordRAM.PolynomialTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {A : Set α} {encode' : ℕ → β → List ℕ} {A' : Set β} {size : α → ℕ} {size' : β → ℕ} (f : α → β) (hf : ∀ (w : ℕ) (a : α), encode w a = encode' w (f a)) (hs : ∀ (a : α), size a = size' (f a)) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A') (h : PolynomialTime B A' encode' size') : PolynomialTime B A encode size

Polynomial time transfers when words and sizes agree.

theorem Cslib.WordRAM.UniformPolynomialTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {A : Set α} {encode' : ℕ → β → List ℕ} {A' : Set β} {size : α → ℕ} {size' : β → ℕ} (f : α → β) (hf : ∀ (w : ℕ) (a : α), encode w a = encode' w (f a)) (hs : ∀ (a : α), size a = size' (f a)) (hA : ∀ (a : α), a ∈ A ↔ f a ∈ A') (h : UniformPolynomialTime B A' encode' size') : UniformPolynomialTime B A encode size

Uniform polynomial time transfers when words and sizes agree.