InformationTheory.Shannon.Kolmogorov.UniversalMachine

Imports 5

A length-additive universal machine for plain Kolmogorov complexity #

Programs are bit strings (List Bool) and their length is List.length, so concatenating a fixed prefix is length-additive with no edge cases (unlike the binary length Nat.size of a natural number, which loses leading zeros).

The fixed universal machine universalEval parses a program in two modes:

literal false :: bs — outputs decodeNat bs, so the echo program false :: encodeNat x describes x in natLen x + 1 bits. This gives the C(x) ≤ natLen x + O(1) upper bound and, being total, makes the defining set of condComplexity nonempty (so the infimum is attained).
interpret true :: unary(idx) ++ [false] ++ q — runs eval (ofNat Code idx) (Nat.pair (decodeNat q) y), delegating to Mathlib's universal interpreter Nat.Partrec.Code.eval. Prepending the fixed selector for a machine's code index costs a constant number of bits, which yields the invariance theorem.

Main definitions #

universalEval — the fixed universal machine.
condComplexity / complexity — conditional / plain Kolmogorov complexity.

def

InformationTheory.Kolmogorov.parseUnary

source

List Bool → ℕ × List Bool

Read a leading run of trues (a unary natural number) terminated by the first false, returning the count together with the remaining bits.

Equations

InformationTheory.Kolmogorov.parseUnary [] = (0, [])
InformationTheory.Kolmogorov.parseUnary (false :: rest) = (0, rest)
InformationTheory.Kolmogorov.parseUnary (true :: rest) = ((InformationTheory.Kolmogorov.parseUnary rest).1 + 1, (InformationTheory.Kolmogorov.parseUnary rest).2)

Instances For

Used by

def

InformationTheory.Kolmogorov.literalProg

source

(x : ℕ) :

List Bool

The echo program describing x: flag bit false followed by the binary digits of x.

Equations

InformationTheory.Kolmogorov.literalProg x = false :: Computability.encodeNat x

Instances For

Used by

def

InformationTheory.Kolmogorov.interpretProg

source

(idx : ℕ) (q : List Bool) :

List Bool

The interpretation program for code index idx running on the description q: flag bit true, then idx in unary terminated by false, then q.

Equations

InformationTheory.Kolmogorov.interpretProg idx q = true :: (List.replicate idx true ++ false :: q)

Instances For

Used by

noncomputable def

InformationTheory.Kolmogorov.universalEval

source

List Bool → ℕ → Part ℕ

The fixed universal machine. A program is a bit string; the leading bit selects the literal or interpret mode. y is the conditioning input.

Equations

One or more equations did not get rendered due to their size.
InformationTheory.Kolmogorov.universalEval [] x✝ = Part.none
InformationTheory.Kolmogorov.universalEval (false :: bs) x✝ = Part.some (Computability.decodeNat bs)

Instances For

Used by

def

InformationTheory.Kolmogorov.natLen

source

(x : ℕ) :

ℕ

Bit length of x, the length of the echo program payload.

Equations

InformationTheory.Kolmogorov.natLen x = (Computability.encodeNat x).length

Instances For

Used by

theorem

InformationTheory.Kolmogorov.posLen_le

source

(p : PosNum) :

2 ^ (Computability.encodePosNum p).length ≤ 2 * ↑p

Used by

theorem

InformationTheory.Kolmogorov.numLen_le

source

(m : Num) (hm : 1 ≤ ↑m) :

2 ^ (Computability.encodeNum m).length ≤ 2 * ↑m

Used by

theorem

InformationTheory.Kolmogorov.natLen_le

source

(n : ℕ) (hn : 1 ≤ n) :

2 ^ natLen n ≤ 2 * n

Used by

theorem

InformationTheory.Kolmogorov.natLen_le_of_lt_two_pow

source

(x k : ℕ) (h : x < 2 ^ k) :

natLen x ≤ k

Used by

noncomputable def

InformationTheory.Kolmogorov.condComplexity

source

(x y : ℕ) :

ℕ

Conditional Kolmogorov complexity C(x | y): the length of the shortest program that, run under condition y, outputs x. The literal mode makes the set nonempty, so this infimum is attained (condComplexity_spec).

Equations