From 2a15f3a28e19ea5e73ebcdb9012025aab8ed5bc7 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 5 Sep 2026 17:27:05 -0400 Subject: [PATCH] feat(MultiTapeTM): redirect input and output through work tapes --- Cslib.lean | 4 + .../MultiTape/Plumbing/InputFromWorkTape.lean | 214 ++++++++++++++++++ .../Plumbing/InputFromWorkTape/Defs.lean | 126 +++++++++++ .../MultiTape/Plumbing/OutputToWorkTape.lean | 95 ++++++++ .../Turing/MultiTape/Plumbing/README.md | 2 + .../MultiTape/Plumbing/TapeContents.lean | 55 +++++ CslibTests.lean | 1 + CslibTests/MultiTapeAdapters.lean | 40 ++++ 8 files changed, 537 insertions(+) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean create mode 100644 CslibTests/MultiTapeAdapters.lean diff --git a/Cslib.lean b/Cslib.lean index 3a80ee7e10..4404ae540e 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -49,7 +49,11 @@ public import Cslib.Computability.Languages.SafetyLiveness public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape.Defs +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OutputToWorkTape public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean new file mode 100644 index 0000000000..42187a4f73 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean @@ -0,0 +1,214 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape.Defs + +/-! # Correctness of work-tape input substitution -/ + +@[expose] public section + +namespace Turing.MultiTapeTM.InputFromWorkTape + +variable {k : ℕ} {Symbol State : Type*} +variable (tm : MultiTapeTM k Symbol State) +variable {outerInput input : List Symbol} (p : Fin (outerInput.length + 2)) + +/-- The virtual work-tape position follows the clamped native input-head movement. -/ +private lemma virtualInputPos_move {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) : + virtualInputPos (moveInputPos p move) = + virtualInputPos p + (inputMode p).move move := by + cases move with + | zero => simp [InputMode.move] + | neg => + by_cases hleft : p = 0 + · rw [hleft] + simp [inputMode, InputMode.move] + · rw [moveInputPos_neg_of_ne_left p hleft] + unfold virtualInputPos + have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) + by_cases hright : p.val = input.length + 1 <;> + simp [inputMode, hleft, hright, InputMode.move] <;> omega + | pos => + by_cases hright : p.val = input.length + 1 + · have hp : p = ⟨input.length + 1, by omega⟩ := Fin.ext hright + rw [hp] + simp [inputMode, InputMode.move] + · rw [moveInputPos_pos_of_ne_right p hright] + unfold virtualInputPos + by_cases hleft : p = 0 <;> + simp [inputMode, hleft, hright, InputMode.move] + +/-- The boundary hint selected before a move is left whenever the resulting native position is +the left boundary. -/ +private lemma nextBoundary_eq_left {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) + (hmove : moveInputPos p move = 0) : + (inputMode p).nextBoundary move = .left := by + cases move <;> + simp_all [inputMode, InputMode.nextBoundary, moveInputPos] + split_ifs at hmove <;> simp_all + +/-- The boundary hint selected before a move is right whenever the resulting native position is +the right boundary. -/ +private lemma nextBoundary_eq_right {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) + (hmove : (moveInputPos p move).val = input.length + 1) : + (inputMode p).nextBoundary move = .right := by + cases move <;> + simp_all [inputMode, InputMode.nextBoundary, moveInputPos] <;> + split_ifs at * <;> simp_all <;> omega + +/-- Classifying the virtual input tape recovers the native input-head mode, provided the +boundary hint agrees at the two blank boundary cells. -/ +private lemma classifyInput_listTape {input : List Symbol} + (p : Fin (input.length + 2)) (boundary : InputBoundary) + (hleft : p = 0 → boundary = .left) + (hright : p.val = input.length + 1 → boundary = .right) : + classifyInput + (listTape input (virtualInputPos p)) boundary = + inputMode p := by + by_cases hp0 : p = 0 + · simp [hp0, hleft hp0, virtualInputPos, inputMode, + classifyInput, InputBoundary.inputMode, listTape] + rfl + · by_cases hpr : p.val = input.length + 1 + · simp [virtualInputPos, hpr, hright hpr, inputMode, hp0, + classifyInput, InputBoundary.inputMode] + · have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hp0 (Fin.ext hz)) + have hi : p.val - 1 < input.length := by omega + have hv : virtualInputPos p = (p.val - 1 : ℕ) := by + unfold virtualInputPos + omega + simp [hv, classifyInput, inputMode, hp0, hpr, hi] + +/-- Classifying the cell reached by a virtual move recovers the native clamped +input-head mode after that move. -/ +private lemma classifyInput_move {input : List Symbol} + (p : Fin (input.length + 2)) (move : SignType) : + classifyInput + (listTape input + (virtualInputPos p + (inputMode p).move move)) + ((inputMode p).nextBoundary move) = + inputMode (moveInputPos p move) := by + rw [← virtualInputPos_move p move] + apply classifyInput_listTape + · exact nextBoundary_eq_left p move + · exact nextBoundary_eq_right p move + + +/-- The simulated input symbol is exactly the symbol on the virtual tape. -/ +private lemma embed_inputSymbol (cfg : Cfg k Symbol State input) : + (if inputMode cfg.inputPos = .inside then (embed p cfg).workTapeSymbols 0 else none) = + cfg.inputSymbol := by + simp only [Cfg.workTapeSymbols, embed, Fin.cases_zero] + by_cases hleft : cfg.inputPos = 0 + · simp [inputMode, hleft, Cfg.inputSymbol] + · by_cases hright : cfg.inputPos.val = input.length + 1 + · simp [inputMode, hleft, hright, Cfg.inputSymbol] + · have hp : 0 < cfg.inputPos.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz)) + have hi : cfg.inputPos.val - 1 < input.length := by omega + have hv : virtualInputPos cfg.inputPos = (cfg.inputPos.val - 1 : ℕ) := by + unfold virtualInputPos + omega + rw [inputSymbolInner (p := cfg.inputPos.val - 1) (by omega) hi] + simp [inputMode, hleft, hright, hv, listTape, hi] + +/-- Classification restores the native boundary mode and changes no tapes. -/ +lemma step_classifyCfg (cfg : Cfg k Symbol State input) (boundary : InputBoundary) + (hmode : classifyInput (listTape input (virtualInputPos cfg.inputPos)) boundary = + inputMode cfg.inputPos) : + tm.inputFromWorkTape.step (classifyCfg p cfg boundary) = embed p cfg := by + cases hs : cfg.state with + | none => simp [step, classifyCfg, embed, hs] + | some q => + ext i z <;> + simp [step, classifyCfg, embed, inputFromWorkTape, hs, Cfg.workTapeSymbols, hmode] + +/-- The moving half of a simulated step performs the native tape actions. -/ +lemma step_embed (cfg : Cfg k Symbol State input) (q : State) (hs : cfg.state = some q) : + tm.inputFromWorkTape.step (embed p cfg) = + classifyCfg p (tm.step cfg) + ((inputMode cfg.inputPos).nextBoundary + (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove) := by + have hwork : (fun i : Fin k => (embed p cfg).workTapeSymbols i.succ) = cfg.workTapeSymbols := by + funext i + simp [embed, Cfg.workTapeSymbols] + unfold step + rw [show (embed p cfg).state = some (.run q (inputMode cfg.inputPos)) by + simp [embed, hs], hs] + simp only [inputFromWorkTape] + rw [embed_inputSymbol p cfg, hwork] + generalize htr : tm.tr q cfg.inputSymbol cfg.workTapeSymbols = out + simp only [htr] + apply Cfg.ext + · rfl + · simp [classifyCfg, embed] + · funext i z + refine Fin.cases ?_ (fun j => ?_) i + · simp [classifyCfg, embed] + · cases hw : (out.workActions j).1 <;> simp [classifyCfg, embed, hw] + · funext i + refine Fin.cases ?_ (fun j => ?_) i + · simpa [classifyCfg, embed] using (virtualInputPos_move cfg.inputPos out.inputMove).symm + · simp [classifyCfg, embed] + · rfl + +/-- Every native step is simulated in two steps, including after a native halt. -/ +lemma runFrom_two (cfg : Cfg k Symbol State input) : + tm.inputFromWorkTape.runFrom (embed p cfg) 2 = embed p (tm.step cfg) := by + cases hs : cfg.state with + | none => simp [runFrom, step, embed, hs] + | some q => + change tm.inputFromWorkTape.step (tm.inputFromWorkTape.step (embed p cfg)) = _ + rw [step_embed tm p cfg q hs] + apply step_classifyCfg + simpa only [step, hs, virtualInputPos_move] using + classifyInput_move cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove + +/-- The native run is simulated on a work tape with a factor of two in time. -/ +lemma runFrom_embed (cfg : Cfg k Symbol State input) (n : ℕ) : + tm.inputFromWorkTape.runFrom (embed p cfg) (2 * n) = embed p (tm.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => + rw [show 2 * (n + 1) = 2 * n + 2 by omega, runFrom_add, ih, + runFrom_two, runFrom_succ_eq_step'] + +/-- Odd simulation steps are classifier configurations. -/ +lemma runFrom_odd (cfg : Cfg k Symbol State input) (n : ℕ) : + ∃ boundary, tm.inputFromWorkTape.runFrom (embed p cfg) (2 * n + 1) = + classifyCfg p (tm.runFrom cfg (n + 1)) boundary := by + rw [runFrom_add, runFrom_embed] + cases hs : (tm.runFrom cfg n).state with + | none => + refine ⟨.right, ?_⟩ + change tm.inputFromWorkTape.step (embed p (tm.runFrom cfg n)) = _ + rw [runFrom_succ_eq_step', step_of_halt hs] + simp [step, embed, classifyCfg, hs] + | some q => + refine ⟨(inputMode (tm.runFrom cfg n).inputPos).nextBoundary + (tm.tr q (tm.runFrom cfg n).inputSymbol (tm.runFrom cfg n).workTapeSymbols).inputMove, ?_⟩ + change tm.inputFromWorkTape.step (embed p (tm.runFrom cfg n)) = _ + rw [step_embed tm p _ q hs, runFrom_succ_eq_step'] + +/-- The initial classifier enters the native initial configuration, also for empty input. -/ +lemma step_init : + tm.inputFromWorkTape.step (classifyCfg p (tm.initCfg input) .right) = + embed p (tm.initCfg input) := by + apply step_classifyCfg + cases input <;> + simp [classifyInput, inputMode, virtualInputPos, InputBoundary.inputMode, listTape] + +/-- A prepared work tape can replace the native input at any real input position. -/ +lemma runFrom_init (n : ℕ) : + tm.inputFromWorkTape.runFrom (classifyCfg p (tm.initCfg input) .right) (2 * n + 1) = + embed p (tm.runFrom (tm.initCfg input) n) := by + rw [runFrom_succ_eq_step, step_init, runFrom_embed] + +end Turing.MultiTapeTM.InputFromWorkTape diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean new file mode 100644 index 0000000000..5afc6a57e1 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Mathlib.Data.Fintype.Prod +public import Mathlib.Data.Fintype.Sum +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Substituting a work tape for the input tape + +The first work tape contains the virtual input. The remaining tapes are the native work tapes. +A classifier distinguishes the two blank boundaries, preserving native head clamping without +extending the alphabet. One native step takes two steps, and the real input head stays parked. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} + +/-- Location of the virtual input head. -/ +inductive InputMode + | left + | inside + | right +deriving DecidableEq + +instance : Finite InputMode := + Finite.of_injective (fun | .left => (0 : Fin 3) | .inside => 1 | .right => 2) + (by intro a b h; cases a <;> cases b <;> simp_all) + +/-- Boundary toward which a virtual input-head move was made. -/ +inductive InputBoundary + | left + | right + +instance : Finite InputBoundary := + Finite.of_injective (fun | .left => true | .right => false) + (by intro a b h; cases a <;> cases b <;> simp_all) + +/-- Movement of the virtual input head, with outward boundary moves clamped. -/ +def InputMode.move : InputMode → SignType → SignType + | .left, .neg => 0 + | .right, .pos => 0 + | _, move => move + +/-- Boundary to use if the cell reached by a virtual input-head move is blank. -/ +def InputMode.nextBoundary : + InputMode → SignType → InputBoundary + | _, .neg | .left, .zero => .left + | _, _ => .right + +/-- Convert a boundary classifier result to an input mode. -/ +def InputBoundary.inputMode : InputBoundary → InputMode + | .left => .left + | .right => .right + +/-- Control state for the work-tape input simulation. -/ +inductive InputState (State : Type*) + | run (q : State) (mode : InputMode) + | classify (q : State) (boundary : InputBoundary) + +instance [Finite State] : Finite (InputState State) := by + let := Fintype.ofFinite State + let := Fintype.ofFinite InputMode + let := Fintype.ofFinite InputBoundary + apply Finite.of_injective (fun s : InputState State => match s with + | .run q mode => ((q, Sum.inl mode) : State × (InputMode ⊕ InputBoundary)) + | .classify q boundary => (q, Sum.inr boundary)) + intro a b h + cases a <;> cases b <;> simp_all + +/-- Classify the cell reached after a virtual input-head movement. -/ +def classifyInput (cell : Option Symbol) (boundary : InputBoundary) : InputMode := + if cell.isSome then .inside else boundary.inputMode + +/-- Use the first work tape as input, and shift native work tapes one index to the right. +The virtual head starts at cell zero; classification also handles empty input. -/ +def inputFromWorkTape (tm : MultiTapeTM k Symbol State) : + MultiTapeTM (k + 1) Symbol (InputState State) where + q₀ := .classify tm.q₀ .right + tr q _ work := match q with + | .run q mode => + let out := tm.tr q (if mode = .inside then work 0 else none) (fun i => work i.succ) + ⟨0, Fin.cases (none, mode.move out.inputMove) out.workActions, out.outS, + out.q'.map fun q => .classify q (mode.nextBoundary out.inputMove)⟩ + | .classify q boundary => + ⟨0, fun _ => (none, 0), none, some (.run q (classifyInput (work 0) boundary))⟩ + +namespace InputFromWorkTape + +/-- View a native input-head position as a work-tape position. -/ +def virtualInputPos {input : List Symbol} (p : Fin (input.length + 2)) : ℤ := + p.val - 1 + +/-- Classify a native input-head position as the left boundary, an input cell, or the right +boundary. -/ +def inputMode {input : List Symbol} + (p : Fin (input.length + 2)) : InputMode := + if p = 0 then .left else if p.val = input.length + 1 then .right else .inside + +/-- Embed a native configuration while parking the real input head at `p`. -/ +def embed {outerInput input : List Symbol} (p : Fin (outerInput.length + 2)) + (cfg : Cfg k Symbol State input) : Cfg (k + 1) Symbol (InputState State) outerInput where + state := cfg.state.map fun q => .run q (inputMode cfg.inputPos) + inputPos := p + workTapes := Fin.cases (listTape input) cfg.workTapes + workTapePos := Fin.cases (virtualInputPos cfg.inputPos) cfg.workTapePos + output := cfg.output + +/-- The classifier configuration between the two halves of a simulated step. -/ +def classifyCfg {outerInput input : List Symbol} (p : Fin (outerInput.length + 2)) + (cfg : Cfg k Symbol State input) (boundary : InputBoundary) : + Cfg (k + 1) Symbol (InputState State) outerInput := + { embed p cfg with state := cfg.state.map fun q => .classify q boundary } + +end InputFromWorkTape + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean new file mode 100644 index 0000000000..c523f53fe0 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToWorkTape.lean @@ -0,0 +1,95 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Redirecting output to a fresh work tape + +`outputToWorkTape` adds one work tape, at index `Fin.last k`, and writes the native output there. +Its head stays immediately after the output. The original work tapes and native input head follow +the original machine exactly; the external output is empty. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- Redirect output to a new last work tape without changing the alphabet or control states. -/ +def outputToWorkTape (tm : MultiTapeTM k Symbol State) : MultiTapeTM (k + 1) Symbol State where + q₀ := tm.q₀ + tr q input work := + let out := tm.tr q input (fun i => work i.castSucc) + ⟨out.inputMove, + Fin.lastCases (out.outS.elim (none, 0) (fun s => (some (some s), 1))) out.workActions, + none, out.q'⟩ + +namespace OutputToWorkTape + +/-- Represent a native configuration with its output on the new tape. -/ +def embed (cfg : Cfg k Symbol State input) : Cfg (k + 1) Symbol State input where + state := cfg.state + inputPos := cfg.inputPos + workTapes := Fin.lastCases (listTape cfg.output) cfg.workTapes + workTapePos := Fin.lastCases cfg.output.length cfg.workTapePos + output := [] + +variable (tm : MultiTapeTM k Symbol State) + +/-- Each original transition is one transition of the output-redirected machine. -/ +lemma step_embed (cfg : Cfg k Symbol State input) : + tm.outputToWorkTape.step (embed cfg) = embed (tm.step cfg) := by + have hwork : (fun i : Fin k => (embed cfg).workTapeSymbols i.castSucc) = cfg.workTapeSymbols := by + funext i + simp [embed, Cfg.workTapeSymbols] + cases hs : cfg.state with + | none => simp [step, embed, hs] + | some q => + unfold step + rw [show (embed cfg).state = some q from hs, hs] + simp only [outputToWorkTape] + rw [show (embed cfg).inputSymbol = cfg.inputSymbol from rfl, hwork] + generalize htr : tm.tr q cfg.inputSymbol cfg.workTapeSymbols = out + simp only [htr] + apply Cfg.ext <;> try rfl + · funext i p + refine Fin.lastCases ?_ (fun j => ?_) i + · cases out.outS <;> simp [embed, listTape_append_single] + · cases hw : (out.workActions j).1 <;> simp [embed, hw] + · funext i + refine Fin.lastCases ?_ (fun j => ?_) i + · cases out.outS <;> simp [embed] + · simp [embed] + +/-- Output redirection preserves arbitrary runs, including padded halting times. -/ +lemma runFrom_embed (cfg : Cfg k Symbol State input) (n : ℕ) : + tm.outputToWorkTape.runFrom (embed cfg) n = embed (tm.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => rw [runFrom_succ_eq_step', ih, step_embed, runFrom_succ_eq_step'] + +end OutputToWorkTape + +/-- The output-redirected machine simulates an ordinary run starting with blank work tapes. -/ +lemma runFrom_outputToWorkTape (tm : MultiTapeTM k Symbol State) (input : List Symbol) (n : ℕ) : + tm.outputToWorkTape.runFrom (tm.outputToWorkTape.initCfg input) n = + OutputToWorkTape.embed (tm.runFrom (tm.initCfg input) n) := by + have hinit : tm.outputToWorkTape.initCfg input = OutputToWorkTape.embed (tm.initCfg input) := by + apply Cfg.ext <;> try rfl + · funext i p + refine Fin.lastCases ?_ (fun j => ?_) i + · cases p <;> simp [OutputToWorkTape.embed, listTape] + · simp [OutputToWorkTape.embed] + · funext i + refine Fin.lastCases ?_ (fun j => ?_) i <;> simp [OutputToWorkTape.embed] + rw [hinit, OutputToWorkTape.runFrom_embed] + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md index 48ab231e2c..a5c8b6e339 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md @@ -7,3 +7,5 @@ These modules describe executable machines and their effects on configurations a transition hands its tapes, head positions, and accumulated output to the second machine. - `ExtendTapes` places a machine's tapes along any injection. Time is unchanged; each unused tape contributes one visited cell to space. Arbitrary data on unused tapes is preserved. +- `OutputToWorkTape` redirects output to one fresh tape, including the symbol on a halting step. +- `InputFromWorkTape` simulates the native input on a work tape, preserving boundary clamping. diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean new file mode 100644 index 0000000000..7cd3bc4048 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TapeContents.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Algebra.Order.Ring.Nat +public import Mathlib.Algebra.Order.Sub.Basic +public import Mathlib.Algebra.Ring.Int.Defs +public import Mathlib.Data.Finset.Attr +public import Mathlib.Data.Nat.SuccPred + +/-! # Contiguous work-tape contents -/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {Symbol : Type*} + +/-- A tape containing exactly the symbols of `xs` at positions `0, ..., xs.length - 1`. -/ +def listTape (xs : List Symbol) : ℤ → Option Symbol + | .ofNat n => xs[n]? + | .negSucc _ => none + +@[simp] +lemma listTape_ofNat (xs : List Symbol) (n : ℕ) : listTape xs n = xs[n]? := rfl + +@[simp] +lemma listTape_negSucc (xs : List Symbol) (n : ℕ) : listTape xs (.negSucc n) = none := rfl + +/-- Appending one output symbol writes precisely the cell after the existing output. -/ +lemma listTape_append_single (xs : List Symbol) (x : Symbol) : + listTape (xs ++ [x]) = Function.update (listTape xs) (xs.length : ℤ) (some x) := by + funext z + cases z with + | negSucc n => simp [listTape] + | ofNat n => + by_cases h : n = xs.length + · subst n; simp + · by_cases hn : n < xs.length + · simp [List.getElem?_append, hn, h] + · simp [List.getElem?_append, hn, h, show n - xs.length ≠ 0 by omega] + +/-- Every position strictly inside a list tape is nonblank. -/ +lemma listTape_isSome (xs : List Symbol) {p : ℤ} (hp : 0 ≤ p) (hlt : p < xs.length) : + (listTape xs p).isSome := by + lift p to ℕ using hp + simp [listTape] + omega + +end Turing.MultiTapeTM diff --git a/CslibTests.lean b/CslibTests.lean index 2c6af5ae9b..6eadb97baf 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -18,6 +18,7 @@ import CslibTests.MLL import CslibTests.Modal import CslibTests.Modal.Ideal import CslibTests.Modal.Stlc +import CslibTests.MultiTapeAdapters import CslibTests.MultiTapeComplexity import CslibTests.MultiTapePlumbing import CslibTests.Reduction diff --git a/CslibTests/MultiTapeAdapters.lean b/CslibTests/MultiTapeAdapters.lean new file mode 100644 index 0000000000..2b2b8c8b89 --- /dev/null +++ b/CslibTests/MultiTapeAdapters.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OutputToWorkTape +import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape + +namespace CslibTests.MultiTapeAdapters + +open Turing.MultiTapeTM + +private def finish (move : SignType) (symbol : Bool) : Turing.MultiTapeTM 0 Bool Unit where + q₀ := () + tr _ _ _ := ⟨move, Fin.elim0, some symbol, none⟩ + +-- Output redirection includes the symbol emitted on the halting transition. +example : ((finish 0 true).outputToWorkTape.runFrom + ((finish 0 true).outputToWorkTape.initCfg []) 1).workTapes 0 0 = some true := by rfl + +example : ((finish 0 true).outputToWorkTape.runFrom + ((finish 0 true).outputToWorkTape.initCfg []) 1).output = [] := by rfl + +private def readInput : Turing.MultiTapeTM 0 Bool Unit where + q₀ := () + tr _ input _ := ⟨0, Fin.elim0, input, none⟩ + +-- Substituted input is read from the work tape, with the real head parked elsewhere. +private def preparedInput (xs : List Bool) : Cfg 1 Bool (InputState Unit) [false] := + InputFromWorkTape.classifyCfg 0 (readInput.initCfg xs) .right + +example : (readInput.inputFromWorkTape.runFrom (preparedInput [true]) 3).output = [true] := by + rfl + +example : (readInput.inputFromWorkTape.runFrom (preparedInput [true]) 3).inputPos = 0 := by rfl + +example : (readInput.inputFromWorkTape.runFrom (preparedInput []) 3).state = none := by rfl + +end CslibTests.MultiTapeAdapters