Invariance

A simulation of a description method M by a description method N compiles every M-program p into an N-program of length at most |p| + c with the same output, and if p halts within t steps, then the compiled program halts within τ |p| t steps. Then N is at most c worse than M: C_N(x) ≤ C_M(x) + c, and a description of length k within time t under M gives a description of length k + c within time τ k t under N, provided the overhead τ is monotone in the program length. This is the invariance theorem of Kolmogorov complexity Li and Vitányi, Chapters 2 and 7, Sipser, Section 6.4, relative to the simulation: a method of a class that simulates every method of the class with constant program overhead is additively optimal for the class, and two additively optimal methods of the class agree up to an additive constant.

For plain complexity only the outputs matter: a compiler that preserves outputs and adds at most c bits is a simulation for some time overhead, because there are finitely many programs of each length (Cslib.Kolmogorov.DescriptionMethod.exists_simulation_of_produces).

Main definitions

• Cslib.Kolmogorov.DescriptionMethod.Simulation: a simulation of M by N with program overhead c and time overhead τ.
• Cslib.Kolmogorov.DescriptionMethod.IsAdditivelyOptimal: a method of a class that is at most a constant worse than every method of the class.

Main results

• Cslib.Kolmogorov.DescriptionMethod.Simulation.ecomplexity_le: C_N(x) ≤ C_M(x) + c.
• Cslib.Kolmogorov.DescriptionMethod.Simulation.etimeBoundedComplexity_le_of_le: if C_M^t(x) ≤ k then C_N^{τ k t}(x) ≤ k + c, for a time overhead monotone in the program length.
• Cslib.Kolmogorov.DescriptionMethod.Simulation.etimeBoundedComplexity_le: C_N^{σ t}(x) ≤ C_M^t(x) + c for a time overhead σ independent of the program.
• Cslib.Kolmogorov.DescriptionMethod.Simulation.etimeBoundedComplexity_le_of_polynomial: the transfer under a polynomial time overhead.
• Cslib.Kolmogorov.DescriptionMethod.exists_simulation_of_produces: an output-preserving compiler is a simulation for some time overhead.
• Cslib.Kolmogorov.DescriptionMethod.IsAdditivelyOptimal.invariance: two additively optimal methods of a class have complexities within an additive constant of each other.

References

• M. Li, P. Vitányi, An Introduction to Kolmogorov Complexity and Its Applications
• M. Sipser, Introduction to the Theory of Computation

structure Cslib.Kolmogorov.DescriptionMethod.Simulation {α : Type u_1} (M N : DescriptionMethod α) (c : ℕ) (τ : ℕ → ℕ → ℕ) : Type

A simulation of the description method M by the description method N, with program overhead c and time overhead τ: a compiler from M-programs to N-programs that adds at most c bits, such that a program halting with output x within t steps compiles to a program halting with output x within τ |p| t steps.

• compile : List Bool → List Bool

  The compiler from M-programs to N-programs.

• length_compile_le (p : List Bool) : (self.compile p).length ≤ p.length + c

  Compiling adds at most c bits.

• mem_runFor_compile {p : List Bool} {t : ℕ} {x : α} : x ∈ (M.run p).runFor t → x ∈ (N.run (self.compile p)).runFor (τ p.length t)

  A compiled program outputs what the original one does, within the time overhead.

def Cslib.Kolmogorov.DescriptionMethod.Simulation.refl {α : Type u_1} (M : DescriptionMethod α) : M.Simulation M 0 fun (x t : ℕ) => t

Every description method simulates itself.

def Cslib.Kolmogorov.DescriptionMethod.Simulation.mono {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} {τ : ℕ → ℕ → ℕ} (S : M.Simulation N c τ) {c' : ℕ} {τ' : ℕ → ℕ → ℕ} (hc : c ≤ c') (hτ : ∀ (n t : ℕ), τ n t ≤ τ' n t) : M.Simulation N c' τ'

A simulation with larger overheads.

def Cslib.Kolmogorov.DescriptionMethod.Simulation.trans {α : Type u_1} {M N P : DescriptionMethod α} {c d : ℕ} {τ σ : ℕ → ℕ → ℕ} (S : M.Simulation N c τ) (T : N.Simulation P d σ) (hσ : ∀ (t : ℕ), Monotone fun (x : ℕ) => σ x t) : M.Simulation P (c + d) fun (n t : ℕ) => σ (n + c) (τ n t)

Simulations compose, provided the second time overhead is monotone in the program length.

def Cslib.Kolmogorov.DescriptionMethod.Simulation.map {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} {τ : ℕ → ℕ → ℕ} {β : Type u_2} (f : α → β) (S : M.Simulation N c τ) : (DescriptionMethod.map f M).Simulation (DescriptionMethod.map f N) c τ

Mapping a function over the outputs of a simulation.

theorem Cslib.Kolmogorov.DescriptionMethod.Simulation.produces_compile {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} {τ : ℕ → ℕ → ℕ} (S : M.Simulation N c τ) {p : List Bool} {x : α} (h : M.Produces p x) : N.Produces (S.compile p) x

theorem Cslib.Kolmogorov.DescriptionMethod.Simulation.ecomplexity_le {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} {τ : ℕ → ℕ → ℕ} (S : M.Simulation N c τ) (x : α) : N.ecomplexity x ≤ M.ecomplexity x + ↑c

Invariance. A method that simulates M with program overhead c is at most c worse than M.

theorem Cslib.Kolmogorov.DescriptionMethod.Simulation.etimeBoundedComplexity_le_of_le {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} {τ : ℕ → ℕ → ℕ} (S : M.Simulation N c τ) {t k : ℕ} {x : α} (hτ : Monotone fun (x : ℕ) => τ x t) (h : M.etimeBoundedComplexity t x ≤ ↑k) : N.etimeBoundedComplexity (τ k t) x ≤ ↑(k + c)

Time-bounded invariance. If M describes x with at most k bits within t steps, then N describes x with at most k + c bits within τ k t steps, for a time overhead τ monotone in the program length.

theorem Cslib.Kolmogorov.DescriptionMethod.Simulation.etimeBoundedComplexity_le {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} {σ : ℕ → ℕ} (S : M.Simulation N c fun (x t : ℕ) => σ t) (t : ℕ) (x : α) : N.etimeBoundedComplexity (σ t) x ≤ M.etimeBoundedComplexity t x + ↑c

Time-bounded invariance for a time overhead σ that does not depend on the program: C_N^{σ t}(x) ≤ C_M^t(x) + c.

theorem Cslib.Kolmogorov.DescriptionMethod.Simulation.etimeBoundedComplexity_le_of_polynomial {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} {τ : ℕ → ℕ → ℕ} (S : M.Simulation N c τ) {a e : ℕ} (hτ : ∀ (n t : ℕ), τ n t ≤ a * (n + t + 1) ^ e) {t k : ℕ} {x : α} (h : M.etimeBoundedComplexity t x ≤ ↑k) : N.etimeBoundedComplexity (a * (k + t + 1) ^ e) x ≤ ↑(k + c)

Time-bounded invariance under a polynomial time overhead. If the compiled programs run in time at most a (|p| + t + 1) ^ e, a description of x by M with at most k bits within t steps gives one by N with at most k + c bits within a (k + t + 1) ^ e steps.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_simulation_of_produces {α : Type u_1} {M N : DescriptionMethod α} {c : ℕ} (compile : List Bool → List Bool) (hlen : ∀ (p : List Bool), (compile p).length ≤ p.length + c) (h : ∀ {p : List Bool} {x : α}, M.Produces p x → N.Produces (compile p) x) : ∃ (τ : ℕ → ℕ → ℕ), Nonempty (M.Simulation N c τ)

A compiler that preserves outputs and adds at most c bits is a simulation for some time overhead: there are finitely many programs of each length, so the halting times of the compiled programs of a given length are bounded. The time overhead is not explicit, so this is useful for plain complexity only.

Additive optimality

structure Cslib.Kolmogorov.DescriptionMethod.IsAdditivelyOptimal {α : Type u_1} (U : DescriptionMethod α) (𝓜 : Set (DescriptionMethod α)) : Prop

The description method U is additively optimal for the class 𝓜 of description methods Li and Vitányi, Section 2.1: U belongs to the class, and for every method M of the class, U is at most a constant worse than M.

• mem : U ∈ 𝓜

  The optimal method belongs to the class.

• exists_ecomplexity_le (M : DescriptionMethod α) : M ∈ 𝓜 → ∃ (c : ℕ), ∀ (x : α), U.ecomplexity x ≤ M.ecomplexity x + ↑c

  The optimal method is at most a constant worse than every method of the class.

theorem Cslib.Kolmogorov.DescriptionMethod.isAdditivelyOptimal_of_simulation {α : Type u_1} {U : DescriptionMethod α} {𝓜 : Set (DescriptionMethod α)} (hU : U ∈ 𝓜) (h : ∀ M ∈ 𝓜, ∃ (c : ℕ) (τ : ℕ → ℕ → ℕ), Nonempty (M.Simulation U c τ)) : U.IsAdditivelyOptimal 𝓜

A method of a class that simulates every method of the class, each with a constant program overhead, is additively optimal for the class.

theorem Cslib.Kolmogorov.DescriptionMethod.IsAdditivelyOptimal.invariance {α : Type u_1} {U V : DescriptionMethod α} {𝓜 : Set (DescriptionMethod α)} (hU : U.IsAdditivelyOptimal 𝓜) (hV : V.IsAdditivelyOptimal 𝓜) : ∃ (c : ℕ), ∀ (x : α), U.ecomplexity x ≤ V.ecomplexity x + ↑c ∧ V.ecomplexity x ≤ U.ecomplexity x + ↑c

Invariance theorem Li and Vitányi, Section 2.1. Two additively optimal methods of a class have complexities within an additive constant of each other.