Skip to content

InformationTheory.Shannon.Kolmogorov.Omega

Imports 4

Chaitin's halting probability #

Cover–Thomas (2nd ed.). The halting probability of the self-delimiting machine is the total weight ∑ 2^{-|p|} of its halting programs. Because the halting set is prefix-free, the Kraft bound applies to every finite subsum, so Ω is a subprobability; the literal echo program halts, so Ω is positive.

The second half of the section is that the prefix world is not computable. The Berry argument of the plain machine transfers: a computable K would let one search for the least string of prefix complexity at least k, and the self-delimiting interpreter describes that string in 2 · natLen k + O(1) bits.

Main definitions #

chaitinOmega — the halting probability Ω in ℝ≥0∞.
prefixInterpretProg — the self-delimited interpretation program.

Main statements #

chaitinOmega_le_one — Ω ≤ 1, the Kraft bound on the halting set.
chaitinOmega_pos — 0 < Ω.
prefixComplexity_not_computable — K is not a computable function.

noncomputable def

InformationTheory.Kolmogorov.chaitinOmega

:

Chaitin's halting probability Ω = ∑_{p halts} 2^{-|p|} in ℝ≥0∞, the weight of the halting programs of the self-delimiting machine. @audit:ok

Equations

InformationTheory.Kolmogorov.chaitinOmega = ∑' (p : { p : List Bool // (InformationTheory.Kolmogorov.prefixUniversalEval p).Dom }), 2⁻¹ ^ (↑p).length

Instances For

Used by

theorem

InformationTheory.Kolmogorov.chaitinOmega_le_one

:

chaitinOmega ≤ 1

The halting probability is a subprobability: Ω ≤ 1, because the halting programs form a prefix-free set and every finite subsum is a Kraft sum. The bound is not the degenerate empty-sum reading: the halting set is nonempty (the literal echo program halts), and chaitinOmega_pos pins Ω to (0, 1]. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.chaitinOmega_pos

:

0 < chaitinOmega

The halting probability is positive: the literal echo program prefixLiteralProg 0 halts, so its weight is a strictly positive term of the sum.

Used by

theorem

InformationTheory.Kolmogorov.chaitinOmega_ne_top

:

chaitinOmega ≠ ⊤

Used by

Non-computability of prefix complexity #

noncomputable def

InformationTheory.Kolmogorov.shortestPrefixProg

(x : ℕ) :

A shortest self-delimiting program for x (attained by prefixComplexity_spec).

Equations

InformationTheory.Kolmogorov.shortestPrefixProg x = ⋯.choose

Instances For

Used by

noncomputable def

InformationTheory.Kolmogorov.shortestPrefixNat

(x : ℕ) :

The natural-number code of x's shortest self-delimiting program.

Equations

InformationTheory.Kolmogorov.shortestPrefixNat x = InformationTheory.Kolmogorov.progNat (InformationTheory.Kolmogorov.shortestPrefixProg x)

Instances For

Used by

theorem

InformationTheory.Kolmogorov.shortestPrefixProg_length

(x : ℕ) :

(shortestPrefixProg x).length = prefixComplexity x

Used by

theorem

InformationTheory.Kolmogorov.shortestPrefixProg_mem

(x : ℕ) :

x ∈ prefixUniversalEval (shortestPrefixProg x)

Used by

theorem

InformationTheory.Kolmogorov.shortestPrefixNat_injective

:

Function.Injective shortestPrefixNat

Used by

theorem

InformationTheory.Kolmogorov.shortestPrefixNat_lt_of_lt

{x k : ℕ} (hx : prefixComplexity x < k) :

shortestPrefixNat x < 2 ^ k

Used by

theorem

InformationTheory.Kolmogorov.prefixComplexity_lt_finite

(k : ℕ) :

{x : ℕ | prefixComplexity x < k}.Finite

Used by

theorem

InformationTheory.Kolmogorov.exists_prefixIncompressible

(k : ℕ) :

∃ (x : ℕ), k ≤ prefixComplexity x

Used by

def

InformationTheory.Kolmogorov.prefixInterpretProg

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

The self-delimited interpretation program for code index idx running on the description q: the interpret flag, then idx in unary terminated by false, then q, all wrapped by the self-delimiting length prefix. @audit:ok

Equations

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

Instances For

Used by

theorem

InformationTheory.Kolmogorov.prefixInterpretProg_length

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

(prefixInterpretProg idx q).length = 2 * q.length + (2 * idx + 5)

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_interpret

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

prefixUniversalEval (prefixInterpretProg idx q) = (Denumerable.ofNat Nat.Partrec.Code idx).eval (Nat.pair (Computability.decodeNat q) 0)

Used by

theorem

InformationTheory.Kolmogorov.prefix_invariance_code

(c : Nat.Partrec.Code) :

∃ (b : ℕ), ∀ (x : ℕ) (q : List Bool), x ∈ c.eval (Nat.pair (Computability.decodeNat q) 0) → prefixComplexity x ≤ 2 * q.length + b

Used by

theorem

InformationTheory.Kolmogorov.prefix_invariance

(A : ℕ → ℕ → Part ℕ) (hA : Partrec₂ A) :

∃ (b : ℕ), ∀ (x : ℕ) (q : List Bool), x ∈ A (Computability.decodeNat q) 0 → prefixComplexity x ≤ 2 * q.length + b

Used by

theorem

InformationTheory.Kolmogorov.prefixComplexity_not_computable

:

¬Computable prefixComplexity

Prefix Kolmogorov complexity is not computable (Berry's paradox): a computable K would let one search for the least string of prefix complexity at least k, which the self-delimiting interpreter then describes in 2 · natLen k + O(1) bits. @audit:ok

Used by