Runs one step at a time, the halting step, and machines computing in zero space

The additions of Christian Reitwiessner's branch crei/tidy-universal to Cslib.Computability.Machines.Turing.MultiTape.Deterministic, together with the addition of cslib PR #1138: runs one step or one phase at a time, the time bound of a deterministic machine as a halted run, the step at which a run halts, the output emitted in t steps, and machines computing in zero space.

Main definitions

• Turing.MultiTapeTM.HaltsAt: the run from a configuration halts at exactly a given step.

Main results

• Turing.MultiTapeTM.runFrom_succ, Turing.MultiTapeTM.runFrom_add: a run, one step or one phase at a time.
• Turing.MultiTapeTM.runsInTime_iff_halted: a deterministic machine runs in time t exactly when it has halted after t steps.
• Turing.MultiTapeTM.exists_haltsAt: a halted run halts at some step.
• Turing.MultiTapeTM.length_output_runFrom_le: in t steps a machine emits at most t symbols.
• Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_no_work_tapes: a function computable in zero space is computable by a machine without work tapes.

theorem Turing.MultiTapeTM.runFrom_succ {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (t : ℕ) : runFrom cfg (t + 1) = step (runFrom cfg t)

One more step of a run.

theorem Turing.MultiTapeTM.runFrom_one {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) : runFrom cfg 1 = step cfg

A run of one step.

theorem Turing.MultiTapeTM.runFrom_add {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (m n : ℕ) : runFrom cfg (m + n) = runFrom (runFrom cfg m) n

A run splits at any intermediate step.

theorem Turing.MultiTapeTM.runsInTime_iff_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {t : ℕ} : tm.RunsInTime input t ↔ (runFrom (tm.initCfg input) t).Halted

A deterministic machine runs in time t exactly when it has halted after t steps.

def Turing.MultiTapeTM.HaltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) {input : List Symbol} (cfg : Cfg k Symbol State input) (t : ℕ) : Prop

The machine tm started in cfg halts at step t: it is halted after t steps and not halted after any smaller number of steps.

theorem Turing.MultiTapeTM.HaltsAt.halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {t : ℕ} (h : tm.HaltsAt cfg t) : (runFrom cfg t).Halted

theorem Turing.MultiTapeTM.HaltsAt.not_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h : tm.HaltsAt cfg t) (hs : s < t) : ¬(runFrom cfg s).Halted

theorem Turing.MultiTapeTM.HaltsAt.le_of_halted {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h : tm.HaltsAt cfg t) (hs : (runFrom cfg s).Halted) : t ≤ s

The halting step is the first step at which the machine is halted.

theorem Turing.MultiTapeTM.HaltsAt.unique {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h₁ : tm.HaltsAt cfg s) (h₂ : tm.HaltsAt cfg t) : s = t

The halting step is unique.

theorem Turing.MultiTapeTM.HaltsAt.runFrom_eq {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {s t : ℕ} (h : tm.HaltsAt cfg t) (hts : t ≤ s) : runFrom cfg s = runFrom cfg t

From the halting step on, the configuration does not change.

theorem Turing.MultiTapeTM.exists_haltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {t : ℕ} (hhalt : (runFrom cfg t).Halted) : ∃ u ≤ t, tm.HaltsAt cfg u

A run that is halted after t steps halts at some step u ≤ t.

theorem Turing.MultiTapeTM.existsUnique_haltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {cfg : Cfg k Symbol State input} {t : ℕ} (hhalt : (runFrom cfg t).Halted) : ∃! u : ℕ, tm.HaltsAt cfg u

A run that is halted after some number of steps halts at exactly one step.

theorem Turing.MultiTapeTM.length_output_runFrom_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : (runFrom cfg t).output.length ≤ cfg.output.length + t

In t steps the machine emits at most t symbols.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_no_work_tapes {α : Type u_3} {β : Type u_4} [Nonempty α] {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {t : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t fun (x : α) => 0) : ∃ (State : Type) (_ : Finite State) (tm : MultiTapeTM 0 Bool State), tm.ComputesFunInTimeAndSpace encIn encOut f t fun (x : α) => 0

A function computable in zero space is computable by a machine without work tapes, within the same bounds, since every work tape costs at least one cell (MultiTapeNTM.RunsInSpace.le). The domain must be nonempty: otherwise the machine is never run and its number of tapes is arbitrary.