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,80 @@ 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
+
+-- TODO we have to be much more radical.
+
+
+-- private lemma succ_space_at_iter {k : ℕ} (i : Fin k)
+--     (n : ℕ) (tapes : Fin k → List (List OneTwo)) :
+--   space_at_iter (tm := succ i) (by simp) n.succ tapes = Function.update (spaceUsed_init tapes)
+--       i
+--      -- TODO 1 + output size - some shortcut?
+--       i (1 + (spaceUsed_init ((succ i).eval_list_tot (by simp) tapes) i)) := by
+--   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 => (dya (dya_inv ((tapes 0).headD []) +
+--              dya_inv ((tapes 1).headD [])) :: (tapes 2)).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₀, spaceUsed_init_simp]
+--   funext j
+--   match j with
+--   | 0 => simp [spaceUsed_init_simp]
+--   | 1 => simp [spaceUsed_init_simp]
+--   | 2 => simp [spaceUsed_init_simp]
+--          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

@@ -373,6 +373,7 @@ public def eval_tot
   Fin k → BiTape Symbol :=
 (tm.eval tapes).get (h_alwaysHalts tapes)
 
+
 end MultiTapeTM
 
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean

@@ -28,6 +28,13 @@ 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₁_spaceUsed_list {tapes : Fin 2 → List (List α)} :
+  copy₁.spaceUsed_list (by simp) 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`.
@@ -48,6 +55,16 @@ public lemma copy_eval_list
   simp_all [copy]
   grind
 
+@[simp]
+public lemma copy_spaceUsed_list {k : ℕ} (i j : Fin k)
+  (h_inj : [i, j].get.Injective := by intro x y; grind)
+  {tapes : Fin k → List (List α)} :
+  (copy i j h_inj).spaceUsed_list (by simp) tapes =
+    Function.update (Function.update (spaceUsed_init tapes)
+    i (1 + (listToString (tapes i)).length))
+    j (listToString (((tapes i).headD []) :: tapes j)).length := by
+  sorry
+
 end Routines
 
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean

@@ -35,7 +35,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 Symbol) (tapes : Fin k → BiTape Symbol) :
+public def MultiTapeTM.headStats (tm : MultiTapeTM k Symbol) (tapes : Fin k → BiTape Symbol) :
   Part (Fin k → HeadStats) := sorry
 
 /-- Execute a Turing machine and also compute head statistics. -/
@@ -53,7 +53,16 @@ def seq_combine_stats (stats₁ stats₂ : Fin k → HeadStats) : Fin k → Head
     final₁ + final₂,
     by omega⟩
 
-lemma seq_evalWithStats (tm₁ tm₂ : MultiTapeTM k Symbol) (tapes : Fin k → BiTape Symbol) (i : Fin k) :
+lemma seq_stats (tm₁ tm₂ : MultiTapeTM k Symbol) (tapes : Fin k → BiTape Symbol) (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 Symbol)
+    (tapes : Fin k → BiTape Symbol)
+    (i : Fin k) :
   (seq tm₁ tm₂).evalWithStats tapes = do
       let (tapes', stats₁) ← tm₁.evalWithStats tapes
       let (tapes'', stats₂) ← tm₂.evalWithStats tapes'

Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean

@@ -31,5 +31,16 @@ 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 (by simp [isZero]) tapes = 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 [isZero, spaceUsed_init_simp]
+  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₀ := PUnit.unit
   tr _ syms := sorry
 
+@[simp]
+public theorem ite_halts
+  {i : Fin k}
+  {tm₁ tm₂ : MultiTapeTM k (WithSep α)}
+  (h_tm₁_halts : ∀ tapes, tm₁.HaltsOnLists tapes)
+  (h_tm₂_halts : ∀ tapes, tm₂.HaltsOnLists tapes) :
+  ∀ tapes, (ite i tm₁ tm₂).HaltsOnLists tapes := by
+  sorry
+
 @[simp, grind =]
 public theorem ite_eval_list
   {i : Fin k}
@@ -35,6 +44,20 @@ 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 α)}
+  (h_tm₁_halts : ∀ tapes, tm₁.HaltsOnLists tapes)
+  (h_tm₂_halts : ∀ tapes, tm₂.HaltsOnLists tapes)
+  {tapes : Fin k → List (List α)} :
+  (ite i tm₁ tm₂).spaceUsed_list (by simp [h_tm₁_halts, h_tm₂_halts]) tapes =
+    if (tapes i).headD [] = [] then
+      tm₂.spaceUsed_list h_tm₂_halts tapes
+    else
+      tm₁.spaceUsed_list h_tm₁_halts tapes := by
+  sorry
+
 end Routines
 
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean

@@ -56,6 +56,18 @@ public def stringToList (s : List (Option (WithSep Symbol))) : Option (List (Lis
         | w :: rest => some ((c :: w) :: rest)))
   (some [])
 
+@[simp, grind =]
+public theorem listToString_length_nil :
+    (listToString ([] : List (List Symbol))).length = 0 := by
+  simp [listToString]
+
+@[simp, grind =]
+public theorem listToString_length_cons
+    (w : List Symbol) (ls : List (List Symbol)) :
+    (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 Symbol)) : BiTape (WithSep Symbol) :=
   BiTape.mk₁ (listToString ls)
@@ -95,6 +107,14 @@ public def MultiTapeTM.eval_list
     Part (Fin k → List (List Symbol)) :=
   (tm.eval (listToTape ∘ tapes)).bind fun tapes => tapesToLists tapes
 
+@[simp]
+public def MultiTapeTM.HaltsOnLists_of_evalList_eq_some
+    (tm : MultiTapeTM k (WithSep Symbol))
+    (tapes : Fin k → List (List Symbol))
+    (h_eval : (tm.eval_list tapes).Dom) :
+  tm.HaltsOnLists tapes := by
+  sorry
+
 @[simp]
 public theorem MultiTapeTM.HaltsOnLists_of_eval_list
     {tm : MultiTapeTM k (WithSep Symbol)}
@@ -121,6 +141,15 @@ public def MultiTapeTM.eval_list_tot
   Fin k → List (List Symbol) :=
     (tm.eval_list tapes).get (tm.eval_list_dom_of_halts_on_lists (h_alwaysHalts tapes))
 
+@[simp]
+public lemma MultiTapeTM.eval_list_tot_eq
+    (tm : MultiTapeTM k (WithSep Symbol))
+    (h_alwaysHalts : ∀ tapes, tm.HaltsOnLists tapes)
+    (tapes : Fin k → List (List Symbol)) :
+  (tm.eval_list_tot) h_alwaysHalts tapes =
+    (tm.eval_list tapes).get (tm.eval_list_dom_of_halts_on_lists (h_alwaysHalts tapes)) := by
+  simp
+
 @[simp, grind =]
 public theorem MultiTapeTM.extend_eval_list
     {k₁ k₂ : ℕ} {h_le : k₁ ≤ k₂}
@@ -155,6 +184,20 @@ public theorem MultiTapeTM.with_tapes_eval_list
 --     (ts : (Fin k → List (List Symbol)) × (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.
@@ -165,6 +208,35 @@ public theorem MultiTapeTM.with_tapes_eval_list
 --     Part ((Fin k → List (List Symbol)) × (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 def MultiTapeTM.spaceUsed_list
+    (tm : MultiTapeTM k (WithSep Symbol))
+    (h_halts : ∀ tapes, tm.HaltsOnLists tapes := by simp)
+    (tapes : Fin k → List (List Symbol)) : 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 Symbol)) : Fin k → ℕ := fun i =>
+  (listToString (tapes i)).length
+
+public def spaceUsed_init_simp (tapes : Fin k → List (List Symbol)) (i : Fin k) :
+  spaceUsed_init tapes i = (listToString (tapes i)).length := by simp [spaceUsed_init]
+
+@[simp]
+public lemma spaceUsed_init_le_spaceUsed
+  {tm : MultiTapeTM k (WithSep Symbol)}
+  (h_halts : ∀ tapes, tm.HaltsOnLists tapes := by simp)
+  (tapes : Fin k → List (List Symbol))
+  (i : Fin k) :
+  spaceUsed_init tapes i ≤ MultiTapeTM.spaceUsed_list tm h_halts tapes 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
@@ -215,4 +287,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
+  {Symbol : Type} [Fintype Symbol] [Inhabited Symbol]
+  {k₁ k₂ : ℕ}
+  {tm : MultiTapeTM k₁ (WithSep Symbol)} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective}
+  {tapes : Fin k₂ → List (List Symbol)} :
+  (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