Partial recursive description methods and the invariance theorem

A code c of a partial recursive function (Mathlib's Nat.Partrec.Code) gives a description method ofCode c for natural numbers: a program p is the input encode p of c, and after t steps its output is Nat.Partrec.Code.evaln t c (encode p), the result of evaluating c with fuel t. More generally, a description method is partial recursive (IsPartrec) when a partial recursive function of the programs has exactly its outputs, whatever its clock.

The universal description method universal reads a program as the self-delimiting code of the binary representation of encode c, for a code c, followed by a program p, and runs p under ofCode c, with the same clock. The header of c costs a constant number of bits, so universal is at most a constant worse than ofCode c (ecomplexity_universal_le). It is itself partial recursive, since the decoder of the self-delimiting code is primitive recursive and evaluating codes is partial recursive (Nat.Partrec.Code.eval_part), and every partial recursive method has the outputs of some ofCode c. So universal is additively optimal for the class of partial recursive description methods: this is the invariance theorem of Kolmogorov complexity Li and Vitányi, Section 2.1, and by Cslib.Kolmogorov.DescriptionMethod.IsAdditivelyOptimal.invariance any two additively optimal partial recursive methods have complexities within an additive constant of each other. Every natural number has a description under universal, so its complexity is a natural number (natCast_complexity_universal).

The simulation of ofCode c by universal has no time overhead, which gives the time-bounded invariance C_U^t(x) ≤ C_{ofCode c}^t(x) + |header c| (etimeBoundedComplexity_universal_le). Its clock, however, is the fuel of evaln, which bounds the depth of the evaluation and the size of the numbers it inspects rather than counting the steps of a machine; time-bounded complexity for a machine model needs a universal machine for that model.

Main definitions

• Cslib.Kolmogorov.DescriptionMethod.ofCode: the description method of a code.
• Cslib.Kolmogorov.DescriptionMethod.IsPartrec: partial recursive description methods.
• Cslib.Kolmogorov.DescriptionMethod.codeHeader: the header announcing a code.
• Cslib.Kolmogorov.DescriptionMethod.universal: the universal description method.
• Cslib.Kolmogorov.DescriptionMethod.universalSimulation: the simulation of ofCode c by universal.

Main results

• Cslib.Kolmogorov.DescriptionMethod.ofCode_produces_iff: ofCode c describes x by p exactly when c outputs x on encode p.
• Cslib.Kolmogorov.primrec_decodeSelfDelimiting: the decoder of the self-delimiting code is primitive recursive.
• Cslib.Kolmogorov.DescriptionMethod.isPartrec_universal: the universal method is partial recursive.
• Cslib.Kolmogorov.DescriptionMethod.isAdditivelyOptimal_universal: the invariance theorem.
• Cslib.Kolmogorov.DescriptionMethod.IsPartrec.of_partrec_eval, Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_of_partrec_eval: generic partial-recursiveness and additive-optimality bridges for description methods with a Partrec evaluation function.
• Cslib.Kolmogorov.DescriptionMethod.ecomplexity_universal_le, Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_universal_le: the constant is the length of the header.

References

• M. Li, P. Vitányi, An Introduction to Kolmogorov Complexity and Its Applications

theorem Cslib.Kolmogorov.primrec_decodeSelfDelimiting : Primrec decodeSelfDelimiting

The decoder of the self-delimiting code is primitive recursive.

The description method of a code

def Cslib.Kolmogorov.DescriptionMethod.ofCode (c : Nat.Partrec.Code) : DescriptionMethod ℕ

The description method of the code c of a partial recursive function: the program p is the input encode p of c, and after t steps its output is Code.evaln t c (encode p), the result of evaluating c with fuel t.

theorem Cslib.Kolmogorov.DescriptionMethod.mem_ofCode_runFor {c : Nat.Partrec.Code} {p : List Bool} {t x : ℕ} : x ∈ ((ofCode c).run p).runFor t ↔ x ∈ Nat.Partrec.Code.evaln t c (Encodable.encode p)

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.ofCode_produces_iff {c : Nat.Partrec.Code} {p : List Bool} {x : ℕ} : (ofCode c).Produces p x ↔ x ∈ c.eval (Encodable.encode p)

A program describes x under ofCode c exactly when c outputs x on its encoding.

Partial recursive description methods

def Cslib.Kolmogorov.DescriptionMethod.IsPartrec (M : DescriptionMethod ℕ) : Prop

A description method for natural numbers is partial recursive when a partial recursive function of the programs has exactly its outputs. Nothing is assumed about its clock.

theorem Cslib.Kolmogorov.DescriptionMethod.isPartrec_ofCode (c : Nat.Partrec.Code) : (ofCode c).IsPartrec

theorem Cslib.Kolmogorov.DescriptionMethod.IsPartrec.exists_produces_iff {M : DescriptionMethod ℕ} (h : M.IsPartrec) : ∃ (c : Nat.Partrec.Code), ∀ (p : List Bool) (x : ℕ), M.Produces p x ↔ (ofCode c).Produces p x

A partial recursive description method has the outputs of the description method of some code.

theorem Cslib.Kolmogorov.DescriptionMethod.IsPartrec.of_partrec_eval {α : Type u_1} [Primcodable α] {M : DescriptionMethod α} {eval : List Bool →. α} (heval : Partrec eval) (hprod : ∀ (p : List Bool) (x : α), M.Produces p x ↔ x ∈ eval p) {dec : α → ℕ} (hdec : Computable dec) : (map dec M).IsPartrec

If M : DescriptionMethod α has a partial recursive evaluation function eval : List Bool →. α characterizing M.Produces, then mapping any computable decoder dec : α → ℕ over M yields a partial recursive description method.

The universal description method

def Cslib.Kolmogorov.DescriptionMethod.codeHeader (c : Nat.Partrec.Code) : List Bool

The header announcing the code c to the universal method: the self-delimiting code of the binary representation of encode c.

theorem Cslib.Kolmogorov.DescriptionMethod.length_codeHeader (c : Nat.Partrec.Code) : (codeHeader c).length = (Encodable.encode c).size + (2 * (Encodable.encode c).size.size + 1)

def Cslib.Kolmogorov.DescriptionMethod.universal : DescriptionMethod ℕ

The universal description method: the decoder of the self-delimiting code splits a program into the binary representation of a number n and a program p (decodeSelfDelimiting), and p runs under the description method of the code ofNat Code n, with the same clock.

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.universal_run_codeHeader_append (c : Nat.Partrec.Code) (p : List Bool) : universal.run (codeHeader c ++ p) = (ofCode c).run p

theorem Cslib.Kolmogorov.DescriptionMethod.universal_produces_codeHeader_append {c : Nat.Partrec.Code} {p : List Bool} {x : ℕ} : universal.Produces (codeHeader c ++ p) x ↔ (ofCode c).Produces p x

theorem Cslib.Kolmogorov.DescriptionMethod.isPartrec_universal : universal.IsPartrec

The universal description method is partial recursive.

def Cslib.Kolmogorov.DescriptionMethod.universalSimulation (c : Nat.Partrec.Code) : (ofCode c).Simulation universal (codeHeader c).length fun (x t : ℕ) => t

The universal method simulates the description method of every code c, with the header of c as program overhead and no time overhead.

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_universal_le (c : Nat.Partrec.Code) (x : ℕ) : universal.ecomplexity x ≤ (ofCode c).ecomplexity x + ↑(codeHeader c).length

Invariance: the universal method is at most |codeHeader c| worse than the description method of the code c.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_universal_le (c : Nat.Partrec.Code) (t x : ℕ) : universal.etimeBoundedComplexity t x ≤ (ofCode c).etimeBoundedComplexity t x + ↑(codeHeader c).length

Time-bounded invariance for the clock of evaln: the universal method is at most |codeHeader c| worse than the description method of the code c, within the same fuel.

theorem Cslib.Kolmogorov.DescriptionMethod.isAdditivelyOptimal_universal : universal.IsAdditivelyOptimal {M : DescriptionMethod ℕ | M.IsPartrec}

Invariance theorem Li and Vitányi, Section 2.1. The universal method is additively optimal for the class of partial recursive description methods: it is partial recursive, and at most a constant worse than every partial recursive description method.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_of_partrec_eval {α : Type u_1} [Primcodable α] {M : DescriptionMethod α} {eval : List Bool →. α} (heval : Partrec eval) (hprod : ∀ (p : List Bool) (x : α), M.Produces p x ↔ x ∈ eval p) {dec : α → ℕ} (hdec : Computable dec) : ∃ (c : ℕ), ∀ (x : α), universal.ecomplexity (dec x) ≤ M.ecomplexity x + ↑c

If M : DescriptionMethod α has a partial recursive evaluation function eval : List Bool →. α characterizing M.Produces, then for every computable decoder dec : α → ℕ, universal is at most an additive constant worse than M.

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_universal_ne_top (x : ℕ) : universal.ecomplexity x ≠ ⊤

Every natural number has a description under the universal method.

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.natCast_complexity_universal (x : ℕ) : ↑(universal.complexity x) = universal.ecomplexity x