Complexity of Almost Constant Functions

A function f : α → β that is constant except for a finite number of arguments is computable in constant time and zero space: the machine reads the encoded input while remembering the prefix it has seen so far. After a finite number of steps it either reaches the end of the input or a point where the prefix cannot be extended to the encoding of one of the finitely many exceptions. In both cases, it emits the corresponding output one symbol at a time.

This result also holds for functions whose domain is already finite.

Main Results

• encodedComputableInTimeAndSpace_of_finite: Every function on a finite type is computable in constant time and zero space, relative to any encoding.
• encodedComputableInTimeAndSpace_of_exists_finite_ne: Every function that is constant except for a finite number of arguments is computable in constant time and zero space, relative to any encoding.
• encodedComputableInTimeAndSpace_of_const: Every constant function is computable in constant time and zero space, relative to any encoding.
• encodedComputableInTimeAndSpace_almostConstTime and encodedComputableInTimeAndSpace_finiteFunTime: The same with explicit time bounds.

The machine computing a function that is constant outside a finite set

The machine almostConstTM encIn encOut f S out computes f, provided that the encoded output of f is the fixed Boolean string out outside of the finite set S.

def Turing.MultiTapeTM.almostConstTime {α : Type u_1} {β : Type u_2} (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (f : α → β) (S : Finset α) (out : List Bool) : ℕ

A constant time bound for the machine almostConstTM.

Equations

• Turing.MultiTapeTM.almostConstTime encIn encOut f S out = 2 + out.length + S.sup fun (a : α) => (encIn a).length + (encOut (f a)).length

theorem Turing.MultiTapeTM.computableInTimeAndSpace_almostConstTime {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (f : α → β) (S : Finset α) (out : List Bool) (h : ∀ a ∉ S, encOut (f a) = out) : ComputableInTimeAndSpace f encIn encOut (fun (x : α) => almostConstTime encIn encOut f S out) fun (x : α) => 0

Every function whose encoded output is constant outside of a finite set is computable in time almostConstTime and zero space.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_of_exists_finite_ne {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : ∃ (b : β), {a : α | f a ≠ b}.Finite) : ∃ (c : ℕ), ComputableInTimeAndSpace f encIn encOut (fun (x : α) => c) fun (x : α) => 0

Every almost constant function is computable in constant time and zero space.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_of_const {α : Type u_3} {β : Type u_4} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (b : β) : ∃ (c : ℕ), ComputableInTimeAndSpace (Function.const α b) encIn encOut (fun (x : α) => c) fun (x : α) => 0

Every constant function is computable in constant time and zero space.

noncomputable def Turing.MultiTapeTM.finiteFunTime {α : Type u_3} {β : Type u_4} [Finite α] (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (f : α → β) : ℕ

A constant time bound for functions on a finite type.

Equations

• Turing.MultiTapeTM.finiteFunTime encIn encOut f = Turing.MultiTapeTM.almostConstTime encIn encOut f Finset.univ []

theorem Turing.MultiTapeTM.computableInTimeAndSpace_finiteFunTime {α : Type u_3} {β : Type u_4} [Finite α] {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (f : α → β) : ComputableInTimeAndSpace f encIn encOut (fun (x : α) => finiteFunTime encIn encOut f) fun (x : α) => 0

Every function on a finite type is computable in time finiteFunTime and zero space.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_of_finite {α : Type u_3} {β : Type u_4} [Finite α] {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (f : α → β) : ∃ (c : ℕ), ComputableInTimeAndSpace f encIn encOut (fun (x : α) => c) fun (x : α) => 0

Every function on a finite type is computable in constant time and zero space.