Documentation

Complexity.Computability.Machines.Turing.MultiTape.Halting.Basic

Halting of machines and of their descriptions #

A deterministic multi-tape machine halts on an input when its run from the initial configuration is halted after some number of steps (Turing.MultiTapeTM.Halts). It then halts with exactly one output (Turing.MultiTapeTM.Computes.unique); cslib's Turing.MultiTapeTM.Computes records that output, without a bound on the number of steps. A halted run neither moves nor visits new cells, so a machine halting with an output computes it within the time at which it halts and the space it has used by then (Turing.MultiTapeTM.Computes.exists_computesInTimeAndSpace).

The same notions for the machines described by a description (Turing.MultiTapeTM.Universal.Desc) are read off the simulation Turing.MultiTapeTM.Universal.simulate, which the universal machine computes: the described machine halts when the simulation reports a halted run after some number of steps (Turing.MultiTapeTM.Universal.Desc.Halts), with the output collected by then (Turing.MultiTapeTM.Universal.Desc.Computes). On the description of a machine with finitely many states and symbols they are the notions of the machine itself, under the renaming of its symbols.

Main definitions #

Main results #

References #

source
def Turing.MultiTapeTM.Halts {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) :
Prop

The machine halts on input: its run from the initial configuration is halted after some number of steps.

Instances For
    source
    theorem Turing.MultiTapeTM.Computes.halts {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} (h : tm.Computes input output) :
    tm.Halts input

    A machine that halts with an output halts.

    source
    theorem Turing.MultiTapeTM.Computes.unique {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input o₁ o₂ : List Symbol} (h₁ : tm.Computes input o₁) (h₂ : tm.Computes input o₂) :
    o₁ = o₂

    A machine halts with at most one output.

    source
    theorem Turing.MultiTapeTM.Computes.output_eq_of_halted {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} (h : tm.Computes input output) {t : ℕ} (ht : (runFrom (tm.initCfg input) t).Halted) :
    (runFrom (tm.initCfg input) t).output = output

    Once halted, a run has the output it halts with.

    source
    theorem Turing.MultiTapeTM.halts_iff_exists_computes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} :
    tm.Halts input ↔ ∃ (output : List Symbol), tm.Computes input output

    A machine halts exactly when it halts with some output.

    source
    theorem Turing.MultiTapeTM.Computes.exists_computesInTimeAndSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} (h : tm.Computes input output) :
    ∃ (t : ℕ) (s : ℕ), tm.ComputesInTimeAndSpace input output t s

    An output computed without bounds is computed within bounds: the time at which the machine halts, and the space it has used by then.

    source
    def Turing.MultiTapeTM.Universal.Desc.Halts (d : Desc) (x : List ℕ) :
    Prop

    The machine described by d halts on the input x: the simulation reports a halted run after some number of steps.

    Instances For
      source
      def Turing.MultiTapeTM.Universal.Desc.Computes (d : Desc) (x out : List ℕ) :
      Prop

      The machine described by d halts on the input x with output out.

      Instances For
        source
        theorem Turing.MultiTapeTM.Universal.Desc.halts_iff_exists_computes {d : Desc} {x : List ℕ} :
        d.Halts x ↔ ∃ (o : List ℕ), d.Computes x o

        The machine described by d halts exactly when it halts with some output.

        source
        theorem Turing.MultiTapeTM.Universal.Desc.halts_desc {k : ℕ} {Symbol S : Type} [Fintype S] [Fintype Symbol] (eS : S ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol S) (x : List Symbol) :
        (desc eS eY tm).Halts (List.map (⇑eY) x) ↔ tm.Halts x

        The machine described by the description of tm halts on the renamed input exactly when tm halts on the input.

        source
        theorem Turing.MultiTapeTM.Universal.Desc.computes_desc {k : ℕ} {Symbol S : Type} [Fintype S] [Fintype Symbol] (eS : S ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol S) (x out : List Symbol) :
        (desc eS eY tm).Computes (List.map (⇑eY) x) (List.map (⇑eY) out) ↔ tm.Computes x out

        The machine described by the description of tm halts on the renamed input with the renamed output exactly when tm halts on the input with the output.