diff --git a/Cslib.lean b/Cslib.lean index cbc202417..34fac9cba 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,6 +46,7 @@ public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Languages.SafetyLiveness +public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Id public import Cslib.Computability.Machines.Turing.MultiTape.Configuration public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Id.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Id.lean new file mode 100644 index 000000000..38e8f5b97 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Id.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Complexity of the identity function + +A machine with a single state and no work tapes scans the input from left to right, copying each +symbol to the output tape, and halts on the blank at the right end of the input. On input `w` it +outputs `w` after `w.length + 1` steps, and having no work tapes it uses zero space. + +## Main results + +* `Turing.MultiTapeTM.computableInTimeAndSpace_id`: the identity is computable in one step per + input symbol and zero space. +-/ + +namespace Turing.MultiTapeTM + +variable {Symbol : Type*} {input : List Symbol} + +/-- The copy machine: a single state and no work tapes. It copies every input symbol to the output +tape while moving right, and halts on reading the blank at the right end of the input. -/ +def copy : MultiTapeTM 0 Symbol Unit where + q₀ := () + tr _ s _ := + match s with + | some b => { inputTape := 1, workTapes := fun i => i.elim0, output := some b, + state := some () } + | none => { inputTape := 0, workTapes := fun i => i.elim0, output := none, state := none } + +namespace Copy + +/-- A configuration of the copy machine, given by the input, the control state, the input head +position and the output written so far. There are no work tapes. `input` is explicit because it is +inferable only through the expected type: the head position is written as an anonymous +constructor, which pins nothing. -/ +def cfg (input : List Symbol) (q : Option Unit) (p : Fin (input.length + 2)) + (out : List Symbol) : Cfg 0 Symbol Unit input := + ⟨q, p, fun _ _ => none, fun _ => 0, out⟩ + +/-- With no work tapes, configurations are equal as soon as the state, the input position and the +output agree. -/ +lemma cfg_ext {c₁ c₂ : Cfg 0 Symbol Unit input} (hstate : c₁.state = c₂.state) + (hpos : c₁.inputPos = c₂.inputPos) (hout : c₁.output = c₂.output) : c₁ = c₂ := + Cfg.ext hstate hpos (funext fun i => i.elim0) (funext fun i => i.elim0) hout + +/-- Over an input symbol, the copy machine emits it and moves right. -/ +lemma step_scan {n : ℕ} (hn : n < input.length) (out : List Symbol) : + copy.step (cfg input (some ()) ⟨n + 1, by omega⟩ out) = + cfg input (some ()) ⟨n + 2, by omega⟩ (out ++ [input[n]]) := by + have hsym : (cfg input (some ()) ⟨n + 1, by omega⟩ out).inputSymbol = + some input[n] := inputSymbolInner n (by simp only [cfg]; omega) hn + unfold step + simp only [cfg] at hsym ⊢ + rw [hsym] + refine cfg_ext rfl ?_ rfl + apply Fin.ext + simp [copy, Action.apply, moveInputPos] + grind + +/-- On the blank at the right end of the input, the copy machine halts in place. -/ +lemma step_halt (out : List Symbol) : + copy.step (cfg input (some ()) ⟨input.length + 1, by omega⟩ out) = + cfg input none ⟨input.length + 1, by omega⟩ out := by + have hsym : (cfg input (some ()) ⟨input.length + 1, by omega⟩ out).inputSymbol = + none := + inputSymbol_eq_none_of_boundary (Or.inr rfl) + unfold step + simp only [cfg] at hsym ⊢ + rw [hsym] + exact cfg_ext rfl (by simp [copy, Action.apply]) (by simp [copy, Action.apply]) + +/-- After `n ≤ input.length` steps, the copy machine has copied the first `n` input symbols to the +output and its head is over the `n`-th cell of the input. -/ +lemma runFrom_scan (n : ℕ) (hn : n ≤ input.length) : + copy.runFrom (copy.initCfg input) n = + cfg input (some ()) ⟨n + 1, by omega⟩ (input.take n) := by + induction n with + | zero => exact cfg_ext rfl rfl rfl + | succ n ih => + rw [runFrom_succ_eq_step', ih (by omega), step_scan (by omega)] + have htake : input.take n ++ [input[n]] = input.take (n + 1) := by + rw [List.take_add_one, List.getElem?_eq_getElem (by omega), Option.toList_some] + rw [htake] + +/-- The complete run: after `input.length + 1` steps the copy machine has halted with the input +copied to the output. -/ +lemma runFrom_full (input : List Symbol) : + copy.runFrom (copy.initCfg input) (input.length + 1) = + cfg input none ⟨input.length + 1, by omega⟩ input := by + rw [runFrom_succ_eq_step', runFrom_scan input.length le_rfl, List.take_length, step_halt] + +/-- The copy machine outputs its input unchanged, in `input.length + 1` steps and zero space. -/ +theorem computesInTimeAndSpace (input : List Symbol) : + ComputesInTimeAndSpace copy input input (input.length + 1) 0 := + ⟨by rw [runFrom_full]; rfl, by rw [runFrom_full]; rfl, + copy.spaceUsed_zero_tapes_eq_zero _ _ rfl⟩ + +end Copy + +variable {α : Type*} + +/-- The identity function is computable in one step per input symbol and zero space. -/ +public theorem computableInTimeAndSpace_id {enc : α ↪ List Bool} : + ComputableInTimeAndSpace (id : α → α) enc enc + (fun a => (enc a).length + 1) (fun _ => 0) := + ⟨0, Unit, inferInstance, copy, fun a => + ⟨(enc a).length + 1, le_rfl, 0, le_rfl, Copy.computesInTimeAndSpace (enc a)⟩⟩ + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean index 93e8aa70f..9ee4ac964 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -141,6 +141,12 @@ lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ) cfg.inputSymbol = some input[p] := by grind [Cfg.inputSymbol] +/-- At either boundary of the input, the head reads a blank. -/ +lemma inputSymbol_eq_none_of_boundary {cfg : Cfg k Symbol State input} + (h : cfg.inputPos.val = 0 ∨ cfg.inputPos.val = input.length + 1) : + cfg.inputSymbol = none := by + grind [Cfg.inputSymbol] + /-- The symbol read by work tape `i`. -/ def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol := cfg.workTapes i (cfg.workTapePos i)