Kolmogorov complexity relative to a description method

A description method runs binary programs: M.run p is the computation of the program p, a Mathlib Computation, which may or may not terminate with an object. The computation comes with a clock: (M.run p).runFor t is the output of p after t steps, or none if p has not halted by then. A computation has at most one result, so every program describes at most one object. The plain Kolmogorov complexity M.ecomplexity x of an object x is the length of a shortest program that eventually outputs x, and its time-bounded Kolmogorov complexity M.etimeBoundedComplexity t x is the length of a shortest program that outputs x within t steps Li and Vitányi, Chapters 2 and 7. Both take values in ℕ∞, and are ⊤ when no program describes x; as for cslib's circuit complexity Cslib.Circuits.ecomplexity, the prefix e stands for "extended".

Nothing here depends on a machine model. A multi-tape Turing machine gives a description method (Cslib.Kolmogorov.DescriptionMethod.ofMultiTapeTM), and so does any other model with a clocked semantics. The usual machine-independent complexity is the complexity of a method that simulates every other one with constant program overhead (Cslib.Kolmogorov.DescriptionMethod.Simulation); for the partial recursive description methods, Cslib.Kolmogorov.DescriptionMethod.universal is such a method.

Main definitions

• Cslib.Kolmogorov.DescriptionMethod: binary programs run as computations.
• Cslib.Kolmogorov.DescriptionMethod.Produces: a program eventually outputs an object.
• Cslib.Kolmogorov.DescriptionMethod.ecomplexity: the plain complexity C_M(x).
• Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity: the time-bounded complexity C_M^t(x).
• Cslib.Kolmogorov.DescriptionMethod.complexity: the plain complexity as a natural number, for objects with a description.
• Cslib.Kolmogorov.DescriptionMethod.literal: the method in which every program prints itself.
• Cslib.Kolmogorov.DescriptionMethod.map: pushforward of a description method along f : α → β.

Main results

• Cslib.Kolmogorov.DescriptionMethod.Produces.unique: a program describes at most one object.
• Cslib.Kolmogorov.DescriptionMethod.ecomplexity_le_natCast_iff, Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_le_natCast_iff: the complexity is at most k exactly when some program of length at most k describes the object (within the time bound); the strict versions are ecomplexity_lt_natCast_iff and etimeBoundedComplexity_lt_natCast_iff.
• Cslib.Kolmogorov.DescriptionMethod.exists_length_eq_ecomplexity: a finite complexity is the length of a describing program.
• Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_antitone: more time cannot increase the time-bounded complexity.
• Cslib.Kolmogorov.DescriptionMethod.iInf_etimeBoundedComplexity, Cslib.Kolmogorov.DescriptionMethod.exists_etimeBoundedComplexity_eq_ecomplexity: the plain complexity is the time-bounded complexity for a large enough time bound.
• Cslib.Kolmogorov.DescriptionMethod.ecomplexity_map_le, Cslib.Kolmogorov.DescriptionMethod.ecomplexity_map_eq_of_injective: pushing forward a description method cannot increase complexity and preserves it under injective maps.

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 (α : Type u_1) : Type u_1

A description method for objects of type α: run p is the computation of the binary program p, which may or may not terminate with an object. Its clock is that of the computation: (run p).runFor t is the output of p after t steps, if p has halted by then. This is the clocked analogue of a partial function from programs to objects Li and Vitányi, Chapter 2.

• run : List Bool → Computation α

  The computation of the program p.

def Cslib.Kolmogorov.DescriptionMethod.Produces {α : Type u_1} (M : DescriptionMethod α) (p : List Bool) (x : α) : Prop

The program p eventually outputs x.

noncomputable def Cslib.Kolmogorov.DescriptionMethod.ecomplexity {α : Type u_1} (M : DescriptionMethod α) (x : α) : ℕ∞

The plain Kolmogorov complexity C_M(x) of x: the length of a shortest program that outputs x, or ⊤ if there is none Sipser, Section 6.4.

noncomputable def Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity {α : Type u_1} (M : DescriptionMethod α) (t : ℕ) (x : α) : ℕ∞

The time-bounded Kolmogorov complexity C_M^t(x) of x: the length of a shortest program that outputs x within t steps, or ⊤ if there is none Li and Vitányi, Chapter 7.

noncomputable def Cslib.Kolmogorov.DescriptionMethod.complexity {α : Type u_1} (M : DescriptionMethod α) (x : α) : ℕ

The plain complexity C_M(x) as a natural number. It is 0 for an object without a description, so it is the plain complexity only when M.ecomplexity x ≠ ⊤ (natCast_complexity).

Programs and their outputs

theorem Cslib.Kolmogorov.DescriptionMethod.produces_iff_exists_mem_runFor {α : Type u_1} {M : DescriptionMethod α} {p : List Bool} {x : α} : M.Produces p x ↔ ∃ (t : ℕ), x ∈ (M.run p).runFor t

theorem Cslib.Kolmogorov.DescriptionMethod.Produces.of_mem_runFor {α : Type u_1} {M : DescriptionMethod α} {p : List Bool} {t : ℕ} {x : α} (h : x ∈ (M.run p).runFor t) : M.Produces p x

theorem Cslib.Kolmogorov.DescriptionMethod.eq_of_mem_runFor {α : Type u_1} {M : DescriptionMethod α} {p : List Bool} {x y : α} {t₁ t₂ : ℕ} (hx : x ∈ (M.run p).runFor t₁) (hy : y ∈ (M.run p).runFor t₂) : x = y

Two outputs of the same program, at any two times, are equal.

theorem Cslib.Kolmogorov.DescriptionMethod.Produces.unique {α : Type u_1} {M : DescriptionMethod α} {p : List Bool} {x y : α} (hx : M.Produces p x) (hy : M.Produces p y) : x = y

A program describes at most one object.

Plain complexity

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_le_length {α : Type u_1} {M : DescriptionMethod α} {p : List Bool} {x : α} (h : M.Produces p x) : M.ecomplexity x ≤ ↑p.length

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_lt_iff {α : Type u_1} {M : DescriptionMethod α} {x : α} {r : ℕ∞} : M.ecomplexity x < r ↔ ∃ (p : List Bool), ↑p.length < r ∧ M.Produces p x

The complexity is below r exactly when a program shorter than r describes the object.

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_lt_natCast_iff {α : Type u_1} {M : DescriptionMethod α} {x : α} {k : ℕ} : M.ecomplexity x < ↑k ↔ ∃ (p : List Bool), p.length < k ∧ M.Produces p x

The complexity is below k exactly when a program of length below k describes the object.

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_le_natCast_iff {α : Type u_1} {M : DescriptionMethod α} {x : α} {k : ℕ} : M.ecomplexity x ≤ ↑k ↔ ∃ (p : List Bool), p.length ≤ k ∧ M.Produces p x

Threshold characterization. The complexity is at most k exactly when a program of length at most k describes the object.

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_eq_top_iff {α : Type u_1} {M : DescriptionMethod α} {x : α} : M.ecomplexity x = ⊤ ↔ ∀ (p : List Bool), ¬M.Produces p x

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_ne_top_iff {α : Type u_1} {M : DescriptionMethod α} {x : α} : M.ecomplexity x ≠ ⊤ ↔ ∃ (p : List Bool), M.Produces p x

theorem Cslib.Kolmogorov.DescriptionMethod.natCast_complexity {α : Type u_1} {M : DescriptionMethod α} {x : α} (h : M.ecomplexity x ≠ ⊤) : ↑(M.complexity x) = M.ecomplexity x

theorem Cslib.Kolmogorov.DescriptionMethod.exists_length_eq_ecomplexity {α : Type u_1} {M : DescriptionMethod α} {x : α} (h : M.ecomplexity x ≠ ⊤) : ∃ (p : List Bool), M.Produces p x ∧ ↑p.length = M.ecomplexity x

A finite complexity is the length of a describing program.

Time-bounded complexity

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_le_length {α : Type u_1} {M : DescriptionMethod α} {p : List Bool} {t : ℕ} {x : α} (h : x ∈ (M.run p).runFor t) : M.etimeBoundedComplexity t x ≤ ↑p.length

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_lt_iff {α : Type u_1} {M : DescriptionMethod α} {t : ℕ} {x : α} {r : ℕ∞} : M.etimeBoundedComplexity t x < r ↔ ∃ (p : List Bool), ↑p.length < r ∧ x ∈ (M.run p).runFor t

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_lt_natCast_iff {α : Type u_1} {M : DescriptionMethod α} {t : ℕ} {x : α} {k : ℕ} : M.etimeBoundedComplexity t x < ↑k ↔ ∃ (p : List Bool), p.length < k ∧ x ∈ (M.run p).runFor t

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_le_natCast_iff {α : Type u_1} {M : DescriptionMethod α} {t : ℕ} {x : α} {k : ℕ} : M.etimeBoundedComplexity t x ≤ ↑k ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ (M.run p).runFor t

Threshold characterization. The time-bounded complexity C_M^t(x) is at most k exactly when a program of length at most k outputs x within t steps.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_eq_top_iff {α : Type u_1} {M : DescriptionMethod α} {t : ℕ} {x : α} : M.etimeBoundedComplexity t x = ⊤ ↔ ∀ (p : List Bool), x ∉ (M.run p).runFor t

theorem Cslib.Kolmogorov.DescriptionMethod.exists_length_eq_etimeBoundedComplexity {α : Type u_1} {M : DescriptionMethod α} {t : ℕ} {x : α} (h : M.etimeBoundedComplexity t x ≠ ⊤) : ∃ (p : List Bool), x ∈ (M.run p).runFor t ∧ ↑p.length = M.etimeBoundedComplexity t x

A finite time-bounded complexity is the length of a program outputting the object in time.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_antitone {α : Type u_1} (M : DescriptionMethod α) (x : α) : Antitone fun (x_1 : ℕ) => M.etimeBoundedComplexity x_1 x

Monotonicity in the time bound. More time cannot increase the time-bounded complexity.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_mono {α : Type u_1} {M : DescriptionMethod α} {x : α} {t₁ t₂ : ℕ} (h : t₁ ≤ t₂) : M.etimeBoundedComplexity t₂ x ≤ M.etimeBoundedComplexity t₁ x

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_le_etimeBoundedComplexity {α : Type u_1} (M : DescriptionMethod α) (t : ℕ) (x : α) : M.ecomplexity x ≤ M.etimeBoundedComplexity t x

Dropping the time bound cannot increase the complexity.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_etimeBoundedComplexity_eq_ecomplexity {α : Type u_1} (M : DescriptionMethod α) (x : α) : ∃ (t : ℕ), M.etimeBoundedComplexity t x = M.ecomplexity x

A large enough time bound attains the plain complexity.

theorem Cslib.Kolmogorov.DescriptionMethod.iInf_etimeBoundedComplexity {α : Type u_1} (M : DescriptionMethod α) (x : α) : ⨅ (t : ℕ), M.etimeBoundedComplexity t x = M.ecomplexity x

The plain complexity is the limit of the time-bounded complexities.

The literal description method

def Cslib.Kolmogorov.DescriptionMethod.literal : DescriptionMethod (List Bool)

The description method for binary strings in which every program prints itself, taking one step per bit.

theorem Cslib.Kolmogorov.DescriptionMethod.results_literal_run (p : List Bool) : (literal.run p).Results p p.length

A literal program halts after exactly one step per bit.

theorem Cslib.Kolmogorov.DescriptionMethod.mem_literal_runFor {t : ℕ} {p x : List Bool} : x ∈ (literal.run p).runFor t ↔ p.length ≤ t ∧ p = x

theorem Cslib.Kolmogorov.DescriptionMethod.literal_produces {p x : List Bool} : literal.Produces p x ↔ p = x

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_literal (x : List Bool) : literal.ecomplexity x = ↑x.length

Every string is its own shortest literal description.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_literal {t : ℕ} {x : List Bool} (h : x.length ≤ t) : literal.etimeBoundedComplexity t x = ↑x.length

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_literal_eq_top {t : ℕ} {x : List Bool} (h : t < x.length) : literal.etimeBoundedComplexity t x = ⊤

Mapping outputs

def Cslib.Kolmogorov.DescriptionMethod.map {α : Type u_1} {β : Type u_2} (f : α → β) (M : DescriptionMethod α) : DescriptionMethod β

Mapping a function over the outputs of a description method, taking no steps of its own.

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.runFor_map {α : Type u_1} {β : Type u_2} (f : α → β) (M : DescriptionMethod α) (p : List Bool) (t : ℕ) : ((map f M).run p).runFor t = Option.map f ((M.run p).runFor t)

theorem Cslib.Kolmogorov.DescriptionMethod.mem_map_runFor_iff {α : Type u_1} {β : Type u_2} {f : α → β} {M : DescriptionMethod α} {p : List Bool} {t : ℕ} {y : β} : y ∈ ((map f M).run p).runFor t ↔ ∃ x ∈ (M.run p).runFor t, f x = y

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.map_produces_iff {α : Type u_1} {β : Type u_2} {f : α → β} {M : DescriptionMethod α} {p : List Bool} {y : β} : (map f M).Produces p y ↔ ∃ (x : α), M.Produces p x ∧ f x = y

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_map_le {α : Type u_1} {β : Type u_2} (f : α → β) (M : DescriptionMethod α) (x : α) : (map f M).ecomplexity (f x) ≤ M.ecomplexity x

Mapping f over the outputs does not increase complexity: f x has complexity under M.map f at most that of x under M.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_map_le {α : Type u_1} {β : Type u_2} (f : α → β) (M : DescriptionMethod α) (t : ℕ) (x : α) : (map f M).etimeBoundedComplexity t (f x) ≤ M.etimeBoundedComplexity t x

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_map_eq_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (M : DescriptionMethod α) (x : α) : (map f M).ecomplexity (f x) = M.ecomplexity x

Mapping an injective f over the outputs preserves complexity: f x has the same complexity under M.map f as x under M.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_map_eq_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (M : DescriptionMethod α) (t : ℕ) (x : α) : (map f M).etimeBoundedComplexity t (f x) = M.etimeBoundedComplexity t x