Documentation

Complexity.Computability.Kolmogorov.MultiTape

Description methods of multi-tape Turing machines #

A deterministic multi-tape Turing machine over the binary alphabet is a description method: a program is an input of the machine, the clock counts steps, and the output of a program is the contents of the output tape once the machine has halted. Its complexity C_tm(x) is the length of a shortest input on which tm computes x, and C_tm^t(x) that of a shortest input on which tm computes x within t steps.

When the state space is finite, tm.eval is partial recursive (Turing.MultiTapeTM.partrec_eval), so mapping any computable decoder dec : List Bool → ℕ over ofMultiTapeTM tm yields a partial recursive description method (isPartrec_ofMultiTapeTM_map). By the invariance theorem (isAdditivelyOptimal_universal), universal is at most an additive constant worse than any finite-state multi-tape Turing machine (exists_ecomplexity_universal_le_ofMultiTapeTM).

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Kolmogorov.DescriptionMethod.ofMultiTapeTM {k : ℕ} {State : Type u_1} (tm : Turing.MultiTapeTM k Bool State) :
DescriptionMethod (List Bool)

The description method of a deterministic multi-tape Turing machine over the binary alphabet: the program p is the input, and after t steps its output is the contents of the output tape if the machine has halted.

Instances For
    source
    theorem Cslib.Kolmogorov.DescriptionMethod.mem_ofMultiTapeTM_runFor_iff_halted {k : ℕ} {State : Type u_1} {tm : Turing.MultiTapeTM k Bool State} {p x : List Bool} {t : ℕ} :
    x ∈ ((ofMultiTapeTM tm).run p).runFor t ↔ (Turing.MultiTapeTM.runFrom (tm.initCfg p) t).Halted ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg p) t).output = x
    source
    @[simp]
    theorem Cslib.Kolmogorov.DescriptionMethod.ofMultiTapeTM_produces_iff {k : ℕ} {State : Type u_1} {tm : Turing.MultiTapeTM k Bool State} {p x : List Bool} :
    (ofMultiTapeTM tm).Produces p x ↔ tm.Computes p x

    A program describes x exactly when the machine computes x from it.

    source
    theorem Cslib.Kolmogorov.DescriptionMethod.mem_ofMultiTapeTM_runFor_iff {k : ℕ} {State : Type u_1} {tm : Turing.MultiTapeTM k Bool State} {p x : List Bool} {t : ℕ} :
    x ∈ ((ofMultiTapeTM tm).run p).runFor t ↔ tm.RunsInTime p t ∧ tm.Computes p x

    A program describes x within t steps exactly when the machine computes x from it and halts within t steps.

    source
    theorem Cslib.Kolmogorov.DescriptionMethod.ecomplexity_ofMultiTapeTM_le {k : ℕ} {State : Type u_1} {tm : Turing.MultiTapeTM k Bool State} {p x : List Bool} (h : tm.Computes p x) :
    (ofMultiTapeTM tm).ecomplexity x ≤ ↑p.length
    source
    theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_ofMultiTapeTM_le {k : ℕ} {State : Type u_1} {tm : Turing.MultiTapeTM k Bool State} {p x : List Bool} {t : ℕ} (ht : tm.RunsInTime p t) (h : tm.Computes p x) :
    (ofMultiTapeTM tm).etimeBoundedComplexity t x ≤ ↑p.length

    An input from which the machine computes x within t steps bounds the time-bounded complexity C_tm^t(x).

    A machine simulating the literal method #

    source
    def Cslib.Kolmogorov.DescriptionMethod.literalSimulation {k : ℕ} {State : Type u_1} {tm : Turing.MultiTapeTM k Bool State} (h : tm.ComputesFunInTimeAndSpace (Function.Embedding.refl (List Bool)) (Function.Embedding.refl (List Bool)) id (fun (p : List Bool) => p.length + 1) fun (x : List Bool) => 0) :
    literal.Simulation (ofMultiTapeTM tm) 0 fun (x t : ℕ) => t + 1

    From a computation of the identity, a simulation of the literal description method with one extra step.

    Instances For
      source
      theorem Cslib.Kolmogorov.DescriptionMethod.exists_simulation_literal :
      ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : Turing.MultiTapeTM k Bool State), Nonempty (literal.Simulation (ofMultiTapeTM tm) 0 fun (x t : ℕ) => t + 1)

      Some machine with finitely many states simulates the literal description method with one extra step, so under it every string x has complexity at most |x| within |x| + 1 steps.

      Partial recursiveness and optimality of universal over MultiTapeTM #

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.isPartrec_ofMultiTapeTM_map {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) {dec : List Bool → ℕ} (hdec : Computable dec) :
      (map dec (ofMultiTapeTM tm)).IsPartrec

      For every finite-state binary MultiTapeTM and computable decoder dec : List Bool → ℕ, mapping dec over ofMultiTapeTM tm yields a partial recursive description method.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_ofMultiTapeTM {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) {dec : List Bool → ℕ} (hdec : Computable dec) :
      ∃ (c : ℕ), ∀ (x : List Bool), universal.ecomplexity (dec x) ≤ (ofMultiTapeTM tm).ecomplexity x + ↑c

      Optimality of universal over finite-state multi-tape Turing machines: for every finite-state binary MultiTapeTM and computable decoder dec : List Bool → ℕ, universal is at most an additive constant worse than ofMultiTapeTM tm.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_ofMultiTapeTM_bits {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) :
      ∃ (c : ℕ), ∀ (n : ℕ), universal.ecomplexity n ≤ (ofMultiTapeTM tm).ecomplexity n.bits + ↑c

      Using Nat.bits and List.foldr Nat.bit 0, universal is at most an additive constant worse than any finite-state binary MultiTapeTM on binary representations of natural numbers.