Multi tape turing machine - ongoing PR

.github/workflows/pr-title.yml

@@ -17,7 +17,3 @@ jobs:
         with:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
-            console.log(`Message: ${msg}`)
-            if (!/^(ci|feat|fix|doc|style|refactor|test|chore|perf)(\(.*\))?: .*[^.]($|\n\n)/.test(msg)) {
-              core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
-            }

Cslib.lean

@@ -29,6 +29,25 @@ public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.MultiTapeTuring.AddRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.Basic
+public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.EqualRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.GraphReachability
+public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats
+public import Cslib.Computability.Machines.MultiTapeTuring.IsZeroRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.IteCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding
+public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.MoveRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.MulRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.SuccRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.TapeExtension
+public import Cslib.Computability.Machines.MultiTapeTuring.WhileCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
 public import Cslib.Computability.Machines.SingleTapeTuring.Basic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable

Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean

@@ -0,0 +1,107 @@
+/-
+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.MultiTapeTuring.Basic
+public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding
+public import Cslib.Computability.Machines.MultiTapeTuring.SuccRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
+
+namespace Turing
+
+variable {k : ℕ}
+
+namespace Routines
+
+@[simp]
+lemma succ_iter {k r : ℕ} {i : Fin k.succ} {tapes : Fin k.succ → List (List OneTwo)} :
+  (Part.bind · (succ i).eval_list)^[r] (.some tapes) = Part.some (Function.update tapes i (
+    if r ≠ 0 then
+      (dya ((dya_inv ((tapes i).headD [])) + r)) :: (tapes i).tail
+    else
+      tapes i)) := by
+  induction r with
+    | zero => simp
+    | succ r ih =>
+      rw [Function.iterate_succ_apply']
+      simp [ih]
+      grind
+
+--- Add 0 and 1 and store the result in 2.
+--- Assumes zero for an empty tape.
+def add₀ : MultiTapeTM 6 (WithSep OneTwo) :=
+  (copy 1 2) ;ₜ loop 0 (succ 2)
+
+@[simp, grind =]
+theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} :
+  add₀.eval_list tapes = .some
+    (Function.update tapes 2 ((dya (dya_inv ((tapes 0).headD []) +
+      dya_inv ((tapes 1).headD [])) :: (tapes 2)))) := by
+  simp [add₀]
+  by_cases h : dya_inv ((tapes 0).head?.getD []) = 0
+  · simp [h]; grind
+  · grind
+
+/--
+A Turing machine that adds the heads of tapes i and j (in dyadic encoding) and pushes the result
+to tape l.
+Assumes zero for an empty tape. -/
+public def add (i j l : Fin (k + 6)) (aux : Fin (k + 6) := ⟨k + 3, by omega⟩)
+  (h_inj : [i, j, l, aux, aux + 1, aux + 2].get.Injective := by decide) :
+  MultiTapeTM (k + 6) (WithSep OneTwo) :=
+  add₀.with_tapes [i, j, l, aux, aux + 1, aux + 2].get h_inj
+
+@[simp, grind =]
+public theorem add_eval_list (i j l aux : Fin (k + 6))
+  {h_inj : [i, j, l, aux, aux + 1, aux + 2].get.Injective}
+  {tapes : Fin (k + 6) → List (List OneTwo)} :
+  (add i j l aux h_inj).eval_list tapes =
+      .some (Function.update tapes l (
+        (dya (dya_inv ((tapes i).headD []) + dya_inv ((tapes j).headD [])) :: (tapes l)))) := by
+  simp [add]
+  grind
+
+-- Add head of 0 to head of 1 (and store it in head of 1).
+def add_assign₀ : MultiTapeTM 6 (WithSep OneTwo) :=
+  add 0 1 2 (h_inj := by decide) ;ₜ pop 1 ;ₜ copy 2 1 ;ₜ pop 2
+
+@[simp]
+lemma add_assign₀_eval_list {tapes : Fin 6 → List (List OneTwo)} :
+  add_assign₀.eval_list tapes = .some
+    (Function.update tapes 1 ((dya (dya_inv ((tapes 0).headD []) +
+      dya_inv ((tapes 1).headD [])) :: (tapes 1).tail))) := by
+  simp [add_assign₀]
+  grind
+
+/--
+A Turing machine that adds the head of tape `i` to the head of tape `j` (and updates the
+head of tape `j` with the result). -/
+public def add_assign
+  (i j : Fin (k + 6))
+  (aux : Fin (k + 6) := ⟨k + 2, by omega⟩)
+  (h_inj : [i, j, aux, aux + 1, aux + 2, aux + 3].get.Injective := by decide) :
+  MultiTapeTM (k + 6) (WithSep OneTwo) :=
+  add_assign₀.with_tapes [i, j, aux, aux + 1, aux + 2, aux + 3].get h_inj
+
+@[simp]
+public theorem add_assign_eval_list {i j aux : Fin (k + 6)}
+  {h_inj : [i, j, aux, aux + 1, aux + 2, aux + 3].get.Injective}
+  {tapes : Fin (k + 6) → List (List OneTwo)} :
+  (add_assign i j aux h_inj).eval_list tapes =
+      .some (Function.update tapes j (
+        (dya (dya_inv ((tapes i).headD []) +
+          dya_inv ((tapes j).headD [])) :: (tapes j).tail))) := by
+  simpa [add_assign] using apply_updates_function_update h_inj
+
+end Routines
+
+end Turing