refactor(MultiTape): simulate machines through adapters

Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean

@@ -60,6 +60,7 @@ the sub-linear space modifications from chapter 2.5 with the following changes:
     output tape
 * `Action`: what a machine does in one step
 * `Action.apply`: the effect of one action on a configuration
+* `HeadSymbols`, `Cfg.headSymbols`: the symbols under the heads, which a transition reads
 * `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in
 
 ## References
@@ -198,6 +199,19 @@ lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ)
 def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol :=
   cfg.workTapes i (cfg.workTapePos i)
 
+/-- The symbols under the heads of a machine with `k` work tapes, which its transitions read. -/
+@[ext]
+structure HeadSymbols (k : ℕ) (Symbol : Type*) where
+  /-- the symbol under the input head -/
+  inputSymbol : Option Symbol
+  /-- the symbols under the work-tape heads -/
+  workTapeSymbols : Fin k → Option Symbol
+
+/-- The symbols under the heads of a configuration. -/
+@[simps]
+def Cfg.headSymbols (cfg : Cfg k Symbol State input) : HeadSymbols k Symbol :=
+  ⟨cfg.inputSymbol, cfg.workTapeSymbols⟩
+
 /-- A configuration is halted when it has no state to continue from. -/
 abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none
 
@@ -212,12 +226,6 @@ output, so prepending to it preserves steps: cf. `Turing.MultiTapeNTM.prependOut
     {State' : Type*} (q : Option State') : Cfg k Symbol State' input :=
   ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
 
-/-- Forget the control state of a configuration, keeping the input head, the work tapes, the
-work-tape heads and the output. A property of this part of a configuration makes sense for every
-machine, whatever its state type. -/
-@[simps] def Cfg.forgetState (cfg : Cfg k Symbol State input) : Cfg k Symbol Unit input :=
-  ⟨some (), cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
-
 /-- Remap the (optional) state of a configuration through `φ`, leaving the input head, the work
 tapes, the work-tape heads and the output alone. Control-flow combinators such as `seq` embed a
 sub-machine's configurations into the combined machine by exactly such a state remap. -/

Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean

@@ -31,6 +31,8 @@ We define a number of structures and concepts related to multi-tape Turing machi
     symbols to exactly one action
 * `MultiTapeTM`: the TM itself
 * `tr`, `ofTr`: the derived transition function and construction from a function
+* `adapt`: the machine run through an adapter
+* `wire`: two machines on the same tapes wired into one
 * `step`, `runFrom`: the successor configuration and iteration of this function
 * `MultiTapeNTM.RunPath.ofDeterministic`, `MultiTapeNTM.ComputationPath.ofDeterministic`:
     paths of a given length from an arbitrary or initial configuration
@@ -110,6 +112,53 @@ lemma tr_ofTr (q₀ : State)
     (ofTr q₀ tr).tr q input work = tr q input work :=
   tr_iff.mp rfl
 
+/-- The transitions of `tm` performed through `adapter`: it reads what `tm` reads through `adapter`
+and performs the adaptation of the action of `tm`. -/
+noncomputable def adaptedTr {k' : ℕ} {State' : Type*} (tm : MultiTapeTM k Symbol State)
+    (adapter : MultiTapeNTM.Adapter k k' Symbol State State') (q : State) (inp : Option Symbol)
+    (work : Fin k' → Option Symbol) : Action k' Symbol State' :=
+  adapter.action ⟨inp, work⟩ (tm.tr q (adapter.read ⟨inp, work⟩).inputSymbol
+    (adapter.read ⟨inp, work⟩).workTapeSymbols)
+
+/-- `tm` run through `adapter`, a `MultiTapeNTM.Adapter`: the adapter computes what `tm` reads
+from the symbols under the heads of the new machine, and gives the action of the new machine
+performing each action of `tm`. In state `q`, `tm.adapt adapter` performs the adaptation of the
+action of `tm` in `q` on what the adapter reads. -/
+noncomputable def adapt {k' : ℕ} (tm : MultiTapeTM k Symbol State)
+    (adapter : MultiTapeNTM.Adapter k k' Symbol State State) : MultiTapeTM k' Symbol State :=
+  ofTr tm.q₀ (tm.adaptedTr adapter)
+
+/-- `tm.adapt adapter` follows `tm`. -/
+lemma Adapt.follows {k' : ℕ} {adapter : MultiTapeNTM.Adapter k k' Symbol State State} :
+    (tm.adapt adapter).Follows tm id adapter :=
+  fun _ _ _ h => tr_iff.mp h ▸ rfl
+
+/-- `tm₀` and `tm₁` wired into one machine on their shared tapes, which starts in `q₀`: in a state
+`inl q` it performs the transition of `tm₀` in `q`, and in `inr q` that of `tm₁`. The wires `next₀`
+and `next₁` say where the steps of each machine lead: within the same machine, to the other
+machine, or to halting. -/
+noncomputable def wire {State₀ State₁ : Type*} (tm₀ : MultiTapeTM k Symbol State₀)
+    (tm₁ : MultiTapeTM k Symbol State₁) (next₀ : Option State₀ → Option (State₀ ⊕ State₁))
+    (next₁ : Option State₁ → Option (State₀ ⊕ State₁)) (q₀ : State₀ ⊕ State₁) :
+    MultiTapeTM k Symbol (State₀ ⊕ State₁) :=
+  ofTr q₀ fun q => q.elim (tm₀.adaptedTr (.mapState next₀)) (tm₁.adaptedTr (.mapState next₁))
+
+namespace Wire
+
+variable {State₀ State₁ : Type*} {tm₀ : MultiTapeTM k Symbol State₀}
+  {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)}
+  {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁}
+
+/-- In its states `inl q`, the wiring follows `tm₀`, its steps leading along `next₀`. -/
+lemma follows_left : (wire tm₀ tm₁ next₀ next₁ q₀).Follows tm₀ .inl (.mapState next₀) :=
+  fun _ _ _ h => tr_iff.mp h ▸ rfl
+
+/-- In its states `inr q`, the wiring follows `tm₁`, its steps leading along `next₁`. -/
+lemma follows_right : (wire tm₀ tm₁ next₀ next₁ q₀).Follows tm₁ .inr (.mapState next₁) :=
+  fun _ _ _ h => tr_iff.mp h ▸ rfl
+
+end Wire
+
 /-!
 ## Stepping a Turing Machine
 
@@ -169,27 +218,6 @@ lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) :
     tm.step cfg = cfg :=
   step_iff.mp ((MultiTapeNTM.step_of_halt h).mpr rfl)
 
-/-- A configuration map semiconjugating the step functions is a homomorphism of the step relations,
-so it maps run paths with `RelSeries.map`. -/
-def stepHom {k' : ℕ} {State' : Type*} {input' : List Symbol}
-    {tm' : MultiTapeTM k' Symbol State'}
-    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
-    (h : Function.Semiconj f tm.step tm'.step) :
-    (tm.stepRel input).Hom (tm'.stepRel input') where
-  toFun := f
-  map_rel' hc := step_iff.mpr ((h _).symm.trans (congrArg f (step_iff.mp hc)))
-
-/-- A configuration map commuting with the step functions on running configurations is a
-homomorphism from the running steps of `tm` to the steps of `tm'`. -/
-@[simps! apply]
-def runningStepHom {k' : ℕ} {State' : Type*} {input' : List Symbol}
-    {tm' : MultiTapeTM k' Symbol State'}
-    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
-    (h : ∀ c, ¬c.Halted → tm'.step (f c) = f (tm.step c)) :
-    (tm.runningStepRel input).Hom (tm'.stepRel input') where
-  toFun := f
-  map_rel' {c _} hc := step_iff.mpr ((h c hc.1).trans (congrArg f (step_iff.mp hc.2)))
-
 end MultiTapeTM
 
 namespace MultiTapeNTM

Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean

@@ -39,6 +39,10 @@ requires every path of at least `t` steps to end in a halted configuration.
 * `Step`: the one-step relation on configurations
 * `RunPath`: finite relation series of steps
 * `ComputationPath`: a run path starting at the initial configuration
+* `Adapter`, `Follows`: a machine follows another when it performs each of its transitions,
+  reading and acting through an adapter
+* `Follows.runningStepHom`, `Follows.stepHom`: a configuration map that agrees with the adapter is a
+  homomorphism of step relations, so it maps run paths
 * `RunsInTime`: every computation path of at least the given length ends in a halted
   configuration
 
@@ -173,20 +177,6 @@ lemma exists_running (p : ntm.RunPath input) (h : p.last.Halted) :
 
 end RunPath
 
-/-- A machine never reads its output tape, so prepending a word to the output preserves steps. -/
-@[simps]
-def prependOutputHom (ntm : MultiTapeNTM k Symbol State) (pre : List Symbol) :
-    (ntm.stepRel input).Hom (ntm.stepRel input) where
-  toFun c := c.prependOutput pre
-  map_rel' {c c'} h := by
-    change ntm.Step c c' at h
-    change ntm.Step (c.prependOutput pre) (c'.prependOutput pre)
-    unfold Step at h ⊢
-    rcases hq : c.state with _ | q <;> simp only [hq, Cfg.prependOutput_state] at h ⊢
-    · rw [h]
-    · obtain ⟨a, ha, rfl⟩ := h
-      exact ⟨a, ha, Cfg.ext rfl rfl rfl rfl (by simp [Action.apply])⟩
-
 /-- A run path starting at the initial configuration for `input`. -/
 structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol)
     extends toRunPath : ntm.RunPath input where
@@ -210,6 +200,82 @@ lemma RunsInTime.mono {input : List Symbol} {t t' : ℕ}
     (h : ntm.RunsInTime input t) (ht : t ≤ t') : ntm.RunsInTime input t' :=
   fun p hp ↦ h p (ht.trans hp)
 
+/-! ### Following a machine -/
+
+/-- How a machine with `k'` work tapes and states `State'` performs the transitions of a machine
+with `k` work tapes and states `State`. A transition turns the symbols under the heads into an
+action, so the outer machine translates both ends: `read` computes the symbols the inner machine
+reads from those under the outer heads, and `action` turns the inner action into an outer one,
+which may also depend on the outer symbols. -/
+structure Adapter (k k' : ℕ) (Symbol State State' : Type*) where
+  /-- the symbols the inner machine reads -/
+  read : HeadSymbols k' Symbol → HeadSymbols k Symbol
+  /-- the outer action performing an inner action -/
+  action : HeadSymbols k' Symbol → Action k Symbol State → Action k' Symbol State'
+
+/-- The adapter that relabels the states through `φ` and reads and acts on the same tapes. -/
+def Adapter.mapState {State' : Type*} (φ : Option State → Option State') :
+    Adapter k k Symbol State State' :=
+  ⟨id, fun _ a => { a with state := φ a.state }⟩
+
+/-- `ntm'` follows `ntm` through `adapter`, in state `state q` while `ntm` is in state `q`: whatever
+`ntm` may do in `q` on what `adapter` reads, `ntm'` may do the adapted action in `state q`. -/
+def Follows {k' : ℕ} {State' : Type*} (ntm' : MultiTapeNTM k' Symbol State')
+    (ntm : MultiTapeNTM k Symbol State) (state : State → State')
+    (adapter : Adapter k k' Symbol State State') : Prop :=
+  ∀ q heads action,
+    ntm.Tr q (adapter.read heads).inputSymbol (adapter.read heads).workTapeSymbols action →
+      ntm'.Tr (state q) heads.inputSymbol heads.workTapeSymbols (adapter.action heads action)
+
+namespace Follows
+
+variable {k' : ℕ} {State' : Type*} {input' : List Symbol} {ntm' : MultiTapeNTM k' Symbol State'}
+  {state : State → State'} {adapter : Adapter k k' Symbol State State'}
+
+/-- **A follower mirrors the running steps.** If `ntm'` follows `ntm`, and `f` sends a configuration
+in state `q` to one in state `state q`, from which `adapter` reads what the configuration reads and
+on which each adapted action acts as the action acts on the configuration, then `f` maps each
+running step of `ntm` to a step of `ntm'`. -/
+def runningStepHom (h : ntm'.Follows ntm state adapter)
+    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
+    (hstate : ∀ c q, c.state = some q → (f c).state = some (state q))
+    (hread : ∀ c, adapter.read (f c).headSymbols = c.headSymbols)
+    (haction : ∀ c action,
+      (adapter.action (f c).headSymbols action).apply (f c) = f (action.apply c)) :
+    (ntm.runningStepRel input).Hom (ntm'.stepRel input') where
+  toFun := f
+  map_rel' {c _} := fun ⟨hrunning, hstep⟩ => by
+    obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp hrunning
+    simp only [Set.mem_ofPred_eq, Step, hq, hstate c q hq] at hstep ⊢
+    obtain ⟨action, hTr, rfl⟩ := hstep
+    exact ⟨_, h q _ action (by rwa [hread]), (haction c action).symm⟩
+
+/-- **A follower mirrors the steps.** As `runningStepHom`, for an `f` that relabels every state
+through `state`, so that it also keeps halted configurations halted. -/
+def stepHom (h : ntm'.Follows ntm state adapter)
+    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
+    (hstate : ∀ c, c.state.map state = (f c).state)
+    (hread : ∀ c, adapter.read (f c).headSymbols = c.headSymbols)
+    (haction : ∀ c action,
+      (adapter.action (f c).headSymbols action).apply (f c) = f (action.apply c)) :
+    (ntm.stepRel input).Hom (ntm'.stepRel input') where
+  toFun := f
+  map_rel' {c _} hc :=
+    if hc' : c.Halted then ((step_of_halt hc').mp hc).symm ▸
+      (step_of_halt ((hstate c).symm.trans (congrArg (Option.map state) hc'))).mpr rfl
+    else (h.runningStepHom f (fun c _ hq => (hstate c).symm.trans (congrArg (Option.map state) hq))
+      hread haction).map_rel ⟨hc', hc⟩
+
+end Follows
+
+/-- A machine never reads its output tape, so prepending a word to the output preserves steps. -/
+@[simps! apply]
+def prependOutputHom (ntm : MultiTapeNTM k Symbol State) (pre : List Symbol) :
+    (ntm.stepRel input).Hom (ntm.stepRel input) :=
+  Follows.stepHom (state := id) (adapter := .mapState id) (fun _ _ _ h => h) (·.prependOutput pre)
+    (fun _ => Option.map_id_apply) (fun _ => rfl) fun _ _ =>
+      Cfg.ext rfl rfl rfl rfl (by simp [Action.apply, Adapter.mapState])
+
 end MultiTapeNTM
 
 end Turing

Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean

@@ -64,22 +64,20 @@ public theorem transformsTapes_clearWork (w : List Symbol) :
       Cfg 1 Symbol RewindWorkState input) (w.length + 2)
   have h₀ : p₀.last = _ := runFrom_forwardWork (input := input) 1 w out (zero_add _)
   have h₁ : p₁.last = _ := runFrom_rewindWork_erase (input := input) 1 (tapeOfList w) out rfl
-  obtain ⟨p, hh, hl, ht, hmem⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁) (by rw [h₀])
-    (by rw [h₀]; rfl) (by rw [h₁])
+  obtain ⟨p, hh, hl, ht, hvisited⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁) (by rw [h₀])
+    (by rw [h₀]; rfl)
   refine ⟨fun _ => [], [], ⟨rfl, rfl⟩, p, hh,
     by rw [hl, h₁]; simp [rightCfg, Cfg.mapState, wordsCfg],
     (show p.length ≤ w.length + 1 + (w.length + 2) from ht).trans (by lia), ?_⟩
-  -- every head position of the two passes is in `[-1, w.length]`
+  -- both passes keep the head within `[-1, w.length]`
   rw [MultiTapeNTM.RunPath.space, Fin.sum_univ_one]
-  refine (p.spaceUsedByTape_le_card (S := .Icc (-1) (w.length : ℤ)) fun c hc => ?_).trans
-    (by simp; lia)
-  rcases hmem c hc with ⟨_, ⟨m, rfl⟩, he⟩ | ⟨_, ⟨m, rfl⟩, he⟩ <;>
-    rw [show c.workTapePos 0 = _ from congrArg (·.workTapePos 0) he]
-  · exact Finset.mem_Icc.2 (Set.Icc_subset_Icc_left (by lia)
-      (workTapePos_runFrom_forwardWork (input := input) 1 w out (Nat.zero_le w.length) m))
-  · exact Finset.mem_Icc.2
-      (workTapePos_runFrom_rewindWork (some none) (input := input) 1 (tapeOfList w) out rfl
-        le_rfl m)
+  refine (Finset.card_le_card (t := .Icc (-1 : ℤ) w.length)
+    ((hvisited 0).trans (Finset.union_subset ?_ ?_))).trans (by simp; lia) <;>
+    refine Finset.image_subset_iff.mpr fun m _ => Finset.mem_Icc.2 ?_
+  · exact Set.Icc_subset_Icc_left (by lia)
+      (workTapePos_runFrom_forwardWork (input := input) 1 w out (Nat.zero_le w.length) m)
+  · exact workTapePos_runFrom_rewindWork (some none) (input := input) 1 (tapeOfList w) out rfl
+      le_rfl m
 
 /-! ### Clearing one of several work tapes -/