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. Local additions give the runs of machines built with combine.

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.runFrom_combine_left, Turing.MultiTapeTM.runFrom_combine_right: a machine built with combine runs as either of its parts.
• 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.

Runs of combined machines

theorem Turing.MultiTapeTM.step_combine_left {k : ℕ} {Symbol : Type u_2} {input : List Symbol} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} (h : ∀ (q : State₀), next₀ (some q) = some (Sum.inl q)) {cfg : Cfg k Symbol State₀ input} (hcfg : ¬cfg.Halted) : step (Cfg.mapState next₀ cfg) = Cfg.mapState next₀ (step cfg)

If next₀ keeps the live states of tm₀ in tm₀, a step of tm₀ from a running configuration is a step of the combined machine, its states relabeled along next₀.

theorem Turing.MultiTapeTM.step_combine_right {k : ℕ} {Symbol : Type u_2} {input : List Symbol} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} (cfg : Cfg k Symbol State₁ input) : step (Cfg.mapState (Option.map Sum.inr) cfg) = Cfg.mapState (Option.map Sum.inr) (step cfg)

A step of tm₁ is a step of the combined machine, if the steps of tm₁ stay in tm₁.

theorem Turing.MultiTapeTM.runFrom_combine_left {k : ℕ} {Symbol : Type u_2} {input : List Symbol} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} (h : ∀ (q : State₀), next₀ (some q) = some (Sum.inl q)) (cfg : Cfg k Symbol State₀ input) {t : ℕ} (hrun : ∀ s < t, ¬(runFrom cfg s).Halted) : runFrom (Cfg.mapState next₀ cfg) t = Cfg.mapState next₀ (runFrom cfg t)

While tm₀ is running, the combined machine runs as tm₀, its states relabeled along next₀, if next₀ keeps the live states of tm₀ in tm₀.

theorem Turing.MultiTapeTM.HaltsAt.runFrom_combine_left {k : ℕ} {Symbol : Type u_2} {input : List Symbol} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} (h : ∀ (q : State₀), next₀ (some q) = some (Sum.inl q)) {cfg : Cfg k Symbol State₀ input} {u t : ℕ} (hu : tm₀.HaltsAt cfg u) (ht : t ≤ u) : runFrom (Cfg.mapState next₀ cfg) t = Cfg.mapState next₀ (runFrom cfg t)

Up to the step at which tm₀ halts, the combined machine runs as tm₀, its states relabeled along next₀, if next₀ keeps the live states of tm₀ in tm₀.

theorem Turing.MultiTapeTM.runFrom_combine_right {k : ℕ} {Symbol : Type u_2} {input : List Symbol} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁} (cfg : Cfg k Symbol State₁ input) (t : ℕ) : runFrom (Cfg.mapState (Option.map Sum.inr) cfg) t = Cfg.mapState (Option.map Sum.inr) (runFrom cfg t)

The combined machine runs as tm₁, if the steps of tm₁ stay in tm₁.

theorem Turing.MultiTapeTM.mapState_handOver_of_halted {k : ℕ} {Symbol : Type u_2} {input : List Symbol} {State₀ : Type u_3} {State₁ : Type u_4} {q₁ : State₁} {cfg : Cfg k Symbol State₀ input} (h : cfg.Halted) : Cfg.mapState (handOver q₁) cfg = Cfg.mapState (Option.map Sum.inr) (cfg.withState (some q₁))

A halted configuration of the first machine, relabeled through handOver q₁, is the configuration in which the second machine starts in q₁.

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.