Description methods of single-tape Turing machines (SingleTapeTM, TM0, TM1)

A binary single-tape Turing machine tm : SingleTapeTM Bool (or a finitely supported Mathlib TM0.Machine or TM1.Stmt program) defines a description method for binary strings: a program p : List Bool is placed on the tape as BiTape.mk₁ p, the clock counts steps, and once tm reaches none with the tape in standard output form BiTape.mk₁ x, it outputs x (ofSingleTapeTM, ofTM0, ofTM1).

Using Turing.MultiTapeTM.ofSingleTapeTM and Turing.MultiTapeTM.computesInTimeAndSpace_ofSingleTapeTM_of_input, every single-tape description method ofSingleTapeTM tm is simulated by the 1-work-tape multi-tape description method ofMultiTapeTM (MultiTapeTM.ofSingleTapeTM tm) with zero program overhead (compile := id) and linear time overhead 3 * |p| + 2 * t + 6 (singleTapeSimulation).

Furthermore, tm.eval is partial recursive (Cslib.Turing.SingleTapeTM.partrec_eval), so mapping any computable decoder dec : List Bool → ℕ over ofSingleTapeTM tm, ofTM0 M S hs, or ofTM1 M S hs yields a partial recursive description method (isPartrec_ofSingleTapeTM_map, isPartrec_ofTM0_map, isPartrec_ofTM1_map). By the invariance theorem (isAdditivelyOptimal_universal), universal is at most an additive constant worse than any single-tape Turing machine.

Main definitions

• Cslib.Kolmogorov.DescriptionMethod.ofSingleTapeTM: the description method of a SingleTapeTM.
• Cslib.Kolmogorov.DescriptionMethod.ofTM0: the description method of a finitely supported Mathlib TM0.Machine.
• Cslib.Kolmogorov.DescriptionMethod.ofTM1: the description method of a finitely supported Mathlib TM1 program.
• Cslib.Kolmogorov.DescriptionMethod.singleTapeSimulation: simulation of ofSingleTapeTM tm by ofMultiTapeTM (MultiTapeTM.ofSingleTapeTM tm) with 0 program overhead and 3 * |p| + 2 * t + 6 time overhead.
• Cslib.Kolmogorov.DescriptionMethod.tm0Simulation: simulation of ofTM0 M S hs by a multi-tape Turing machine with 0 program overhead and 3 * |p| + 2 * t + 6 time overhead.

Main results

• Cslib.Kolmogorov.DescriptionMethod.mem_ofSingleTapeTM_runFor_iff: a program outputs x within t steps under ofSingleTapeTM tm iff tm.OutputsWithinTime p x t.
• Cslib.Kolmogorov.DescriptionMethod.ofSingleTapeTM_produces_iff: a program describes x under ofSingleTapeTM tm iff tm.Outputs p x.
• Cslib.Kolmogorov.DescriptionMethod.ofTM0_produces_iff: a program describes x under ofTM0 M S hs iff StateTransition.eval (TM0.step M) halts with BiTape.equivTape (BiTape.mk₁ x).
• Cslib.Kolmogorov.DescriptionMethod.ecomplexity_ofMultiTapeTM_ofSingleTapeTM_le, Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_ofMultiTapeTM_ofSingleTapeTM_le: plain and time-bounded complexity transfer from SingleTapeTM to MultiTapeTM.
• Cslib.Kolmogorov.DescriptionMethod.isPartrec_ofSingleTapeTM_map, Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_ofSingleTapeTM: partial recursiveness and additive optimality of universal over SingleTapeTM (and TM0 / TM1).

References

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

def Cslib.Kolmogorov.DescriptionMethod.ofSingleTapeTM (tm : Turing.SingleTapeTM Bool) : DescriptionMethod (List Bool)

The description method of a binary single-tape Turing machine tm : SingleTapeTM Bool: on program p, after t steps, outputs x if tm has halted with BiTape.mk₁ x on its tape.

theorem Cslib.Kolmogorov.DescriptionMethod.mem_ofSingleTapeTM_runFor_iff {tm : Turing.SingleTapeTM Bool} {p x : List Bool} {t : ℕ} : x ∈ ((ofSingleTapeTM tm).run p).runFor t ↔ tm.OutputsWithinTime p x t

A program outputs x within t steps under ofSingleTapeTM tm iff tm.OutputsWithinTime p x t.

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.ofSingleTapeTM_produces_iff {tm : Turing.SingleTapeTM Bool} {p x : List Bool} : (ofSingleTapeTM tm).Produces p x ↔ tm.Outputs p x

A program describes x under ofSingleTapeTM tm iff tm.Outputs p x.

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_ofSingleTapeTM_le {tm : Turing.SingleTapeTM Bool} {p x : List Bool} (h : tm.Outputs p x) : (ofSingleTapeTM tm).ecomplexity x ≤ ↑p.length

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_ofSingleTapeTM_le {tm : Turing.SingleTapeTM Bool} {p x : List Bool} {t : ℕ} (h : tm.OutputsWithinTime p x t) : (ofSingleTapeTM tm).etimeBoundedComplexity t x ≤ ↑p.length

Description methods of Mathlib's TM0 and TM1

def Cslib.Kolmogorov.DescriptionMethod.ofTM0 {Λ : Type} [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine (Option Bool) Λ) (S : Finset Λ) (hs : Turing.TM0.Supports M ↑S) : DescriptionMethod (List Bool)

The description method of a finitely supported Mathlib TM0.Machine (Option Bool) Λ.

theorem Cslib.Kolmogorov.DescriptionMethod.mem_ofTM0_runFor_succ_iff {p x : List Bool} {t : ℕ} {Λ : Type} [Inhabited Λ] [DecidableEq Λ] {M : Turing.TM0.Machine (Option Bool) Λ} {S : Finset Λ} {hs : Turing.TM0.Supports M ↑S} : x ∈ ((ofTM0 M S hs).run p).runFor (t + 1) ↔ ∃ (q_f : Λ), Relation.RelatesWithinSteps (fun (a b : Turing.TM0.Cfg (Option Bool) Λ) => b ∈ Turing.TM0.step M a) (Turing.TM0.init (List.map some p)) { q := q_f, Tape := Turing.BiTape.equivTape (Turing.BiTape.mk₁ x) } t ∧ Turing.TM0.step M { q := q_f, Tape := Turing.BiTape.equivTape (Turing.BiTape.mk₁ x) } = none

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.ofTM0_produces_iff {p x : List Bool} {Λ : Type} [Inhabited Λ] [DecidableEq Λ] {M : Turing.TM0.Machine (Option Bool) Λ} {S : Finset Λ} {hs : Turing.TM0.Supports M ↑S} : (ofTM0 M S hs).Produces p x ↔ ∃ (q_f : Λ), { q := q_f, Tape := Turing.BiTape.equivTape (Turing.BiTape.mk₁ x) } ∈ StateTransition.eval (Turing.TM0.step M) (Turing.TM0.init (List.map some p))

noncomputable def Cslib.Kolmogorov.DescriptionMethod.ofTM1 {Λ σ : Type} [Inhabited Λ] [Inhabited σ] [Fintype σ] (M : Λ → Turing.TM1.Stmt (Option Bool) Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) : DescriptionMethod (List Bool)

The description method of a finitely supported Mathlib TM1 statement table.

Simulation of ofSingleTapeTM and ofTM0 by ofMultiTapeTM

def Cslib.Kolmogorov.DescriptionMethod.singleTapeSimulation (tm : Turing.SingleTapeTM Bool) : (ofSingleTapeTM tm).Simulation (ofMultiTapeTM (Turing.MultiTapeTM.ofSingleTapeTM tm)) 0 fun (n t : ℕ) => 3 * n + 2 * t + 6

Every single-tape description method ofSingleTapeTM tm is simulated by the 1-work-tape multi-tape description method ofMultiTapeTM (MultiTapeTM.ofSingleTapeTM tm) with zero program overhead (compile := id) and linear time overhead 3 * |p| + 2 * t + 6.

theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_ofMultiTapeTM_ofSingleTapeTM_le (tm : Turing.SingleTapeTM Bool) (x : List Bool) : (ofMultiTapeTM (Turing.MultiTapeTM.ofSingleTapeTM tm)).ecomplexity x ≤ (ofSingleTapeTM tm).ecomplexity x

Plain Kolmogorov complexity under MultiTapeTM.ofSingleTapeTM tm is at most that under tm.

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_ofMultiTapeTM_ofSingleTapeTM_le (tm : Turing.SingleTapeTM Bool) {t k : ℕ} {x : List Bool} (h : (ofSingleTapeTM tm).etimeBoundedComplexity t x ≤ ↑k) : (ofMultiTapeTM (Turing.MultiTapeTM.ofSingleTapeTM tm)).etimeBoundedComplexity (3 * k + 2 * t + 6) x ≤ ↑k

Time-bounded Kolmogorov complexity transfer from SingleTapeTM to MultiTapeTM: a description of length at most k running in t single-tape steps gives a multi-tape description of length at most k running in 3 * k + 2 * t + 6 steps.

def Cslib.Kolmogorov.DescriptionMethod.tm0Simulation {Λ : Type} [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine (Option Bool) Λ) (S : Finset Λ) (hs : Turing.TM0.Supports M ↑S) : (ofTM0 M S hs).Simulation (ofMultiTapeTM (Turing.MultiTapeTM.ofSingleTapeTM (Turing.SingleTapeTM.ofTM0 M S hs))) 0 fun (n t : ℕ) => 3 * n + 2 * t + 6

Every TM0 description method ofTM0 M S hs is simulated by a 1-work-tape MultiTapeTM with zero program overhead and linear time overhead 3 * |p| + 2 * t + 6.

Partial recursiveness and optimality of universal over SingleTapeTM, TM0, TM1

theorem Cslib.Kolmogorov.DescriptionMethod.isPartrec_ofSingleTapeTM_map (tm : Turing.SingleTapeTM Bool) {dec : List Bool → ℕ} (hdec : Computable dec) : (map dec (ofSingleTapeTM tm)).IsPartrec

For every tm : SingleTapeTM Bool and computable decoder dec : List Bool → ℕ, mapping dec over ofSingleTapeTM tm yields a partial recursive description method.

theorem Cslib.Kolmogorov.DescriptionMethod.isPartrec_ofTM0_map {Λ : Type} [Inhabited Λ] [DecidableEq Λ] (M : Turing.TM0.Machine (Option Bool) Λ) (S : Finset Λ) (hs : Turing.TM0.Supports M ↑S) {dec : List Bool → ℕ} (hdec : Computable dec) : (map dec (ofTM0 M S hs)).IsPartrec

For every finitely supported TM0.Machine (Option Bool) Λ and computable decoder dec : List Bool → ℕ, mapping dec over ofTM0 M S hs yields a partial recursive description method.

theorem Cslib.Kolmogorov.DescriptionMethod.isPartrec_ofTM1_map {Λ σ : Type} [Inhabited Λ] [Inhabited σ] [Fintype σ] (M : Λ → Turing.TM1.Stmt (Option Bool) Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) {dec : List Bool → ℕ} (hdec : Computable dec) : (map dec (ofTM1 M S hs)).IsPartrec

For every finitely supported TM1 statement table and computable decoder dec : List Bool → ℕ, mapping dec over ofTM1 M S hs yields a partial recursive description method.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_ofSingleTapeTM (tm : Turing.SingleTapeTM Bool) {dec : List Bool → ℕ} (hdec : Computable dec) : ∃ (c : ℕ), ∀ (x : List Bool), universal.ecomplexity (dec x) ≤ (ofSingleTapeTM tm).ecomplexity x + ↑c

Optimality of universal over single-tape Turing machines: for every tm : SingleTapeTM Bool and computable decoder dec : List Bool → ℕ, universal is at most an additive constant worse than ofSingleTapeTM tm.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_ofSingleTapeTM_bits (tm : Turing.SingleTapeTM Bool) : ∃ (c : ℕ), ∀ (n : ℕ), universal.ecomplexity n ≤ (ofSingleTapeTM tm).ecomplexity n.bits + ↑c

Using Nat.bits and List.foldr Nat.bit 0, universal is at most an additive constant worse than any tm : SingleTapeTM Bool on binary representations of natural numbers.