Space requirements.

Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean

@@ -16,6 +16,8 @@ public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator
 public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator
 public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
 
+import Mathlib.Tactic.FinCases
+
 namespace Turing
 
 variable {k : ℕ}
@@ -51,6 +53,88 @@ theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} :
   · simp [h]; grind
   · grind
 
+/-- The value of succ's eval_list at index j when applied via get. -/
+private lemma succ_eval_list_get_apply {k : ℕ} {i j : Fin k}
+    {tapes : Fin k → List (List OneTwo)}
+    (h : ((succ i).eval_list tapes).Dom) :
+    ((succ i).eval_list tapes).get h j =
+    (Function.update tapes i ((dya (dya_inv ((tapes i).headD [])).succ) :: (tapes i).tail)) j := by
+  sorry
+
+
+private lemma succ_space_at_iter {k : ℕ} (i : Fin k)
+    (n : ℕ) (tapes : Fin k → List (List OneTwo)) :
+  space_at_iter (tm := succ i) succ_halts n.succ tapes = Function.update (spaceUsed_init tapes)
+      i 1 + (listToString (((succ i).eval_list tapes).get (by sorry) i)).length := by
+  funext j
+  by_cases h : j = i
+  · rw [h, space_at_iter_of_mono succ_halts]
+    · simp
+      sorry
+    · intro tapes
+      exact succ_spaceUsed_mono_iter
+  · simp [h]
+    sorry
+
+
+theorem add₀_spaceUsed {tapes : Fin 6 → List (List OneTwo)} :
+  add₀.spaceUsed_list tapes (h_halts := by sorry) = fun j : Fin 6 =>
+    match j with
+    | 0 => spaceUsed_init tapes 0
+    | 1 => 1 + spaceUsed_init tapes 1
+    | 2 => max (((tapes 1).headD []).length + 1 + spaceUsed_init tapes 2)
+               ((dya (dya_inv ((tapes 1).headD [])).succ).length + 1 + spaceUsed_init tapes 2)
+    | 3 => ((tapes 0).headD []).length + 1 + spaceUsed_init tapes 3
+    | 4 => ((tapes 0).headD []).length + 1 + spaceUsed_init tapes 4
+    | 5 => ((tapes 0).headD []).length + 1 + spaceUsed_init tapes 5 := by
+  simp [add₀, copy_halts, succ_halts, loop_halts_of_halts]
+  funext j
+  match j with
+  | 0 => simp
+         rw [space_at_iter_of_constant]
+         · sorry
+         · simp
+           sorry
+         · simp
+  | 1 => sorry
+  | 2 => sorry
+  | 3 => sorry
+  | 4 => sorry
+  | 5 => sorry
+
+  -- -- Establish halting proofs for each component
+  -- have h_halts_copy : ∀ t : Fin 6 → BiTape (WithSep OneTwo),
+  --     (copy (k := 6) 1 2 (h_neq := by decide)).haltsOn t := by intro; sorry
+  -- have h_halts_loop : ∀ t : Fin 6 → BiTape (WithSep OneTwo),
+  --     (loop (h_i := by decide) (k := 3) 0 (succ (2 : Fin 3))).haltsOn t :=
+  --   loop_halts_of_halts succ_halts
+  -- -- Unfold add₀ = (copy 1 2) <;> loop 0 (succ 2), split space via seq
+  -- simp only [add₀, MultiTapeTM.seq_spaceUsed_list h_halts_copy h_halts_loop]
+  -- -- Compute the copy step's space usage and the intermediate tape state
+  -- simp only [copy_spaceUsed_list, copy_eval_list]
+  -- -- Expand the loop's space: aux tapes (≥3) get fixed formula, inner tapes (<3) use space_at_iter
+  -- simp only [loop_space_list (h_halts := succ_halts)]
+  -- -- Case analysis on tape index; apply succ_space_at_iter after j is concrete
+  -- funext ⟨j, hj⟩
+  -- match j, hj with
+  -- | 0, _ =>
+  --   simp only [succ_space_at_iter (2 : Fin 3) _ succ_halts]
+  --   simp [Function.update, Fin.ext_iff]
+  -- | 1, _ =>
+  --   simp only [succ_space_at_iter (2 : Fin 3) _ succ_halts]
+  --   simp [Function.update, Fin.ext_iff]
+  -- | 2, _ =>
+  --   simp only [succ_space_at_iter (2 : Fin 3) _ succ_halts]
+  --   simp only [succ_eval_list_get_apply, Part.get_some, Function.update,
+  --              Fin.ext_iff, listToString_length_cons]
+  --   simp (config := { decide := true }) only [if_true, dif_pos, List.headD_cons, List.tail_cons,
+  --              listToString_length_cons, spaceUsed_init_simp]
+  --   simp only [show (⟨1, (by omega : 1 < 6)⟩ : Fin 6) = 1 from rfl,
+  --              show (⟨2, (by omega : 2 < 6)⟩ : Fin 6) = 2 from rfl]
+  -- | 3, _ => simp [Function.update, Fin.ext_iff]
+  -- | 4, _ => simp [Function.update, Fin.ext_iff]
+  -- | 5, _ => simp [Function.update, Fin.ext_iff]
+
 /--
 A Turing machine that adds the heads of tapes i and j (in dyadic encoding) and pushes the result
 to tape l.

Cslib/Computability/Machines/MultiTapeTuring/Basic.lean

@@ -371,6 +371,11 @@ def OutputsWithinTime (tm : MultiTapeTM k α) (l l' : List α) (m : ℕ) :=
 --   grind [hevals.apply_le_apply_add (Cfg.space_used tm)
 --       fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)]
 
+structure MultiTapeTotalTM k α extends MultiTapeTM k α where
+  /-- The Turing machine halts on all inputs. -/
+  haltsOn : ∀ tapes, toMultiTapeTM.haltsOn tapes
+
+
 end MultiTapeTM
 
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean

@@ -27,6 +27,19 @@ lemma copy₁_eval_list {tapes : Fin 2 → List (List α)} :
     Part.some (Function.update tapes 1 (((tapes 0).headD []) :: tapes 1)) := by
   sorry
 
+@[simp]
+lemma copy₁_halts {tapes : Fin 2 → BiTape (WithSep α)} :
+  copy₁.haltsOn tapes := by
+  sorry
+
+@[simp]
+lemma copy₁_spaceUsed_list {tapes : Fin 2 → List (List α)} :
+  copy₁.spaceUsed_list tapes = Function.update (Function.update (spaceUsed_init tapes)
+    0 (1 + (listToString (tapes 0)).length))
+    1 (listToString (((tapes 0).headD []) :: tapes 1)).length := by
+  sorry
+
+
 /--
 A Turing machine that copies the first word on tape `i` to tape `j`.
 If Tape `i` is empty, pushes the empty word to tape `j`.
@@ -38,6 +51,12 @@ public def copy {k : ℕ} (i j : ℕ)
   MultiTapeTM k (WithSep α) :=
   copy₁.with_tapes [⟨i, h_i_lt⟩, ⟨j, h_j_lt⟩].get (by intro x y; grind)
 
+@[simp]
+public lemma copy_halts {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k}
+  {tapes : Fin k → BiTape (WithSep α)} :
+  (copy i j (h_neq := h_neq) (h_i_lt) (h_j_lt)).haltsOn tapes = true := by
+  simp [copy]
+
 @[simp, grind =]
 public lemma copy_eval_list
   {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k}
@@ -48,6 +67,18 @@ public lemma copy_eval_list
   have h_inj : [(⟨i, h_i_lt⟩ : Fin k), ⟨j, h_j_lt⟩].get.Injective := by intro x y; grind
   simp_all [copy]
 
+@[simp]
+public lemma copy_spaceUsed_list
+  {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k}
+  {tapes : Fin k → List (List α)} :
+  (copy i j h_neq h_i_lt h_j_lt).spaceUsed_list tapes (by simp [copy]) =
+    Function.update (Function.update (spaceUsed_init tapes)
+    ⟨i, h_i_lt⟩ (1 + (listToString (tapes ⟨i, h_i_lt⟩)).length))
+    ⟨j, h_j_lt⟩ (listToString (((tapes ⟨i, h_i_lt⟩).headD []) :: tapes ⟨j, h_j_lt⟩)).length := by
+  have h_inj : [(⟨i, h_i_lt⟩ : Fin k), ⟨j, h_j_lt⟩].get.Injective := by intro x y; grind
+  simp_all [copy, apply_updates_function]
+  grind
+
 end Routines
 
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean

@@ -37,7 +37,7 @@ public def HeadStats.space (hs : HeadStats) : ℕ :=
 
 
 /-- Compute the head statistics for a turing machine starting with a certain tape configuration. -/
-public def headStats (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) :
+public def MultiTapeTM.headStats (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) :
   Part (Fin k → HeadStats) := sorry
 
 /-- Execute a Turing machine and also compute head statistics. -/
@@ -55,6 +55,12 @@ def seq_combine_stats (stats₁ stats₂ : Fin k → HeadStats) : Fin k → Head
     final₁ + final₂,
     by omega⟩
 
+lemma seq_stats (tm₁ tm₂ : MultiTapeTM k α) (tapes : Fin k → BiTape α) (i : Fin k) :
+  (seq tm₁ tm₂).headStats tapes = do
+      let stats₁ ← tm₁.headStats tapes
+      let stats₂ ← tm₂.headStats tapes'
+      return seq_combine_stats stats₁ stats₂ := by sorry
+
 lemma seq_evalWithStats (tm₁ tm₂ : MultiTapeTM k α) (tapes : Fin k → BiTape α) (i : Fin k) :
   (seq tm₁ tm₂).evalWithStats tapes = do
       let (tapes', stats₁) ← tm₁.evalWithStats tapes

Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean

@@ -31,5 +31,27 @@ public theorem isZero_eval_list {i : Fin k} {tapes : Fin k → List (List OneTwo
   simp [isZero]
   grind
 
+@[simp]
+public theorem isZero_spaceUsed_list {i j : Fin k} {tapes : Fin k → List (List OneTwo)} :
+  (isZero i).spaceUsed_list tapes (by simp [isZero]) = Function.update (spaceUsed_init tapes) i
+    (if (tapes i).headD [] = [] then
+      (listToString ([OneTwo.one] :: (tapes i).tail)).length
+    else
+      (listToString (tapes i)).length) := by
+  simp only [isZero, ite_spaceUsed_list]
+  by_cases h : j = i
+  · simp only [List.headD_eq_head?_getD, pop_halts, implies_true, push_halts_on,
+    MultiTapeTM.seq_spaceUsed_list, pop_spaceUsed, pop_eval_list, Part.get_some,
+    push_spaceUsed_list, Function.update_self, listToString_length_cons, List.length_cons,
+    List.length_nil, zero_add, Nat.reduceAdd]
+    sorry
+    -- cases (tapes i) with
+    -- | nil =>  grind
+    -- | cons hd tl => grind
+  · simp [h]
+    -- grind
+    sorry
+
+
 end Routines
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean

@@ -26,6 +26,15 @@ public def ite (i : Fin k) (tm₁ tm₂ : MultiTapeTM k (WithSep α)) :
   q₀ := 0
   M _ syms := sorry
 
+@[simp]
+public theorem ite_halts
+  {i : Fin k}
+  {tm₁ tm₂ : MultiTapeTM k (WithSep α)}
+  (h_tm₁_halts : ∀ tapes, tm₁.haltsOn tapes)
+  (h_tm₂_halts : ∀ tapes, tm₂.haltsOn tapes) :
+  ∀ tapes, (ite i tm₁ tm₂).haltsOn tapes := by
+  sorry
+
 @[simp, grind =]
 public theorem ite_eval_list
   {i : Fin k}
@@ -35,6 +44,18 @@ public theorem ite_eval_list
     if (tapes i).headD [] = [] then tm₂.eval_list tapes else tm₁.eval_list tapes := by
   sorry
 
+@[simp]
+public theorem ite_spaceUsed_list
+  {i : Fin k}
+  {tm₁ tm₂ : MultiTapeTM k (WithSep α)}
+  {tapes : Fin k → List (List α)} :
+  (ite i tm₁ tm₂).spaceUsed_list tapes sorry =
+    if (tapes i).headD [] = [] then
+      tm₂.spaceUsed_list tapes sorry
+    else
+      tm₁.spaceUsed_list tapes sorry := by
+  sorry
+
 end Routines
 
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean

@@ -42,6 +42,18 @@ of the resulting string (if the list is non-empty). -/
 public def listToString (ls : List (List α)) : List (WithSep α) :=
   (ls.map (fun w : List α => (w.map .ofChar) ++ [.comma])).flatten
 
+@[simp, grind =]
+public theorem listToString_length_nil :
+    (listToString ([] : List (List α))).length = 0 := by
+  simp [listToString]
+
+@[simp, grind =]
+public theorem listToString_length_cons
+    (w : List α) (ls : List (List α)) :
+    (listToString (w :: ls)).length = w.length + 1 + (listToString ls).length := by
+  simp [listToString]
+  grind
+
 /-- Encodes a list of words into a tape. -/
 public def listToTape (ls : List (List α)) : BiTape (WithSep α) :=
   BiTape.mk₁ (listToString ls)
@@ -118,6 +130,20 @@ def MultiTapeTM.TransformsListsWithStats
     (ts : (Fin k → List (List α)) × (Fin k → HeadStats)) : Prop :=
     tm.evalWithStats (listToTape ∘ tapes) = .some (listToTape ∘ ts.1, ts.2)
 
+/-- Head statistics for list computations.
+The assumption is that the head starts on the leftmost symbol of the initial tape and ends on the
+leftmost symbol of the final tape. The zero-point is the right-most non-blank symbol of the initial
+tape which is the same point as the right-most non-blank symbol of the final tape.
+The head never moves right of the zero point and it moves at most `leftmost` points left of the
+zero point. -/
+public structure HeadStatsList where
+  /-- The number of symbols on the initial tape. TODO isn't this redundant? -/
+  initialLength : ℕ
+  /-- The number of symbols on the tape after termination. TODO isn't this redundant? -/
+  finalLength : ℕ
+  /-- The left-most position of the head in number of symbols left of the zero point. -/
+  leftmost : ℕ
+
 /--
 Evaluate the Turing machine `tm` on the list-encoded tapes `tapes` and also return the head
 statistics of the computation.
@@ -128,6 +154,34 @@ public noncomputable def MultiTapeTM.evalWithStats_list
     Part ((Fin k → List (List α)) × (Fin k → HeadStats)) :=
   ⟨∃ ts, tm.TransformsListsWithStats tapes ts, fun h => h.choose⟩
 
+-- TODO we could also use "tape cells moved over" or "added".
+-- the benefit is that we could say `0` if the head did not move at all or only deleted symbols.
+-- the problem is that the situation of adding symbols is more complicated.
+
+/-- The max number of tape cells the head traversed over or that contain non-blank symbols.
+Note that the head will always be left of or on the "zero" point which is the initial position
+for an empty initial tape or the rightmost non-blank cell. -/
+-- TODO we could even make this Part now.
+public noncomputable def MultiTapeTM.spaceUsed_list
+    (tm : MultiTapeTM k (WithSep α))
+    (tapes : Fin k → List (List α))
+    (h_halts : ∀ tapes, tm.haltsOn tapes := by simp) : Fin k → ℕ := sorry
+
+/-- The space initially used by a Turing machine that has the given tape configuration. -/
+public def spaceUsed_init (tapes : Fin k → List (List α)) : Fin k → ℕ := fun i =>
+  (listToString (tapes i)).length
+
+public def spaceUsed_init_simp (tapes : Fin k → List (List α)) (i : Fin k) :
+  spaceUsed_init tapes i = (listToString (tapes i)).length := by simp [spaceUsed_init]
+
+@[simp]
+public lemma spaceUsed_init_le_spaceUsed {k : ℕ} {α : Type}
+  {tm : MultiTapeTM k (WithSep α)}
+  (tapes : Fin k → List (List α))
+  (i : Fin k) :
+  spaceUsed_init tapes i ≤ MultiTapeTM.spaceUsed_list tm tapes sorry i := by
+  sorry
+
 -- TODO for machines running on lists, we can actually have more precise head stats:
 -- we know (and should enforce) that the head never moves to the right of the rightmost symbol
 -- and always starts and ends on the leftmost symbol (and if the tape is empty, it never moves
@@ -176,4 +230,13 @@ public lemma dya_inv_dya (n : ℕ) : dya_inv (dya n) = n := by sorry
 @[simp, grind =]
 public lemma dya_dya_inv (w : List OneTwo) : dya (dya_inv w) = w := by sorry
 
+@[simp, grind =]
+public theorem MultiTapeTM.with_tapes_spaceUsed
+  {α : Type} [Fintype α] [Inhabited α]
+  {k₁ k₂ : ℕ}
+  {tm : MultiTapeTM k₁ (WithSep α)} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective}
+  {tapes : Fin k₂ → List (List α)} :
+  (tm.with_tapes f h_inj).spaceUsed_list tapes (h_halts := sorry) =
+    apply_updates (spaceUsed_init tapes) (tm.spaceUsed_list (tapes ∘ f) (h_halts := sorry)) f := by
+  sorry
 end Turing