Kolmogorov complexity

Algorithmic information content of individual strings: universal description methods, incompressible strings, non-computability and upper semicomputability of Kolmogorov complexity.

DefinitionRunning a program on a binary string#✓fully proved

For a code \(c\) of a partial recursive function on the natural numbers and a binary string \(w\), running \(c\) on \(w\) evaluates \(c\) at the number encoding \(w\); if this halts with output \(m\), the result is the binary string encoded by \(m\). The result is undefined when the evaluation does not halt or \(m\) encodes no binary string.

def run (c : Code) (w : List Bool) : Part (List Bool) :=
  (c.eval (encode w)).bind fun n ↦ Part.ofOption (decode n)
Used by 8
Used byOptimality (the invariance theorem) · Shortest descriptions exist · Every partial recursive description method has a code · Kolmogorov complexity · A description bounds the complexity · Complexity is at most the length plus a constant · The universal description method is partial recursive · The universal description method

DefinitionDescription of a code running on an input#✓fully proved

Let \(c\) be a code for a partial recursive function and let \(n\) be its number in the standard encoding of codes as natural numbers. For a binary string \(w\), the description of \(c\) running on \(w\) is the binary string \(1^n 0 w\), that is, \(n\) ones, then a zero, then \(w\).

def describe (c : Code) (w : List Bool) : List Bool :=
  List.replicate (encode c) true ++ false :: w
Used by 5
Used byOptimality (the invariance theorem) · Shortest descriptions exist · Kolmogorov complexity · A description bounds the complexity · Complexity is at most the length plus a constant

DefinitionThe universal description method#✓fully proved

A description 1ⁿ 0 w runs code number n on w; a string of 1s describes nothing.

def U (p : List Bool) : Part (List Bool) :=
  (Part.ofOption (p.dropWhile id).head?).bind fun _ ↦
    run (ofNat Code (p.takeWhile id).length) (p.dropWhile id).tail
Uses 1 · Used by 14
Statement usesRunning a program on a binary string
Used byOptimality (the invariance theorem) · Shortest descriptions exist · Few strings have small complexity · Kolmogorov complexity · Concatenation costs at most twice the first part · Doubling costs a constant · A description bounds the complexity · Complexity is at most the length plus a constant · Reading pair descriptions · The universal description method is partial recursive · A partial recursive map raises complexity by at most a constant · Shortest descriptions are incompressible · Kolmogorov complexity is upper semicomputable · The description relation is recognizable

DefinitionKolmogorov complexity#✓fully proved

The Kolmogorov complexity \(K(x)\) of a binary string \(x\) is the least length of a binary string \(p\) such that \(U(p)\) is defined and equals \(x\), where \(U\) is the universal description method.

noncomputable def K (x : List Bool) : ℕ :=
  Nat.find (⟨_, (exists_mem_U x).choose, rfl, (exists_mem_U x).choose_spec⟩ :
    ∃ n, ∃ p : List Bool, p.length = n ∧ x ∈ U p)
Uses 3 · Used by 19
Statement usesThe universal description method · Description of a code running on an input · Running a program on a binary string
Used byOptimality (the invariance theorem) · Shortest descriptions exist · Most strings are incompressible · Few strings have small complexity · Incompressible strings exist at every length · Kolmogorov complexity is not computable · Concatenation costs at most twice the first part · Doubling costs a constant · A description bounds the complexity · Complexity is at most the length plus a constant · A computable lower bound of Kolmogorov complexity is bounded · Chaitin's incompleteness theorem · A partial recursive map raises complexity by at most a constant · Shortest descriptions are incompressible · The incompressible strings are not decidable · The incompressible strings are not recognizable · Kolmogorov complexity is not lower semicomputable · No recognizable set with arbitrarily long members consists of incompressible strings · Kolmogorov complexity is upper semicomputable

TheoremA description bounds the complexity#✓fully proved

Let \(x\) and \(p\) be binary strings such that \(U(p)\) is defined and equals \(x\), where \(U\) is the universal description method. Then the Kolmogorov complexity of \(x\) is at most the length of \(p\): \(K(x) \le |p|\).

theorem K_le {x p : List Bool} (h : x ∈ U p) : K x ≤ p.length
Uses 4 · Used by 3
Statement usesKolmogorov complexity · The universal description method
Proof usesDescription of a code running on an input · Running a program on a binary string
Used byOptimality (the invariance theorem) · Complexity is at most the length plus a constant · Kolmogorov complexity is upper semicomputable

TheoremShortest descriptions exist#✓fully proved

For every binary string \(x\) there is a binary string \(p\) whose length is the Kolmogorov complexity \(K(x)\) and such that \(U(p)\) is defined and equals \(x\), where \(U\) is the universal description method.

theorem exists_length_eq_K (x : List Bool) : ∃ p : List Bool, p.length = K x ∧ x ∈ U p
Uses 4 · Used by 5
Statement usesKolmogorov complexity · The universal description method
Proof usesDescription of a code running on an input · Running a program on a binary string
Used byFew strings have small complexity · Concatenation costs at most twice the first part · Doubling costs a constant · A partial recursive map raises complexity by at most a constant · Kolmogorov complexity is upper semicomputable

TheoremComplexity is at most the length plus a constant#✓fully proved

There is a natural number \(c\) such that every binary string \(x\) satisfies \(K(x) \le |x| + c\), where \(K(x)\) is the Kolmogorov complexity of \(x\) and \(|x|\) is its length.

theorem K_le_length_add : ∃ c, ∀ x : List Bool, K x ≤ x.length + c
Uses 5
Statement usesKolmogorov complexity
Proof usesA description bounds the complexity · The universal description method · Description of a code running on an input · Running a program on a binary string

TheoremThe universal description method is partial recursive#✓fully proved

The universal description method, as a partial function from binary strings to binary strings, is partial recursive.

theorem partrec_U : Partrec U
Uses 2 · Used by 5
Statement usesThe universal description method
Proof usesRunning a program on a binary string
Used byConcatenation costs at most twice the first part · Doubling costs a constant · A partial recursive map raises complexity by at most a constant · Shortest descriptions are incompressible · The description relation is recognizable

TheoremEvery partial recursive description method has a code#✓fully proved

Let \(D\) be a partial recursive function from binary strings to binary strings. Then there is a code \(c\) for a partial recursive function such that running \(c\) equals \(D\) as a partial function: for every binary string \(w\), running \(c\) on \(w\) is defined exactly when \(D(w)\) is, and then has the same value.

theorem exists_run_eq {D : List Bool →. List Bool} (hD : Partrec D) : ∃ c : Code, run c = D
Uses 1 · Used by 1
Statement usesRunning a program on a binary string
Used byOptimality (the invariance theorem)

TheoremOptimality (the invariance theorem)#✓fully proved

Let \(D\) be a partial recursive function from binary strings to binary strings, viewed as a description method. Then there is a natural number \(c\) such that for all binary strings \(x\) and \(p\) for which \(D(p)\) is defined and equals \(x\), the Kolmogorov complexity of \(x\) satisfies \(K(x) \le |p| + c\), where \(|p|\) is the length of \(p\).

theorem exists_K_le_of_partrec {D : List Bool →. List Bool} (hD : Partrec D) :
    ∃ c, ∀ x p : List Bool, x ∈ D p → K x ≤ p.length + c
Uses 6 · Used by 5
Statement usesKolmogorov complexity
Proof usesA description bounds the complexity · The universal description method · Description of a code running on an input · Every partial recursive description method has a code · Running a program on a binary string
Used byKolmogorov complexity is not computable · Concatenation costs at most twice the first part · Doubling costs a constant · Chaitin's incompleteness theorem · A partial recursive map raises complexity by at most a constant

TheoremDoubling costs a constant#✓fully proved

There is a natural number \(c\) such that for every binary string \(x\), the Kolmogorov complexity of the concatenation \(xx\) of \(x\) with itself satisfies \(K(xx) \le K(x) + c\).

theorem K_append_self_le : ∃ c, ∀ x : List Bool, K (x ++ x) ≤ K x + c
Uses 5
Statement usesKolmogorov complexity
Proof usesThe universal description method · Optimality (the invariance theorem) · Shortest descriptions exist · The universal description method is partial recursive

DefinitionPair description#✓fully proved

For binary strings \(p\) and \(q\), the pair description of \(p\) and \(q\) is the binary string \(1^{|p|} 0 p q\), that is, \(|p|\) ones, where \(|p|\) is the length of \(p\), then a zero, then \(p\), then \(q\).

The prefix \(1^{|p|} 0\) records the length of \(p\), so the string splits back into \(p\) and \(q\).

def pairDescribe (p q : List Bool) : List Bool := List.replicate p.length true ++ false :: (p ++ q)
Used by 1
Used byConcatenation costs at most twice the first part

DefinitionReading pair descriptions#✓fully proved

Write a binary string \(s\) as \(1^n s'\), where \(n\) is the number of leading \(1\)s, and let \(r\) be \(s'\) without its first letter (\(r\) is empty when \(s'\) is). Let \(r_1\) be the first \(\min(n, |r|)\) letters of \(r\) and \(r_2\) the remaining ones. The pair reader maps \(s\) to the concatenation \(U(r_1)\,U(r_2)\), where \(U\) is the universal description method, and is undefined when \(U(r_1)\) or \(U(r_2)\) is undefined. On a pair description \(1^n 0 r\) with \(|r| \ge n\), this is the concatenation of what the first \(n\) letters of \(r\) and the rest describe.

def pairU (s : List Bool) : Part (List Bool) :=
  (U (((s.dropWhile id).tail).take (s.takeWhile id).length)).bind fun x ↦
    (U (((s.dropWhile id).tail).drop (s.takeWhile id).length)).map fun y ↦ x ++ y
Uses 1 · Used by 1
Statement usesThe universal description method
Used byConcatenation costs at most twice the first part

TheoremConcatenation costs at most twice the first part#✓fully proved

There is a natural number \(c\) such that for all binary strings \(x\) and \(y\), the Kolmogorov complexity of their concatenation \(xy\) satisfies \(K(xy) \le 2K(x) + K(y) + c\).

theorem K_append_le : ∃ c, ∀ x y : List Bool, K (x ++ y) ≤ 2 * K x + K y + c
Uses 7
Statement usesKolmogorov complexity
Proof usesThe universal description method · Optimality (the invariance theorem) · Shortest descriptions exist · Pair description · Reading pair descriptions · The universal description method is partial recursive
14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.