feat(Computability/MultiTapeTM): input/output tape predicates

Cslib.lean

@@ -50,6 +50,7 @@ public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
+public import Cslib.Foundations.Data.BiTape.Canonical
 public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update

Cslib/Computability/Machines/TuringCommon.lean

@@ -6,6 +6,7 @@ Authors: Bolton Bailey, Pim Spelier, Daan van Gent
 
 module
 
+public import Cslib.Init
 public import Mathlib.Computability.TuringMachine.Tape
 
 @[expose] public section
@@ -25,4 +26,114 @@ deriving Inhabited
 
 instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance
 
+namespace Stmt
+
+variable {Symbol : Type}
+
+/--
+A `Stmt` is *write-only* if it either writes a blank and stays put, or writes a non-blank
+symbol and moves the head right.
+
+A transition function that produces only write-only `Stmt`s on a given tape implements a
+"write-only output tape" in the sense of Arora–Barak when started from a blank output
+tape: the head remains on the first blank cell after the output, and the tape content to
+the left of the head is the reverse of the sequence of non-blank writes.
+
+Note that the "write a blank, move right" case is deliberately excluded: on a write-only
+output tape, blanks only appear in cells the head has not yet visited. Admitting blank
+writes would break the "left of the head is the reverse of the emitted output" reading.
+-/
+def IsWriteOnly (s : Stmt Symbol) : Prop :=
+  (s.symbol = none ∧ s.movement = none) ∨
+    (s.symbol.isSome ∧ s.movement = some .right)
+
+/--
+A `Stmt` is *read-preserving with respect to the currently read symbol `r`* if it writes
+back exactly what it read. The head is free to move in either direction (or stay).
+
+A transition function that produces only read-preserving `Stmt`s on a given tape never
+modifies that tape. This is the syntactic half of the classical "two-way read-only input
+tape" condition; the complementary *boundedness* property—that the head stays within the
+input region plus at most one cell on either side—cannot be stated purely on the
+transition function (a transition reading a blank cannot distinguish the left blank from
+the right blank) and is left to a separate predicate.
+-/
+def IsReadPreserving (r : Option Symbol) (s : Stmt Symbol) : Prop :=
+  s.symbol = r
+
+end Stmt
+
+/-! ## Syntactic predicates on multi-tape transition functions
+
+These predicates characterise reachability patterns in the finite control of a transition
+function `tr` of the multi-tape shape, independently of any wrapping machine structure.
+They are used to phrase head-boundedness of designated input tapes syntactically.
+-/
+
+variable {State Symbol : Type} {k : ℕ}
+
+/--
+A transition function is *read-preserving on tape `i`* if every transition writes back the
+symbol read on tape `i`.
+-/
+def IsReadPreservingOnTape
+    (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State))
+    (i : Fin k) : Prop :=
+  ∀ q reads, ((tr q reads).1 i).symbol = reads i
+
+/--
+State `q` is *harmful in direction `d`* on tape index `i` of transition function `tr` if some
+transition from `q` reads a blank on tape `i` and moves the head on tape `i` in direction `d`.
+
+These are the states whose firing would step the head one cell further past an end of the
+input region.
+-/
+def MovesOffBlankInDir
+    (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State))
+    (i : Fin k) (d : Dir) (q : State) : Prop :=
+  ∃ reads, reads i = none ∧ ((tr q reads).1 i).movement = some d
+
+/--
+`MoveThenStays tr i d q q'` holds if `q'` is reachable from `q` by a tape-`i` trajectory
+of the form `q →[move in direction d] q₁ →[stay while reading blank]* q'`.
+
+The initial transition's read is unconstrained — the head may have been on an input cell
+before stepping out to the blank — but every subsequent transition keeps the head fixed at
+the blank, hence reads blank on tape `i`, writes the blank back, and produces no movement
+on tape `i`.
+-/
+inductive MoveThenStays
+    (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State))
+    (i : Fin k) (d : Dir) : State → State → Prop where
+  /-- Single move in direction `d`, with no constraint on the read. -/
+  | move (q q' : State) (reads : Fin k → Option Symbol)
+      (h_mov : ((tr q reads).1 i).movement = some d)
+      (h_next : (tr q reads).2 = some q') :
+      MoveThenStays tr i d q q'
+  /-- Extend an existing chain by a stay-move while reading blank on tape `i`. -/
+  | stay (q q' q'' : State)
+      (h_prev : MoveThenStays tr i d q q')
+      (reads : Fin k → Option Symbol)
+      (h_reads : reads i = none)
+      (h_write : ((tr q' reads).1 i).symbol = none)
+      (h_mov : ((tr q' reads).1 i).movement = none)
+      (h_next : (tr q' reads).2 = some q'') :
+      MoveThenStays tr i d q q''
+
+/--
+Transition function `tr` is *bounded in direction `d`* on tape `i` if no chain of the form
+"move in direction `d`, then stay-on-blank repeatedly, then move in direction `d` again"
+exists. Equivalently: no harmful state in direction `d` is reachable via a post-`d`-move
+stay-on-blank chain.
+
+This is the syntactic condition we use to keep the head within the input region (plus one
+cell on either side): once the head steps off the input in direction `d`, it cannot step
+further in direction `d` without returning first. The condition is finitary — both the
+reachability relation and the existential in `MovesOffBlankInDir` range over finite types.
+-/
+def IsBoundedInDirectionOnTape
+    (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State))
+    (i : Fin k) (d : Dir) : Prop :=
+  ∀ q q', MoveThenStays tr i d q q' → ¬ MovesOffBlankInDir tr i d q'
+
 end Turing

Cslib/Foundations/Data/BiTape.lean

@@ -7,6 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Foundations.Data.StackTape
+public import Mathlib.Algebra.Group.End
 public import Mathlib.Computability.TuringMachine.Tape
 public import Mathlib.Data.Finset.Attr
 public import Mathlib.Tactic.SetLike
@@ -44,6 +45,7 @@ namespace Turing
 A structure for bidirectionally-infinite Turing machine tapes
 that eventually take on blank `none` values
 -/
+@[ext]
 structure BiTape (Symbol : Type) where
   /-- The symbol currently under the tape head -/
   head : Option Symbol
@@ -114,13 +116,95 @@ lemma move_left_move_right (t : BiTape Symbol) : t.move_left.move_right = t := b
 lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by
   simp [move_left, move_right]
 
+@[simp]
+lemma move_left_nil : (nil : BiTape Symbol).move_left = nil := rfl
+
+@[simp]
+lemma move_right_nil : (nil : BiTape Symbol).move_right = nil := rfl
+
+@[simp]
+lemma optionMove_nil (m : Option Dir) : (nil : BiTape Symbol).optionMove m = nil := by
+  cases m with
+  | none => rfl
+  | some d => cases d <;> rfl
+
+/-- The right-move equivalence, with inverse `move_left`. -/
+def moveEquiv : Equiv.Perm (BiTape Symbol) where
+  toFun := move_right
+  invFun := move_left
+  left_inv := move_right_move_left
+  right_inv := move_left_move_right
+
+/-- Move the head by an integer amount of cells: positive values move right, negative
+values move left. -/
+def move_int (t : BiTape Symbol) (delta : ℤ) : BiTape Symbol :=
+  (moveEquiv ^ delta) t
+
+@[simp]
+lemma move_int_zero_eq_id (t : BiTape Symbol) :
+    t.move_int 0 = t := by
+  simp [move_int]
+
+@[simp]
+lemma move_int_one_eq_move_right (t : BiTape Symbol) :
+    t.move_int 1 = t.move_right := by
+  simp [move_int, moveEquiv]
+
+@[simp]
+lemma move_int_neg_one_eq_move_left (t : BiTape Symbol) :
+    t.move_int (-1) = t.move_left := by
+  simp [move_int, moveEquiv]
+
+@[simp]
+lemma move_int_move_right (t : BiTape Symbol) (delta : ℤ) :
+    (t.move_int delta).move_right = t.move_int (delta + 1) := by
+  change moveEquiv ((moveEquiv ^ delta) t) = (moveEquiv ^ (delta + 1)) t
+  rw [← Equiv.Perm.mul_apply, ← zpow_one_add, add_comm]
+
+@[simp]
+lemma move_int_move_left (t : BiTape Symbol) (delta : ℤ) :
+    (t.move_int delta).move_left = t.move_int (delta - 1) := by
+  change (moveEquiv (Symbol := Symbol))⁻¹ ((moveEquiv ^ delta) t) =
+    (moveEquiv ^ (delta - 1)) t
+  rw [← Equiv.Perm.mul_apply, ← zpow_neg_one, ← zpow_add]
+  rw [show -1 + delta = delta - 1 by omega]
+
+@[simp]
+lemma move_int_move_int (t : BiTape Symbol) (delta₁ delta₂ : ℤ) :
+    (t.move_int delta₁).move_int delta₂ = t.move_int (delta₁ + delta₂) := by
+  change (moveEquiv ^ delta₂) ((moveEquiv ^ delta₁) t) =
+    (moveEquiv ^ (delta₁ + delta₂)) t
+  rw [← Equiv.Perm.mul_apply, ← zpow_add, add_comm]
+
+@[simp]
+lemma move_int_nil (delta : ℤ) : (nil : BiTape Symbol).move_int delta = nil := by
+  cases delta with
+  | ofNat n =>
+      induction n with
+      | zero => simp
+      | succ n ih =>
+          rw [show Int.ofNat (n + 1) = (Int.ofNat n : ℤ) + 1 by
+            simp [Int.natCast_succ]]
+          rw [← move_int_move_right, ih, move_right_nil]
+  | negSucc n =>
+      induction n with
+      | zero => simp
+      | succ n ih =>
+          rw [show Int.negSucc (n + 1) = Int.negSucc n - 1 by
+            rw [Int.negSucc_eq, Int.negSucc_eq]
+            omega]
+          rw [← move_int_move_left, ih, move_left_nil]
+
 end Move
 
 /--
 Write a value under the head of the `BiTape`.
 -/
 def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a }
 
+@[simp]
+lemma write_head (t : BiTape Symbol) : t.write t.head = t := rfl
+
 /--
 The space used by a `BiTape` is the number of symbols
 between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`.