Word-valued computation by word-RAM program families

The primary computability predicates allow code and constants to depend on word size, with one register count and a uniform bound on program length. Their Uniform counterparts use one program at every width; that program may read the width, branch on it, and have width-dependent execution time. Both permit arbitrary admissible-width conditions, width-dependent input encodings and width-dependent time bounds. Instruction counts include halt. Input placement follows State.init; loading registers and constructing maintained representations must be part of the certified program.

The LogWord wrappers express the transdichotomous assumption: a positive multiple of logWidth 1 (size a), where logWidth k n = k * (Nat.log 2 n + 1), is a lower threshold, independently of input fit. Applications claiming successful execution must supply the separate fit guarantee. Outputs also have to fit, since a machine register returns them. No cost is assigned to the mathematical input encoding, and no conversion to Turing-machine polynomial time is asserted.

Main definitions

• WordSizeDependentProgram.ComputesInTime: a family computes a word-valued function.
• ComputableInTime: existence of a family with bounded program length.
• UniformComputableInTime: existence of one fixed program.
• ComputableInTimeLogWord, UniformComputableInTimeLogWord: transdichotomous word-size wrappers.
• ComputableInPolyTime, UniformComputableInPolyTime: polynomial instruction bounds.

Main results

• UniformComputableInTime.computableInTime: uniform computation gives a bounded-code family.
• Code.computesInTime_program: a structured certificate charges the final halt.
• UniformComputableInPolyTime.of_code: structured execution yields polynomial RAM time.

References

See WordRAM.Time for the transdichotomous word-size convention and its sources.

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

One program returns f a at every admitted fitting width within time a w instructions. The final halt is counted; the mathematical input encoding is a convention.

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

At width w, the selected program computes every admitted fitting input. The selected program depends only on the width, and the running-time bound may depend on both parameters.

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

A width-indexed family with uniformly bounded program length computes the function.

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

One program computes the function uniformly at every admitted fitting width.

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

Computation under the transdichotomous word-size assumption: every fitting width above some positive multiple of the logarithmic input size is admitted.

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

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

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

Correct computation on every admitted fitting input, with an eventual runtime bound using one positive multiplicative constant and one size threshold shared by every admitted width.

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

Uniform asymptotic computation, with constants shared by every admitted width.

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

A bounded-code family computes the function in polynomially many instructions in size a, at every fitting width above a positive logarithmic threshold.

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

A fixed program computes the function in polynomially many instructions in size a, at every fitting width above a positive logarithmic threshold.

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

Increase a fixed program's time bound and restrict its admitted widths.

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

Increase a family's time bound and restrict its admitted widths.

theorem Cslib.WordRAM.Program.ComputesInTime.recode {B : Basis} {r : ℕ} {α : Type u_1} {β : Type u_2} {p : Program B r} {encode : ℕ → α → List ℕ} {encode' : ℕ → β → List ℕ} {time : α → ℕ → ℕ} {time' : β → ℕ → ℕ} {allowed : α → ℕ → Prop} {allowed' : β → ℕ → Prop} {f : α → ℕ} {f' : β → ℕ} (g : α → β) (he : ∀ (w : ℕ) (a : α), encode w a = encode' w (g a)) (hf : ∀ (a : α), f a = f' (g a)) (ht : ∀ (a : α) (w : ℕ), time' (g a) w ≤ time a w) (ha : ∀ (a : α) (w : ℕ), allowed a w → allowed' (g a) w) (h : p.ComputesInTime encode' time' allowed' f') : p.ComputesInTime encode time allowed f

Transfer fixed-program computation along a change of instances.

theorem Cslib.WordRAM.WordSizeDependentProgram.ComputesInTime.recode {B : Basis} {r : ℕ} {α : Type u_1} {β : Type u_2} {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {encode' : ℕ → β → List ℕ} {time : α → ℕ → ℕ} {time' : β → ℕ → ℕ} {allowed : α → ℕ → Prop} {allowed' : β → ℕ → Prop} {f : α → ℕ} {f' : β → ℕ} (g : α → β) (he : ∀ (w : ℕ) (a : α), encode w a = encode' w (g a)) (hf : ∀ (a : α), f a = f' (g a)) (ht : ∀ (a : α) (w : ℕ), time' (g a) w ≤ time a w) (ha : ∀ (a : α) (w : ℕ), allowed a w → allowed' (g a) w) (h : P.ComputesInTime encode' time' allowed' f') : P.ComputesInTime encode time allowed f

Transfer a program family along a change of instances.

theorem Cslib.WordRAM.WordSizeDependentProgram.ComputesInTime.of_inputFits {B : Basis} {r : ℕ} {α : Type u_1} {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (h : P.ComputesInTime encode time allowed f) (hi : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a)) (a : α) (w : ℕ) : allowed a w → ∃ (n : ℕ), Executes w (P w) (State.init (encode w a)) (f a) n ∧ n ≤ time a w

A fit certificate removes the conditional input-fit premise.

theorem Cslib.WordRAM.UniformComputableInTime.computableInTime {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (h : UniformComputableInTime B f encode time allowed) : ComputableInTime B f encode time allowed

A uniform certificate gives a nonuniform certificate using a constant family.

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

Increase an existential family's time bound and restrict its admitted widths.

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

Increase an existential fixed program's time bound and restrict its admitted widths.

theorem Cslib.WordRAM.ComputableInTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {encode' : ℕ → β → List ℕ} {time : α → ℕ → ℕ} {time' : β → ℕ → ℕ} {allowed : α → ℕ → Prop} {allowed' : β → ℕ → Prop} {f : α → ℕ} {f' : β → ℕ} (g : α → β) (he : ∀ (w : ℕ) (a : α), encode w a = encode' w (g a)) (hf : ∀ (a : α), f a = f' (g a)) (ht : ∀ (a : α) (w : ℕ), time' (g a) w ≤ time a w) (ha : ∀ (a : α) (w : ℕ), allowed a w → allowed' (g a) w) (h : ComputableInTime B f' encode' time' allowed') : ComputableInTime B f encode time allowed

Transfer bounded-code computation along an encoding-preserving instance map.

theorem Cslib.WordRAM.UniformComputableInTime.recode {B : Basis} {α : Type u_1} {β : Type u_2} {encode : ℕ → α → List ℕ} {encode' : ℕ → β → List ℕ} {time : α → ℕ → ℕ} {time' : β → ℕ → ℕ} {allowed : α → ℕ → Prop} {allowed' : β → ℕ → Prop} {f : α → ℕ} {f' : β → ℕ} (g : α → β) (he : ∀ (w : ℕ) (a : α), encode w a = encode' w (g a)) (hf : ∀ (a : α), f a = f' (g a)) (ht : ∀ (a : α) (w : ℕ), time' (g a) w ≤ time a w) (ha : ∀ (a : α) (w : ℕ), allowed a w → allowed' (g a) w) (h : UniformComputableInTime B f' encode' time' allowed') : UniformComputableInTime B f encode time allowed

Transfer uniform computation along an encoding-preserving instance map.

theorem Cslib.WordRAM.Program.ComputesInTime.mapOp {B B' : Basis} {r : ℕ} {α : Type u_1} {p : Program B r} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (φ : B.Hom B') (h : p.ComputesInTime encode time allowed f) : (Program.mapOp φ p).ComputesInTime encode time allowed f

Basis translation preserves fixed-program computation with the same instruction count.

theorem Cslib.WordRAM.WordSizeDependentProgram.ComputesInTime.mapOp {B B' : Basis} {r : ℕ} {α : Type u_1} {P : WordSizeDependentProgram B r} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (φ : B.Hom B') (h : P.ComputesInTime encode time allowed f) : (WordSizeDependentProgram.mapOp φ P).ComputesInTime encode time allowed f

Basis translation preserves family computation with the same instruction count.

theorem Cslib.WordRAM.ComputableInTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (φ : B.Hom B') (h : ComputableInTime B f encode time allowed) : ComputableInTime B' f encode time allowed

Computation transfers to a basis implementing the original operations.

theorem Cslib.WordRAM.UniformComputableInTime.mapOp {B B' : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (φ : B.Hom B') (h : UniformComputableInTime B f encode time allowed) : UniformComputableInTime B' f encode time allowed

Uniform computation transfers to a basis implementing the original operations.

theorem Cslib.WordRAM.UniformComputableInTimeLogWord.computableInTimeLogWord {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {size : α → ℕ} {time : α → ℕ → ℕ} {f : α → ℕ} (h : UniformComputableInTimeLogWord B f encode size time) : ComputableInTimeLogWord B f encode size time

Uniform logarithmic-threshold computation gives bounded-code computation.

theorem Cslib.WordRAM.UniformComputableInO.computableInO {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {size : α → ℕ} {T : ℕ → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (h : UniformComputableInO B f encode size T allowed) : ComputableInO B f encode size T allowed

Uniform asymptotic computation gives bounded-code asymptotic computation.

theorem Cslib.WordRAM.UniformComputableInPolyTime.computableInPolyTime {B : Basis} {α : Type u_1} {encode : ℕ → α → List ℕ} {size f : α → ℕ} (h : UniformComputableInPolyTime B f encode size) : ComputableInPolyTime B f encode size

Uniform polynomial computation is a special case of bounded-code polynomial computation.

theorem Cslib.WordRAM.Code.computesInTime_program {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (c : Code B r) (out : Fin r) (h : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a) → ∃ (y : Data r), ExecWithin w c (Data.init (encode w a)) y (time a w) ∧ y.regs out = f a) : (c.program out).ComputesInTime encode (fun (a : α) (w : ℕ) => time a w + 1) allowed f

Structured computation followed by halt gives the same word in one additional instruction.

theorem Cslib.WordRAM.WordSizeDependentProgram.computesInTime_program {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (c : ℕ → Code B r) (out : Fin r) (h : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a) → ∃ (y : Data r), ExecWithin w (c w) (Data.init (encode w a)) y (time a w) ∧ y.regs out = f a) : ComputesInTime (fun (w : ℕ) => (c w).program out) encode (fun (a : α) (w : ℕ) => time a w + 1) allowed f

A width-indexed structured certificate includes one instruction for the final halt.

theorem Cslib.WordRAM.UniformComputableInTime.of_code {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (c : Code B r) (out : Fin r) (h : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a) → ∃ (y : Data r), ExecWithin w c (Data.init (encode w a)) y (time a w) ∧ y.regs out = f a) : UniformComputableInTime B f encode (fun (a : α) (w : ℕ) => time a w + 1) allowed

A structured fixed-program execution certificate yields computation including halt.

theorem Cslib.WordRAM.ComputableInTime.of_code {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {time : α → ℕ → ℕ} {allowed : α → ℕ → Prop} {f : α → ℕ} (c : ℕ → Code B r) (out : Fin r) (hsize : ∃ (L : ℕ), ∀ (w : ℕ), (c w).size ≤ L) (h : ∀ (a : α) (w : ℕ), allowed a w → InputFits w (encode w a) → ∃ (y : Data r), ExecWithin w (c w) (Data.init (encode w a)) y (time a w) ∧ y.regs out = f a) : ComputableInTime B f encode (fun (a : α) (w : ℕ) => time a w + 1) allowed

Structured families with uniformly bounded assembled size yield computation including halt.

theorem Cslib.WordRAM.UniformComputableInPolyTime.of_program {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {size f : α → ℕ} (p : Program B r) {T : ℕ → ℕ} (hT : PolynomiallyBounded T) (k : ℕ) (hk : 0 < k) (h : p.ComputesInTime encode (fun (a : α) (x : ℕ) => T (size a)) (fun (a : α) (w : ℕ) => logWidth k (size a) ≤ w) f) : UniformComputableInPolyTime B f encode size

A supplied polynomial bound for complete flat execution yields a uniform certificate.

theorem Cslib.WordRAM.ComputableInPolyTime.of_family {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {size f : α → ℕ} (P : WordSizeDependentProgram B r) (hP : P.BoundedCode) {T : ℕ → ℕ} (hT : PolynomiallyBounded T) (k : ℕ) (hk : 0 < k) (h : P.ComputesInTime encode (fun (a : α) (x : ℕ) => T (size a)) (fun (a : α) (w : ℕ) => logWidth k (size a) ≤ w) f) : ComputableInPolyTime B f encode size

A supplied polynomial bound and bounded program length yield a family certificate.

theorem Cslib.WordRAM.UniformComputableInPolyTime.of_code {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {size f : α → ℕ} (c : Code B r) (out : Fin r) {T : ℕ → ℕ} (hT : PolynomiallyBounded T) (k : ℕ) (hk : 0 < k) (h : ∀ (a : α) (w : ℕ), logWidth k (size a) ≤ w → InputFits w (encode w a) → ∃ (y : Data r), ExecWithin w c (Data.init (encode w a)) y (T (size a)) ∧ y.regs out = f a) : UniformComputableInPolyTime B f encode size

Structured execution yields uniform polynomial RAM time, including the final halt.

theorem Cslib.WordRAM.ComputableInPolyTime.of_code {B : Basis} {r : ℕ} {α : Type u_1} {encode : ℕ → α → List ℕ} {size f : α → ℕ} (c : ℕ → Code B r) (out : Fin r) (hsize : ∃ (L : ℕ), ∀ (w : ℕ), (c w).size ≤ L) {T : ℕ → ℕ} (hT : PolynomiallyBounded T) (k : ℕ) (hk : 0 < k) (h : ∀ (a : α) (w : ℕ), logWidth k (size a) ≤ w → InputFits w (encode w a) → ∃ (y : Data r), ExecWithin w (c w) (Data.init (encode w a)) y (T (size a)) ∧ y.regs out = f a) : ComputableInPolyTime B f encode size

Bounded structured families yield polynomial RAM time, including the final halt.