Always-halting Turing machines

Cslib/Computability/Machines/MultiTapeTuring/Basic.lean

@@ -238,6 +238,10 @@ def TransformsTapes
     (tapes tapes' : Fin k → BiTape α) : Prop :=
   ∃ t, tm.TransformsTapesInTime tapes tapes' t
 
+/-- The Turing machine `tm` eventually halts starting from any initial tape configuration. -/
+def haltsOn (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) : Prop :=
+  ∃ tapes', tm.TransformsTapes tapes tapes'
+
 @[scoped grind =]
 lemma relatesInSteps_iff_step_iter_eq_some
     (tm : MultiTapeTM k α)
@@ -294,6 +298,13 @@ public noncomputable def eval (tm : MultiTapeTM k α) (tapes : Fin k → BiTape
     Part (Fin k → BiTape α) :=
   ⟨∃ tapes', tm.TransformsTapes tapes tapes', fun h => h.choose⟩
 
+/--
+Execute the Turing machine `tm` on initial tapes `tapes` given a proof that it always halts
+and thus this yields a total function. -/
+public noncomputable def eval_tot (tm : MultiTapeTM k α) {h : ∀ tapes, tm.haltsOn tapes}
+  (tapes : Fin k → BiTape α) : Fin k → BiTape α :=
+  (tm.eval tapes).get (h tapes)
+
 -- TODO use MultiTapeTM.configurations?
 -- TODO this is a simple consequence of relatesInSteps_iff_configurations_eq_some, maybe not needed.
 lemma configurations_of_transformsTapesInTime

Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean

@@ -53,12 +53,34 @@ public def MultiTapeTM.TransformsLists
     (tapes tapes' : Fin k → List (List α)) : Prop :=
   tm.TransformsTapes (listToTape ∘ tapes) (listToTape ∘ tapes')
 
+/-- The Turing machine `tm` halts starting with list-encoded tapes `tapes`. -/
+public def MultiTapeTM.HaltsOnLists
+    (tm : MultiTapeTM k (WithSep α))
+    (tapes : Fin k → List (List α)) : Prop :=
+  ∃ tapes', tm.TransformsLists tapes tapes'
+
 /-- Execute the Turing machine `tm` on the list-encoded tapes `tapes`. -/
 public noncomputable def MultiTapeTM.eval_list
     (tm : MultiTapeTM k (WithSep α))
     (tapes : Fin k → List (List α)) :
     Part (Fin k → List (List α)) :=
-  ⟨∃ tapes', tm.TransformsLists tapes tapes', fun h => h.choose⟩
+  ⟨tm.HaltsOnLists tapes, fun h => h.choose⟩
+
+public theorem MultiTapeTM.HaltsOnLists_of_eval_list
+    {tm : MultiTapeTM k (WithSep α)}
+    {tapes : Fin k → List (List α)}
+    (h_dom : (tm.eval_list tapes).Dom) :
+    tm.HaltsOnLists tapes := by
+  simpa using h_dom
+
+/-- Execute the Turing machine `tm` knowing that it always halts, thus yielding a total function
+on the tapes. -/
+public noncomputable def MultiTapeTM.eval_list_tot
+  (tm : MultiTapeTM k (WithSep α))
+  (h_alwaysHalts : ∀ tapes, tm.HaltsOnLists tapes)
+  (tapes : Fin k → List (List α)) :
+  Fin k → List (List α) :=
+  (tm.eval_list tapes).get (h_alwaysHalts tapes)
 
 @[simp, grind =]
 public theorem MultiTapeTM.extend_eval_list

Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean

@@ -50,14 +50,14 @@ public def doWhile (i : Fin k) (tm : MultiTapeTM k (WithSep α)) :
   M _ syms := sorry
 
 @[simp]
-public theorem doWhile_eval
-  (i : Fin k)
-  (tm : MultiTapeTM k (WithSep α))
-  (tapes_seq : ℕ → Fin k → List (List α))
-  (h_transform : ∀ j, tm.eval_list (tapes_seq j) = .some (tapes_seq j.succ))
-  (h_nonempty : ∀ j, tapes_seq j i ≠ [])
-  (h_stops : ∃ m, (tapes_seq m i).head (h_nonempty m) = []) :
-  (doWhile i tm).eval_list (tapes_seq 0) = .some (tapes_seq (Nat.find h_stops)) := by
+public theorem doWhile_eval_list
+  {i : Fin k}
+  {tm : MultiTapeTM k (WithSep α)}
+  {tapes : Fin k → List (List α)}
+  (h_halts : ∀ tapes', tm.HaltsOnLists tapes') :
+  (doWhile i tm).eval_list tapes =
+    ⟨∃ n, ((tm.eval_list_tot h_halts)^[n] tapes i).head?.getD [] = [],
+      fun h_loopEnds => (tm.eval_list_tot h_halts)^[Nat.find h_loopEnds] tapes⟩ := by
   sorry
 
 end Routines