diff --git a/Cslib.lean b/Cslib.lean index 9ed9aa2ab..d14330643 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,9 +46,11 @@ public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Languages.SafetyLiveness +public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Concat public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.RewindInput public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Concat 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 diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Concat.lean b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Concat.lean new file mode 100644 index 000000000..3d267e0d0 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/Concat.lean @@ -0,0 +1,90 @@ +/- +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 Mathlib.Basic.Finite.Sum +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Concat + +/-! +# Complexity of a concatenation of two functions + +If `f` and `g` are computable, then so is any function whose encoded result is the encoded result +of `f` followed by the encoded result of `g`. The bounds are the sums of the two bounds, plus one +input rewind in time and a constant in space. + +The result is stated for an arbitrary function `h` together with the assumption that its encoding +is the concatenation of the two encodings, rather than for a fixed pairing. That way it covers +whatever the caller happens to be encoding — a pair, a list, a tagged union — and the caller is +the one who has to know that the concatenation of the two encodings is again injective. The pair +is the typical case and is spelled out in `computableInTimeAndSpace_pair`. + +Note that nothing has to be assumed about how the two encodings compose beyond `henc`: the machine +never inspects the concatenation. It writes the first encoded result to the output tape, and then +writes the second one after it, so the concatenation is produced simply by not resetting the output +tape in between. + +## Main results + +* `Turing.MultiTapeTM.computableInTimeAndSpace_concat`: the complexity of a concatenation. +* `Turing.MultiTapeTM.computableInTimeAndSpace_pair`: the special case of a pair. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {α β γ δ : Type*} + +/-- **Complexity of a concatenation.** If `f` and `g` are computable and the encoded result of `h` +is the encoded result of `f` followed by the encoded result of `g`, then `h` is computable in the +sum of the two times plus the length of the input, and in the sum of the two spaces plus a +constant. + +The machine runs the machine for `f`, rewinds the input head, and runs the machine for `g` on fresh +work tapes; the length of the input in the time bound is the cost of that rewind. The intermediate +results are never stored: both machines write straight to the output tape, which is append-only, so +their outputs end up concatenated. The constant in the space bound is the number of work tapes of +the two machines, each of which contributes the one cell its head is parked on while the other +machine runs; the rewind itself costs no space. -/ +theorem computableInTimeAndSpace_concat + {f : α → β} {g : α → γ} {h : α → δ} + {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {encD : δ ↪ List Bool} + {tf sf tg sg : α → ℕ} + (henc : ∀ x, encD (h x) = encB (f x) ++ encC (g x)) + (hf : ComputableInTimeAndSpace f encIn encB tf sf) + (hg : ComputableInTimeAndSpace g encIn encC tg sg) : + ∃ c, ComputableInTimeAndSpace h encIn encD + (fun x => tf x + tg x + (encIn x).length + 2) + (fun x => sf x + sg x + c) := by + obtain ⟨k₀, State₀, hfinite₀, tm₀, htm₀⟩ := hf + obtain ⟨k₁, State₁, hfinite₁, tm₁, htm₁⟩ := hg + refine ⟨k₀ + k₁, k₀ + k₁, (State₀ ⊕ RewindState) ⊕ State₁, inferInstance, + concat tm₀ tm₁, fun x => ?_⟩ + obtain ⟨t₀, ht₀, s₀, hs₀, hcomp₀⟩ := htm₀ x + obtain ⟨t₁, ht₁, s₁, hs₁, hcomp₁⟩ := htm₁ x + obtain ⟨t, htle, s, hsle, hcomp⟩ := computesInTimeAndSpace_concat tm₀ tm₁ hcomp₀ hcomp₁ + have htbound : t ≤ tf x + tg x + (encIn x).length + 2 := by omega + have hsbound : s ≤ sf x + sg x + (k₀ + k₁) := by omega + exact ⟨t, htbound, s, hsbound, henc x ▸ hcomp⟩ + +/-- **Complexity of computing a pair.** The special case of `computableInTimeAndSpace_concat` in +which the two results are packed into a pair, encoded by concatenating the two encodings. It is up +to the caller to provide such an encoding; this needs the encoding of the first component to +determine where it ends, as a prefix-free or length-prefixed encoding does. -/ +theorem computableInTimeAndSpace_pair + {f : α → β} {g : α → γ} + {encIn : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} + {encPair : β × γ ↪ List Bool} {tf sf tg sg : α → ℕ} + (henc : ∀ p : β × γ, encPair p = encB p.1 ++ encC p.2) + (hf : ComputableInTimeAndSpace f encIn encB tf sf) + (hg : ComputableInTimeAndSpace g encIn encC tg sg) : + ∃ c, ComputableInTimeAndSpace (fun x => (f x, g x)) encIn encPair + (fun x => tf x + tg x + (encIn x).length + 2) + (fun x => sf x + sg x + c) := + computableInTimeAndSpace_concat (fun x => henc (f x, g x)) hf hg + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md new file mode 100644 index 000000000..c1b0c47c0 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Combinators/README.md @@ -0,0 +1,11 @@ +# Function combinators + +These modules state the complexity of a function built from other functions. They are the reusable +interface: a caller combines `ComputableInTimeAndSpace` facts without ever mentioning tapes, head +positions or configurations. The machines behind them come from [Plumbing](../Plumbing) and +[NormalForms](../NormalForms). + +- `Concat` computes a function whose encoded result is the concatenation of the encoded results of + two functions, of which the pair is the typical case. The two machines write straight to the + append-only output tape, so no intermediate result is ever stored; the cost over the two machines + is one rewind of the input tape in time, and one idle cell per work tape in space. diff --git a/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md b/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md index dadf3ffbe..eb7d66070 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md +++ b/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/README.md @@ -7,3 +7,8 @@ The transformation adds at most the input length plus two steps, including on em The `HaltsWithInputAtStart` predicate states the property at every halting time, so padded runs also satisfy it. The construction does not require the original machine to be total. + +`rewindInput_halts_spaceUsed` bundles the normal form with its cost, so a combinator that needs to +feed one input to two machines never has to unfold the rewind. Only the time bound grows: the +rewind moves no work-tape head, so it visits no cell that was not visited already, and the space +bound is preserved exactly. diff --git a/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean b/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean index 1accf2fac..b9dc60365 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/NormalForms/RewindInput.lean @@ -27,6 +27,10 @@ variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} def rewindInput (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol (State ⊕ RewindState) := tm.seq (rewind .input) +/-- The normalized machine starts in the original machine's initial configuration. -/ +lemma initCfg_rewindInput (tm : MultiTapeTM k Symbol State) (input : List Symbol) : + tm.rewindInput.initCfg input = Sequential.left (rewind .input) (tm.initCfg input) := rfl + /-- Exact input-rewind execution from any configuration, once the first machine reaches its least halting time. Everything other than the input head and control state is preserved. -/ lemma runFrom_rewindInput (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) @@ -52,6 +56,43 @@ lemma rewindInput_halts (tm : MultiTapeTM k Symbol State) (t : ℕ) · rw [tm.runFrom_eq_of_halt (tm.initCfg input) hu hhaltu] exact runFrom_rewindInput tm (tm.initCfg input) u hhaltu hactiveu +/-- **Normalizing costs no space.** The rewind moves no work-tape head, so every cell the +normalized machine visits was already visited by the original one. This is what makes the normal +form free to use inside a combinator: only the time bound grows. -/ +lemma spaceUsed_rewindInput_le (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) + (u v : ℕ) (hhalt : (tm.runFrom cfg u).state = none) + (hactive : ∀ m < u, (tm.runFrom cfg m).state ≠ none) : + tm.rewindInput.spaceUsed (Sequential.left (rewind .input) cfg) (u + v) ≤ + tm.spaceUsed cfg u := by + refine spaceUsed_le_of_workTapePos_mem _ _ (u + v) u fun m _ i => ?_ + rcases Nat.lt_or_ge m u with hm | hm + · rw [rewindInput, + Sequential.runFrom_left tm (rewind .input) cfg m fun r hr => hactive r (by omega)] + exact mem_visitedByTapeHead.mpr ⟨m, by omega, rfl⟩ + · obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le hm + rw [rewindInput, runFrom_seq tm (rewind .input) cfg u j hhalt hactive] + simp only [Sequential.right, Cfg.withState_workTapePos, Rewind.runFrom_input_workTapePos, + Cfg.withState_workTapePos] + exact mem_visitedByTapeHead.mpr ⟨u, by omega, rfl⟩ + +/-- The normal form together with its cost: the run takes at most the input length plus two extra +steps, and uses no extra space at all. The bound accepts padded native halting times. -/ +lemma rewindInput_halts_spaceUsed (tm : MultiTapeTM k Symbol State) (t : ℕ) + (hhalt : (tm.runFrom (tm.initCfg input) t).state = none) : + ∃ t' ≤ t + input.length + 2, + tm.rewindInput.runFrom (tm.rewindInput.initCfg input) t' = + Sequential.right (Rewind.inputCfg (tm.runFrom (tm.initCfg input) t) none 1) ∧ + tm.rewindInput.spaceUsed (tm.rewindInput.initCfg input) t' ≤ + tm.spaceUsed (tm.initCfg input) t := by + obtain ⟨u, hu, hhaltu, hactiveu⟩ := exists_minimal_halting_time tm (tm.initCfg input) t hhalt + refine ⟨u + ((tm.runFrom (tm.initCfg input) u).inputPos.val - 1 + 2), ?_, ?_, ?_⟩ + · have := (tm.runFrom (tm.initCfg input) u).inputPos.isLt + omega + · rw [tm.runFrom_eq_of_halt (tm.initCfg input) hu hhaltu] + exact runFrom_rewindInput tm (tm.initCfg input) u hhaltu hactiveu + · exact (spaceUsed_rewindInput_le tm (tm.initCfg input) u _ hhaltu hactiveu).trans + (spaceUsed_mono tm (tm.initCfg input) hu) + /-- Every halting run from an initial configuration has its input head at the initial position. -/ def HaltsWithInputAtStart (tm : MultiTapeTM k Symbol State) : Prop := ∀ (input : List Symbol) (t : ℕ), (tm.runFrom (tm.initCfg input) t).state = none → diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean index ab83d4d1e..b823c034a 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean @@ -6,7 +6,7 @@ Authors: Christian Reitwiessner, Samuel Schlesinger module -public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas /-! # Configuration state replacement @@ -63,6 +63,68 @@ lemma Cfg.withState_withState {cfg : Cfg k Symbol State input} {State' State'' : lemma Cfg.withState_self {cfg : Cfg k Symbol State input} : cfg.withState cfg.state = cfg := rfl +/-- The configuration `cfg` with `o` prepended to the output produced so far. -/ +def Cfg.prependOutput (o : List Symbol) (cfg : Cfg k Symbol State input) : + Cfg k Symbol State input := + { cfg with output := o ++ cfg.output } + +@[simp] +lemma Cfg.prependOutput_state {o : List Symbol} {cfg : Cfg k Symbol State input} : + (cfg.prependOutput o).state = cfg.state := rfl + +@[simp] +lemma Cfg.prependOutput_inputPos {o : List Symbol} {cfg : Cfg k Symbol State input} : + (cfg.prependOutput o).inputPos = cfg.inputPos := rfl + +@[simp] +lemma Cfg.prependOutput_workTapes {o : List Symbol} {cfg : Cfg k Symbol State input} : + (cfg.prependOutput o).workTapes = cfg.workTapes := rfl + +@[simp] +lemma Cfg.prependOutput_workTapePos {o : List Symbol} {cfg : Cfg k Symbol State input} : + (cfg.prependOutput o).workTapePos = cfg.workTapePos := rfl + +@[simp] +lemma Cfg.prependOutput_output {o : List Symbol} {cfg : Cfg k Symbol State input} : + (cfg.prependOutput o).output = o ++ cfg.output := rfl + +@[simp] +lemma Cfg.prependOutput_inputSymbol {o : List Symbol} {cfg : Cfg k Symbol State input} : + (cfg.prependOutput o).inputSymbol = cfg.inputSymbol := rfl + +@[simp] +lemma Cfg.prependOutput_workTapeSymbols {o : List Symbol} {cfg : Cfg k Symbol State input} : + (cfg.prependOutput o).workTapeSymbols = cfg.workTapeSymbols := rfl + +/-- A step does not depend on the output accumulated so far, since the output tape is write-only +and a step only appends to it. -/ +lemma step_prependOutput (tm : MultiTapeTM k Symbol State) (o : List Symbol) + (cfg : Cfg k Symbol State input) : + tm.step (cfg.prependOutput o) = (tm.step cfg).prependOutput o := by + cases hs : cfg.state with + | none => simp [step, Cfg.prependOutput, hs] + | some q => + have hstate : (cfg.prependOutput o).state = some q := hs + unfold step + rw [hstate, hs, Cfg.prependOutput_inputSymbol, Cfg.prependOutput_workTapeSymbols] + apply Cfg.ext <;> simp [List.append_assoc] + +/-- A whole run does not depend on the output accumulated before it. This is what lets a machine +be run after another one has already written part of the output. -/ +lemma runFrom_prependOutput (tm : MultiTapeTM k Symbol State) (o : List Symbol) + (cfg : Cfg k Symbol State input) (n : ℕ) : + tm.runFrom (cfg.prependOutput o) n = (tm.runFrom cfg n).prependOutput o := by + induction n with + | zero => rfl + | succ n ih => rw [runFrom_succ_eq_step', ih, step_prependOutput, runFrom_succ_eq_step'] + +/-- Prepending output does not change the space used. -/ +lemma spaceUsed_prependOutput (tm : MultiTapeTM k Symbol State) (o : List Symbol) + (cfg : Cfg k Symbol State input) (n : ℕ) : + tm.spaceUsed (cfg.prependOutput o) n = tm.spaceUsed cfg n := + spaceUsed_eq_of_workTapePos _ _ n fun m _ => by + rw [runFrom_prependOutput, Cfg.prependOutput_workTapePos] + /-- A family of configurations with the prescribed steps agrees with `runFrom`. -/ lemma runFrom_eq_of_step (tm : MultiTapeTM k Symbol State) (path : ℕ → Cfg k Symbol State input) (n : ℕ) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Concat.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Concat.lean new file mode 100644 index 000000000..42053b832 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Concat.lean @@ -0,0 +1,210 @@ +/- +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 Mathlib.Data.Fin.Embedding +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes +public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.RewindInput + +/-! +# Concatenating the outputs of two machines + +`concat tm₀ tm₁` runs `tm₀`, rewinds the native input head, and then runs `tm₁`. Since the output +tape is write-only and a machine only ever appends to it, the output of the composite is the output +of `tm₀` followed by the output of `tm₁`, and no intermediate result has to be stored anywhere. + +The two machines are placed on disjoint blocks of work tapes: `tm₀` on the first `k₀` and `tm₁` on +the last `k₁`. So `tm₁` starts on blank tapes, exactly as it would when started on its own, and the +tapes `tm₀` leaves behind are never touched again. Giving `tm₁` fresh tapes is what makes it +unnecessary to know anything about the configuration `tm₀` halts in, and rewinding the input head +in between is what lets `tm₁` read the same input as `tm₀`. + +## Main definitions + +* `Turing.MultiTapeTM.concatTapeLeft`, `Turing.MultiTapeTM.concatTapeRight`: the two blocks of work + tapes. +* `Turing.MultiTapeTM.concatPrefix`: the first phase, the first machine followed by the rewind. +* `Turing.MultiTapeTM.concat`: the composite machine. + +## Main results + +* `Turing.MultiTapeTM.computesInTimeAndSpace_concat`: the composite computes the concatenation of + the two outputs. The extra time is one input rewind. The extra space is `k₀ + k₁`: whichever + machine is not running has an idle head on each of its tapes, and each such head still counts for + the one cell it sits on. The rewind itself costs no space at all, by + `spaceUsed_rewindInput_le` — it moves no work-tape head, so it visits no new cell. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type*} + +/-- The block of work tapes the first machine of a concatenation runs on. -/ +def concatTapeLeft (k₀ k₁ : ℕ) : Fin k₀ ↪ Fin (k₀ + k₁) := Fin.castAddEmb k₁ + +/-- The block of work tapes the second machine of a concatenation runs on. -/ +def concatTapeRight (k₀ k₁ : ℕ) : Fin k₁ ↪ Fin (k₀ + k₁) := Fin.natAddEmb k₀ + +/-- The two blocks of work tapes are disjoint, so the second machine of a concatenation starts on +tapes that the first one never touched. -/ +lemma concatTapeRight_notMem_range_left (j : Fin k₁) : + concatTapeRight k₀ k₁ j ∉ Set.range (concatTapeLeft k₀ k₁) := by + rintro ⟨i, hi⟩ + have hval := congrArg Fin.val hi + simp only [concatTapeLeft, concatTapeRight, Fin.castAddEmb_apply, Fin.natAddEmb_apply, + Fin.val_castAdd, Fin.val_natAdd] at hval + have := i.isLt + omega + +/-- The first phase of a concatenation: the first machine, on its block of work tapes, followed by +the native-input rewind. -/ +def concatPrefix (k₁ : ℕ) (tm₀ : MultiTapeTM k₀ Symbol State₀) : + MultiTapeTM (k₀ + k₁) Symbol (State₀ ⊕ RewindState) := + (tm₀.extendTapes (concatTapeLeft k₀ k₁)).rewindInput + +/-- Run `tm₀`, rewind the input head, then run `tm₁` on a disjoint block of work tapes. -/ +def concat (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) : + MultiTapeTM (k₀ + k₁) Symbol ((State₀ ⊕ RewindState) ⊕ State₁) := + (concatPrefix k₁ tm₀).seq (tm₁.extendTapes (concatTapeRight k₀ k₁)) + +namespace Concat + +variable (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) + {input : List Symbol} + +/-- The composite is the sequential composition of its two phases. -/ +lemma concat_eq_seq : + concat tm₀ tm₁ = (concatPrefix k₁ tm₀).seq (tm₁.extendTapes (concatTapeRight k₀ k₁)) := rfl + +/-- The configuration in which the first phase halts, in terms of the first machine's own run. -/ +def prefixCfg (t₀ : ℕ) : Cfg (k₀ + k₁) Symbol (State₀ ⊕ RewindState) input := + Sequential.right (Rewind.inputCfg (ExtendTapes.embed (concatTapeLeft k₀ k₁) + (tm₀.runFrom (tm₀.initCfg input) t₀) (fun _ _ => none) (fun _ => 0)) none 1) + +/-- The first phase halts with the input head rewound, having produced exactly the output of the +first machine and used its space plus the one cell each idle tape's head sits on. + +This is `rewindInput_halts_spaceUsed` read on the left block of tapes: the normal form carries its +own cost, so nothing about the rewind has to be unfolded here. -/ +lemma exists_concatPrefix (k₁ : ℕ) {t₀ : ℕ} + (hhalt : (tm₀.runFrom (tm₀.initCfg input) t₀).state = none) : + ∃ u ≤ t₀ + input.length + 2, + (concatPrefix k₁ tm₀).runFrom ((concatPrefix k₁ tm₀).initCfg input) u = + prefixCfg tm₀ (k₁ := k₁) t₀ ∧ + (concatPrefix k₁ tm₀).spaceUsed ((concatPrefix k₁ tm₀).initCfg input) u ≤ + tm₀.spaceUsed (tm₀.initCfg input) t₀ + k₁ := by + have hrun := runFrom_extendTapes tm₀ (concatTapeLeft k₀ k₁) input + have hhalt' : ((tm₀.extendTapes (concatTapeLeft k₀ k₁)).runFrom + ((tm₀.extendTapes (concatTapeLeft k₀ k₁)).initCfg input) t₀).state = none := by + rw [hrun]; exact hhalt + obtain ⟨u, hule, hucfg, huspace⟩ := + rewindInput_halts_spaceUsed (tm₀.extendTapes (concatTapeLeft k₀ k₁)) t₀ hhalt' + refine ⟨u, hule, ?_, ?_⟩ + · unfold concatPrefix + rw [hucfg, hrun t₀] + rfl + · refine huspace.trans ?_ + rw [spaceUsed_extendTapes tm₀ _ input t₀] + omega + +/-- Everything the second machine of a concatenation needs of the configuration handed to it: its +own block of tapes is blank and rewound and the input head is back at the start. The tapes of the +first machine may hold anything, and the output produced so far is kept. + +All of the content is `ExtendTapes.eq_embed_initCfg`; what is left here is only that the second +machine's block of tapes is disjoint from the first machine's, so the first machine left it +blank. -/ +lemma handoff_eq (t₀ : ℕ) (out : List Symbol) + (hout : (tm₀.runFrom (tm₀.initCfg input) t₀).output = out) : + (prefixCfg tm₀ (k₁ := k₁) t₀).withState + (some (tm₁.extendTapes (concatTapeRight k₀ k₁)).q₀) = + (ExtendTapes.embed (concatTapeRight k₀ k₁) (tm₁.initCfg input) + (prefixCfg tm₀ (k₁ := k₁) (input := input) t₀).workTapes + (prefixCfg tm₀ (k₁ := k₁) (input := input) t₀).workTapePos).prependOutput out := by + have houtH : ((prefixCfg tm₀ (k₁ := k₁) t₀).withState + (some (tm₁.extendTapes (concatTapeRight k₀ k₁)).q₀)).output = out := hout + rw [← houtH] + refine ExtendTapes.eq_embed_initCfg (concatTapeRight k₀ k₁) tm₁ _ rfl rfl ?_ ?_ + · intro j + simp [prefixCfg, Sequential.right, Rewind.inputCfg, concatTapeRight_notMem_range_left j] + · intro j + simp [prefixCfg, Sequential.right, Rewind.inputCfg, concatTapeRight_notMem_range_left j] + +end Concat + +/-- **Correctness of output concatenation.** If `tm₀` computes `out₀` and `tm₁` computes `out₁` +from the same input, then `concat tm₀ tm₁` computes `out₀ ++ out₁`. + +The extra time is the cost of one input rewind, which `rewindInput` accounts for. The extra space is +`k₀ + k₁`: whichever machine is not running has an idle head on each of its tapes, and each such +head still counts for the one cell it sits on. The rewind contributes nothing, since it moves no +work-tape head. -/ +theorem computesInTimeAndSpace_concat + (tm₀ : MultiTapeTM k₀ Symbol State₀) (tm₁ : MultiTapeTM k₁ Symbol State₁) + {input out₀ out₁ : List Symbol} {t₀ s₀ t₁ s₁ : ℕ} + (h₀ : ComputesInTimeAndSpace tm₀ input out₀ t₀ s₀) + (h₁ : ComputesInTimeAndSpace tm₁ input out₁ t₁ s₁) : + ∃ t ≤ t₀ + t₁ + input.length + 2, ∃ s ≤ s₀ + s₁ + (k₀ + k₁), + ComputesInTimeAndSpace (concat tm₀ tm₁) input (out₀ ++ out₁) t s := by + obtain ⟨hhalt₀, hout₀, hspace₀⟩ := h₀ + obtain ⟨hhalt₁, hout₁, hspace₁⟩ := h₁ + -- ### The first phase + obtain ⟨v, hvle, hvcfg, hvspace⟩ := Concat.exists_concatPrefix tm₀ k₁ hhalt₀ + have hvhalt : ((concatPrefix k₁ tm₀).runFrom ((concatPrefix k₁ tm₀).initCfg input) v).state + = none := by + rw [hvcfg]; rfl + obtain ⟨u, hule, huhalt, huactive⟩ := + exists_minimal_halting_time _ ((concatPrefix k₁ tm₀).initCfg input) v hvhalt + have hucfg : (concatPrefix k₁ tm₀).runFrom ((concatPrefix k₁ tm₀).initCfg input) u = + Concat.prefixCfg tm₀ (k₁ := k₁) t₀ := by + rw [← hvcfg] + exact (runFrom_eq_of_halt _ hule huhalt).symm + -- ### The second phase, on its own blank block of tapes and with the output so far + have hhandoff := Concat.handoff_eq tm₀ tm₁ t₀ out₀ hout₀ + rw [← hucfg] at hhandoff + have hNhalt : ((tm₁.extendTapes (concatTapeRight k₀ k₁)).runFrom + (((concatPrefix k₁ tm₀).runFrom ((concatPrefix k₁ tm₀).initCfg input) u).withState + (some (tm₁.extendTapes (concatTapeRight k₀ k₁)).q₀)) t₁).state = none := by + rw [hhandoff, runFrom_prependOutput, ExtendTapes.runFrom_embed] + simpa [ExtendTapes.embed] using hhalt₁ + have hNout : ((tm₁.extendTapes (concatTapeRight k₀ k₁)).runFrom + (((concatPrefix k₁ tm₀).runFrom ((concatPrefix k₁ tm₀).initCfg input) u).withState + (some (tm₁.extendTapes (concatTapeRight k₀ k₁)).q₀)) t₁).output = out₀ ++ out₁ := by + rw [hhandoff, runFrom_prependOutput, ExtendTapes.runFrom_embed] + simpa [ExtendTapes.embed] using congrArg (out₀ ++ ·) hout₁ + -- ### The composite + refine ⟨u + t₁, by omega, (concat tm₀ tm₁).spaceUsed ((concat tm₀ tm₁).initCfg input) (u + t₁), + ?_, ?_, ?_, rfl⟩ + · -- space: the two phases, each paying one cell for every tape of the other machine + have hsplit : (concat tm₀ tm₁).spaceUsed ((concat tm₀ tm₁).initCfg input) (u + t₁) ≤ + (concatPrefix k₁ tm₀).spaceUsed ((concatPrefix k₁ tm₀).initCfg input) u + + (tm₁.extendTapes (concatTapeRight k₀ k₁)).spaceUsed + (((concatPrefix k₁ tm₀).runFrom ((concatPrefix k₁ tm₀).initCfg input) u).withState + (some (tm₁.extendTapes (concatTapeRight k₀ k₁)).q₀)) t₁ := by + rw [Concat.concat_eq_seq, initCfg_seq] + exact spaceUsed_seq_le _ _ _ u t₁ huhalt huactive + have hsecond : (tm₁.extendTapes (concatTapeRight k₀ k₁)).spaceUsed + (((concatPrefix k₁ tm₀).runFrom ((concatPrefix k₁ tm₀).initCfg input) u).withState + (some (tm₁.extendTapes (concatTapeRight k₀ k₁)).q₀)) t₁ = s₁ + (k₀ + k₁ - k₁) := by + rw [hhandoff, spaceUsed_prependOutput, ExtendTapes.spaceUsed_embed, hspace₁] + have hfirst : (concatPrefix k₁ tm₀).spaceUsed ((concatPrefix k₁ tm₀).initCfg input) u ≤ + s₀ + k₁ := by + refine (spaceUsed_mono _ _ hule).trans ?_ + rwa [hspace₀] at hvspace + omega + · -- halting + rw [Concat.concat_eq_seq, initCfg_seq, runFrom_seq _ _ _ u t₁ huhalt huactive] + simp only [Sequential.right, Cfg.withState_state, hNhalt] + rfl + · -- output + rw [Concat.concat_eq_seq, initCfg_seq, runFrom_seq _ _ _ u t₁ huhalt huactive] + simp only [Sequential.right, Cfg.withState_output] + exact hNout + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean index f9a5ad304..6c7ba7842 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean @@ -6,7 +6,7 @@ Authors: Samuel Schlesinger module -public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic public import Mathlib.Data.Fintype.Inv public import Mathlib.Data.Fintype.Card @@ -16,6 +16,12 @@ public import Mathlib.Data.Fintype.Card `extendTapes` embeds a machine's work tapes along an injection. The extra tapes are idle, and each native step still takes exactly one step. The configuration embedding permits arbitrary contents and head positions on the extra tapes, so the transformation also applies to intermediate runs. + +`eq_embed_initCfg` is the converse reading, and is what hands a fresh block of tapes to a machine: +a configuration in that machine's initial state, with the input head at the start and its own block +of tapes blank and rewound, *is* its embedded initial configuration, whatever the other tapes hold +and whatever output has been produced. A machine placed on such a block therefore runs exactly as +it would on its own. -/ @[expose] public section @@ -36,6 +42,15 @@ lemma extend_apply {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α) (extra : Fin k' → α) (i : Fin k) : extend e values extra (e i) = values i := by simp [extend] +/-- A family that already agrees with the values on the image is unchanged by extension. -/ +lemma extend_eq_self {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α) + (extra : Fin k' → α) (h : ∀ i, extra (e i) = values i) : extend e values extra = extra := by + funext j + by_cases hj : j ∈ Set.range e + · obtain ⟨i, rfl⟩ := hj + rw [extend_apply, h i] + · simp [extend, hj] + /-- Embed a native configuration while retaining arbitrary data on the unused tapes. -/ def embed (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : @@ -46,6 +61,40 @@ def embed (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) workTapePos := extend e cfg.workTapePos extraPos output := cfg.output +/-- A tape outside the image of `e` holds whatever was supplied for it. -/ +@[simp] +lemma workTapes_embed_of_notMem_range (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) + (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) {j : Fin k'} + (hj : j ∉ Set.range e) : + (embed e cfg extraTapes extraPos).workTapes j = extraTapes j := by + simp [embed, extend, hj] + +/-- The head of a tape outside the image of `e` sits where it was supplied to. -/ +@[simp] +lemma workTapePos_embed_of_notMem_range (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) + (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) {j : Fin k'} + (hj : j ∉ Set.range e) : + (embed e cfg extraTapes extraPos).workTapePos j = extraPos j := by + simp [embed, extend, hj] + +/-- **Handing a fresh block of tapes to a machine.** A configuration in `tm`'s initial state, with +the input head at the start and the tapes in the image of `e` blank and rewound, is the embedded +initial configuration of `tm`, with whatever the other tapes hold and with the output produced so +far. This is what lets a machine be started inside a bigger one without knowing anything about the +configuration the previous machine left behind, beyond its output and that it did not touch this +block. -/ +lemma eq_embed_initCfg (e : Fin k ↪ Fin k') (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k' Symbol State input) (hstate : cfg.state = some tm.q₀) (hpos : cfg.inputPos = 1) + (hblank : ∀ i, cfg.workTapes (e i) = fun _ => none) + (hzero : ∀ i, cfg.workTapePos (e i) = 0) : + cfg = (embed e (tm.initCfg input) cfg.workTapes cfg.workTapePos).prependOutput cfg.output := by + refine Cfg.ext ?_ ?_ ?_ ?_ ?_ + · simpa [embed] using hstate + · simpa [embed] using hpos + · exact (extend_eq_self e _ cfg.workTapes hblank).symm + · exact (extend_eq_self e _ cfg.workTapePos hzero).symm + · simp [embed] + end ExtendTapes /-- Relabel the work tapes by an injection, leaving every tape outside its image idle. -/ @@ -124,14 +173,25 @@ lemma spaceUsed_embed (n : ℕ) : end ExtendTapes +/-- The extended machine starts on blank tapes, with the unused ones blank as well. -/ +lemma initCfg_extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') + (input : List Symbol) : + (tm.extendTapes e).initCfg input = + ExtendTapes.embed e (tm.initCfg input) (fun _ _ => none) (fun _ => 0) := by + ext i p <;> simp [ExtendTapes.embed, ExtendTapes.extend, extendTapes] + /-- Starting with blank work tapes commutes with tape extension. -/ lemma runFrom_extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (input : List Symbol) (n : ℕ) : (tm.extendTapes e).runFrom ((tm.extendTapes e).initCfg input) n = ExtendTapes.embed e (tm.runFrom (tm.initCfg input) n) (fun _ _ => none) (fun _ => 0) := by - have hinit : (tm.extendTapes e).initCfg input = - ExtendTapes.embed e (tm.initCfg input) (fun _ _ => none) (fun _ => 0) := by - ext i p <;> simp [ExtendTapes.embed, ExtendTapes.extend, extendTapes] - rw [hinit, ExtendTapes.runFrom_embed] + rw [initCfg_extendTapes, ExtendTapes.runFrom_embed] + +/-- Tape extension costs exactly one visited cell for each unused tape. -/ +lemma spaceUsed_extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') + (input : List Symbol) (n : ℕ) : + (tm.extendTapes e).spaceUsed ((tm.extendTapes e).initCfg input) n = + tm.spaceUsed (tm.initCfg input) n + (k' - k) := by + rw [initCfg_extendTapes, ExtendTapes.spaceUsed_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 72f5f51f8..ad901bea8 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md @@ -7,7 +7,15 @@ 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. + `eq_embed_initCfg` reads this backwards, and is what hands a fresh block of tapes to a machine: a + configuration in that machine's initial state whose own block is blank and rewound, with the + input head at the start, *is* its embedded initial configuration. So a combinator can start a + machine on a block without knowing anything about the configuration the previous one left behind, + beyond its output and that it did not touch this block. - `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. - `Rewind` shares one controller between native-input and work-tape rewinding. Work-tape rewind starts immediately after contiguous contents and finishes at their first cell, including when empty. +- `Concat` runs two machines one after the other on disjoint blocks of work tapes, rewinding the + input in between so that both read the same input. Their outputs land on the append-only output + tape in order, so the composite outputs their concatenation. diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean index e2bc0d968..5cc6f48b1 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Rewind.lean @@ -172,6 +172,19 @@ lemma runFrom_input (cfg : Cfg k Symbol State input) : split_ifs <;> simp_all <;> omega rw [hm, runFrom_input_scan cfg _ (by have := cfg.inputPos.isLt; omega), step_input_stop] +/-- The native-input rewind never moves a work-tape head. -/ +lemma step_input_workTapePos (cfg : Cfg k Symbol RewindState input) : + ((rewind (Symbol := Symbol) (k := k) .input).step cfg).workTapePos = cfg.workTapePos := by + funext i + cases hs : cfg.state <;> simp [step, rewind, hs] + +/-- A whole native-input rewind leaves every work-tape head where it was. -/ +lemma runFrom_input_workTapePos (cfg : Cfg k Symbol RewindState input) (n : ℕ) : + ((rewind (Symbol := Symbol) (k := k) .input).runFrom cfg n).workTapePos = cfg.workTapePos := by + induction n with + | zero => rfl + | succ n ih => rw [runFrom_succ_eq_step', step_input_workTapePos, ih] + end Rewind end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean index 4915af738..6dc98422a 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean @@ -83,6 +83,11 @@ lemma runFrom_right (cfg : Cfg k Symbol State₁ input) (n : ℕ) : end Sequential +/-- Sequential execution starts in the first machine's initial configuration. -/ +lemma initCfg_seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) + (input : List Symbol) : + (tm₀.seq tm₁).initCfg input = Sequential.left tm₁ (tm₀.initCfg input) := rfl + /-- Sequential execution splits at the first machine's earliest halt. The second machine receives all final tapes and head positions, together with the output accumulated so far. -/ lemma runFrom_seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) @@ -97,4 +102,24 @@ lemma runFrom_seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k simp [Sequential.left, Sequential.right, Cfg.withState, hhalt]] exact Sequential.runFrom_right tm₀ tm₁ _ v +/-- Sequential execution uses at most the space of its two phases. The two phases may revisit +each other's cells, so the bound is an inequality. -/ +lemma spaceUsed_seq_le (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) + (cfg : Cfg k Symbol State₀ input) (u v : ℕ) + (hhalt : (tm₀.runFrom cfg u).state = none) + (hactive : ∀ m < u, (tm₀.runFrom cfg m).state ≠ none) : + (tm₀.seq tm₁).spaceUsed (Sequential.left tm₁ cfg) (u + v) ≤ + tm₀.spaceUsed cfg u + tm₁.spaceUsed ((tm₀.runFrom cfg u).withState (some tm₁.q₀)) v := by + refine ((tm₀.seq tm₁).spaceUsed_add_le _ u v).trans (Nat.add_le_add (le_of_eq ?_) (le_of_eq ?_)) + · refine spaceUsed_eq_of_workTapePos _ _ u fun m hm => ?_ + rw [Sequential.runFrom_left tm₀ tm₁ cfg m fun r hr => hactive r (by omega)] + rfl + · rw [Sequential.runFrom_left tm₀ tm₁ cfg u hactive, + show Sequential.left tm₁ (tm₀.runFrom cfg u) = + Sequential.right ((tm₀.runFrom cfg u).withState (some tm₁.q₀)) by + simp [Sequential.left, Sequential.right, Cfg.withState, hhalt]] + refine spaceUsed_eq_of_workTapePos _ _ v fun m _ => ?_ + rw [Sequential.runFrom_right tm₀ tm₁ _ m] + rfl + end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 1b10ff9e6..6c65d140b 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -148,4 +148,52 @@ lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State intro t t' h exact Finset.sum_le_sum (fun i _ => spaceUsedByTape_mono tm cfg i h) +/-- The cells a run visits are the ones visited by its two halves. -/ +lemma visitedByTapeHead_add (cfg : Cfg k Symbol State input) (a b : ℕ) (i : Fin k) : + tm.visitedByTapeHead cfg (a + b) i = + tm.visitedByTapeHead cfg a i ∪ tm.visitedByTapeHead (tm.runFrom cfg a) b i := by + ext z + simp only [mem_visitedByTapeHead, Finset.mem_union] + constructor + · rintro ⟨r, hr, rfl⟩ + rcases Nat.lt_or_ge r (a + 1) with h | h + · exact Or.inl ⟨r, h, rfl⟩ + · exact Or.inr ⟨r - a, by omega, + by rw [← runFrom_add, show a + (r - a) = r from by omega]⟩ + · rintro (⟨r, hr, rfl⟩ | ⟨r, hr, rfl⟩) + · exact ⟨r, by omega, rfl⟩ + · exact ⟨a + r, by omega, by rw [runFrom_add]⟩ + +/-- Splitting a run into two phases can only overcount the cells it visits, since the two phases +may revisit each other's cells. -/ +lemma spaceUsed_add_le (cfg : Cfg k Symbol State input) (a b : ℕ) : + tm.spaceUsed cfg (a + b) ≤ tm.spaceUsed cfg a + tm.spaceUsed (tm.runFrom cfg a) b := by + rw [spaceUsed, spaceUsed, spaceUsed, ← Finset.sum_add_distrib] + refine Finset.sum_le_sum fun i _ => ?_ + rw [spaceUsedByTape, visitedByTapeHead_add] + exact Finset.card_union_le _ _ + +/-- Space usage only depends on where the work-tape heads are at each step, so two runs whose head +positions agree use the same space. This is what lets a machine be replaced by a simulation of it, +or by the same machine started with different output already accumulated. -/ +lemma spaceUsed_eq_of_workTapePos {State' : Type*} {input' : List Symbol} + {tm' : MultiTapeTM k Symbol State'} (cfg : Cfg k Symbol State input) + (cfg' : Cfg k Symbol State' input') (t : ℕ) + (h : ∀ m ≤ t, (tm.runFrom cfg m).workTapePos = (tm'.runFrom cfg' m).workTapePos) : + tm.spaceUsed cfg t = tm'.spaceUsed cfg' t := by + refine Finset.sum_congr rfl fun i _ => congrArg Finset.card (Finset.image_congr fun m hm => ?_) + exact congrFun (h m (Nat.lt_succ_iff.mp (Finset.mem_range.mp hm))) i + +/-- A run that never takes a head outside the cells another run visits uses no more space than +that other run. This is the sharp form of the space bound for a phase that moves no head: such a +phase visits no new cell at all, rather than one per tape. -/ +lemma spaceUsed_le_of_workTapePos_mem {State' : Type*} {input' : List Symbol} + {tm' : MultiTapeTM k Symbol State'} (cfg : Cfg k Symbol State input) + (cfg' : Cfg k Symbol State' input') (t t' : ℕ) + (h : ∀ m ≤ t, ∀ i, (tm.runFrom cfg m).workTapePos i ∈ tm'.visitedByTapeHead cfg' t' i) : + tm.spaceUsed cfg t ≤ tm'.spaceUsed cfg' t' := by + refine Finset.sum_le_sum fun i _ => Finset.card_le_card fun z hz => ?_ + obtain ⟨m, hm, rfl⟩ := mem_visitedByTapeHead.mp hz + exact h m (by omega) i + end Turing.MultiTapeTM diff --git a/CslibTests.lean b/CslibTests.lean index f9244f07f..184e92a14 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -20,6 +20,7 @@ import CslibTests.Modal.Ideal import CslibTests.Modal.Stlc import CslibTests.MultiTapeAdapters import CslibTests.MultiTapeComplexity +import CslibTests.MultiTapeConcat import CslibTests.MultiTapePlumbing import CslibTests.MultiTapeRewind import CslibTests.Reduction diff --git a/CslibTests/MultiTapeConcat.lean b/CslibTests/MultiTapeConcat.lean new file mode 100644 index 000000000..d4594173b --- /dev/null +++ b/CslibTests/MultiTapeConcat.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Concat + +namespace CslibTests.MultiTapeConcat + +open Turing.MultiTapeTM + +/-- Emit the symbol under the input head, having first moved the head off the start. Since the head +is left at the right boundary, the second machine of a concatenation only sees the same input if +the head is rewound in between. -/ +private def echo : Turing.MultiTapeTM 0 Bool Unit where + q₀ := () + tr _ input _ := ⟨1, Fin.elim0, input, none⟩ + +example : (echo.runFrom (echo.initCfg [true]) 1).output = [true] := by rfl + +-- One step for each machine and three for the rewind in between. +example : ((concat echo echo).runFrom ((concat echo echo).initCfg [true]) 5).state = none := by rfl + +example : ((concat echo echo).runFrom ((concat echo echo).initCfg [true]) 5).output = + [true, true] := by rfl + +example : ((concat echo echo).runFrom ((concat echo echo).initCfg [false]) 5).output = + [false, false] := by rfl + +/-- Copy the symbol under the input head to a work tape, then emit it from there. -/ +private def echoVia : Turing.MultiTapeTM 1 Bool Bool where + q₀ := false + tr q input work := match q with + | false => ⟨1, fun _ => (some input, 0), none, some true⟩ + | true => ⟨0, fun _ => (none, 0), work 0, none⟩ + +example : (echoVia.runFrom (echoVia.initCfg [true]) 2).output = [true] := by rfl + +-- Two steps for each machine and three for the rewind in between. +example : ((concat echoVia echoVia).runFrom + ((concat echoVia echoVia).initCfg [true]) 7).output = [true, true] := by rfl + +-- Each of the two work tapes is used, and each of them for a single cell. +example : (concat echoVia echoVia).spaceUsed ((concat echoVia echoVia).initCfg [true]) 7 = 2 := by + rfl + +-- The two machines really do run on disjoint blocks of work tapes. +example : ((concat echoVia echoVia).runFrom + ((concat echoVia echoVia).initCfg [true]) 7).workTapes (concatTapeLeft 1 1 0) 0 = + some true := by rfl + +example : ((concat echoVia echoVia).runFrom + ((concat echoVia echoVia).initCfg [true]) 7).workTapes (concatTapeRight 1 1 0) 0 = + some true := by rfl + +end CslibTests.MultiTapeConcat