InformationTheory.Shannon.Kolmogorov.PrefixComputability

Imports 5

Computability of the self-delimiting machine #

The self-delimiting machine prefixUniversalEval is a partial recursive function, and its halting set is undecidable. The first statement assembles the machine from the primitive recursive parser parseUnary and the partial recursive payload decoder decodePayload. The second reduces the halting problem of Mathlib's universal interpreter to it along the interpret-mode entry prefixInterpretProg.

Main statements #

prefixUniversalEval_partrec — the machine is partial recursive.
prefixUniversalEval_dom_not_computablePred — its halting set is undecidable.

theorem

InformationTheory.Kolmogorov.primrec_replicate_true

source

Primrec fun (n : ℕ) => List.replicate n true

Used by

theorem

InformationTheory.Kolmogorov.primrec_prefixInterpretProg_nil

source

Primrec fun (idx : ℕ) => prefixInterpretProg idx []

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_partrec

source

Partrec prefixUniversalEval

The self-delimiting machine is partial recursive: its length guard is primitive recursive through parseUnary, and the payload it hands on is decoded by the partial recursive decodePayload.

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_dom_not_computablePred

source

¬ComputablePred fun (p : List Bool) => (prefixUniversalEval p).Dom

The halting set of the self-delimiting machine is undecidable: a decision procedure for it would decide the halting problem of Mathlib's universal interpreter, which the interpret-mode entry prefixInterpretProg embeds into it. @audit:ok

Used by