diff --git a/Cslib.lean b/Cslib.lean index 6d5d11c93..dc5c898ed 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -99,6 +99,8 @@ public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Id public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound public import Cslib.Computability.Machines.Turing.MultiTape.Configuration public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.InputShortening +public import Cslib.Computability.Machines.Turing.MultiTape.LoglognEqualsNoSpace public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ClearWork public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes @@ -140,6 +142,7 @@ public import Cslib.Crypto.Protocols.SecretSharing.Defs public import Cslib.Crypto.Protocols.SecretSharing.Scheme public import Cslib.Crypto.Protocols.SecretSharing.Shamir public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial +public import Cslib.Foundations.Analysis.Asymptotics public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean index b23837b34..e7bd5426a 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean @@ -232,6 +232,33 @@ lemma storageBound_le_pow [Fintype Symbol] [Fintype State] : ∃ a c : ℕ, ∀ s : ℕ, storageBound Symbol State k s ≤ a * 2 ^ (c * s) := ⟨_, _, storageBound_le_base_mul_pow⟩ +/-- A fixed multiple of `(storageBound + 1) ^ storageBound` grows at most doubly exponentially +in the space. -/ +lemma storageBound_pow_le_pow_pow [Fintype Symbol] [Fintype State] (m : ℕ) : + ∃ a c : ℕ, ∀ s : ℕ, + m * (storageBound Symbol State k s + 1) ^ storageBound Symbol State k s + ≤ 2 ^ (2 ^ (a + c * s)) := by + obtain ⟨a, c, hbound⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k) + refine ⟨m + 2 * a + 1, 2 * c, fun s ↦ ?_⟩ + let B := storageBound Symbol State k s + let E := m + 2 * a + 2 * c * s + have hB : B ≤ 2 ^ (a + c * s) := by + rw [pow_add] + exact (hbound s).trans (by gcongr; exact Nat.lt_two_pow_self.le) + have hsum : m + B * B ≤ 2 ^ (E + 1) := by + calc m + B * B + _ ≤ 2 ^ m + 2 ^ (a + c * s) * 2 ^ (a + c * s) := by + gcongr; exact Nat.lt_two_pow_self.le + _ = 2 ^ m + 2 ^ (2 * a + 2 * c * s) := by ring + _ ≤ 2 ^ E + 2 ^ E := by gcongr <;> omega + _ = 2 ^ (E + 1) := by ring + calc m * (B + 1) ^ B + _ ≤ 2 ^ m * (2 ^ B) ^ B := by + exact Nat.mul_le_mul Nat.lt_two_pow_self.le (Nat.pow_le_pow_left Nat.lt_two_pow_self B) + _ = 2 ^ (m + B * B) := by ring + _ ≤ 2 ^ (2 ^ (E + 1)) := by gcongr; omega + _ = _ := by dsimp [E]; ring + /-! ## The storage and the core of a configuration Now we relate `Cfg` and `Storage` by giving the projection. diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean index 40c59283f..aee972c9c 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/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. -/ @@ -225,6 +233,11 @@ sub-machine's configurations into the combined machine by exactly such a state r (c : Cfg k Symbol State input) : Cfg k Symbol State' input := ⟨φ c.state, c.inputPos, c.workTapes, c.workTapePos, c.output⟩ +/-- Remap the successor state of an action through `φ`, leaving its effect on the tapes alone. -/ +@[simps] def Action.mapState {State' : Type*} (φ : Option State → Option State') + (action : Action k Symbol State) : Action k Symbol State' := + { action with state := φ action.state } + /-- The initial configuration for a starting state and an input string. -/ @[simp] def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input := diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 33afcdebb..12bfc1725 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -31,10 +31,20 @@ 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 * `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 * `Computes`: the machine halts with the given output on an input +* `ComputesSuchThat`: computation satisfying a predicate on the machine and input +* `ComputesFunSuchThat`: function computation satisfying such a predicate for each argument +* `ComputableSuchThat`: such a machine exists with binary alphabet and finitely many states +* `ComputesInTime` and `ComputesFunInTime`: computation within a time bound +* `ComputableInTime`: computability by a finite-state binary machine within a time bound +* `ComputesInSpace`: the machine produces an output within a space bound +* `ComputesFunInSpace`: function computation within an input-indexed space bound +* `ComputableInSpace`: computability by a finite-state binary machine within a space bound +* `DecidableInSpace`: the Boolean indicator of a set is computable within a space bound * `ComputesInTimeAndSpace`: the machine produces an output within the shared resource bounds * `ComputesFunInTimeAndSpace`: function computation with the shared time and space bounds * `ComputableInTimeAndSpace`: such a machine exists with binary alphabet and finitely many states. @@ -110,6 +120,19 @@ lemma tr_ofTr (q₀ : State) (ofTr q₀ tr).tr q input work = tr q input work := tr_iff.mp rfl +/-- `tm` run through `adapter`: it reads what `tm` reads through `adapter` and performs the +adaptation of the action of `tm`. -/ +noncomputable def adapt {k' : ℕ} (tm : MultiTapeTM k Symbol State) + (adapter : MultiTapeNTM.Adapter k k' Symbol State State) : MultiTapeTM k' Symbol State := + ofTr tm.q₀ fun q inp work => + adapter.action ⟨inp, work⟩ (tm.tr q (adapter.read ⟨inp, work⟩).inputSymbol + (adapter.read ⟨inp, work⟩).workTapeSymbols) + +/-- `tm.adapt adapter` follows `tm`, in the same states. -/ +lemma follows_adapt {k' : ℕ} {adapter : MultiTapeNTM.Adapter k k' Symbol State State} : + (tm.adapt adapter).Follows tm id adapter := + fun _ _ _ h => tr_iff.mp h ▸ rfl + /-! ## Stepping a Turing Machine @@ -169,27 +192,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 @@ -232,6 +234,17 @@ lemma RunPath.eq_take {p q : tm.RunPath input} (hhead : p.head = q.head) (h : p. rw [RelSeries.head_take, hhead] rfl +/-- Every computation prefix ends at a configuration of any halted computation path. -/ +lemma ComputationPath.last_mem_of_halted (p : tm.ComputationPath input) + {q : tm.ComputationPath input} (hq : q.last.Halted) : p.last ∈ q.toRunPath := by + rcases le_total p.length q.length with h | h + · have hp := RunPath.eq_take (p.head_eq.trans q.head_eq.symm) h + exact ⟨⟨p.length, Nat.lt_succ_of_le h⟩, (congrArg RelSeries.last hp).symm⟩ + · have hq' := congrArg RelSeries.last (RunPath.eq_take (q.head_eq.trans p.head_eq.symm) h) + rw [RelSeries.last_take] at hq' + rw [RunPath.last_eq_of_halted p.toRunPath _ (hq' ▸ hq), ← hq'] + exact RelSeries.last_mem _ + /-- The computation paths of a deterministic machine are prefixes of one another, so a path visiting at most as many cells as another visits at most as many on each tape. -/ lemma ComputationPath.spaceUsedByTape_le_of_space_le (p : tm.ComputationPath input) @@ -329,15 +342,65 @@ def Computes (tm : MultiTapeTM k Symbol State) (input output : List Symbol) : Pr ∃ u, (tm.runFrom (tm.initCfg input) u).Halted ∧ (tm.runFrom (tm.initCfg input) u).output = output +/-- The machine computes `output` from `input`, and `P` holds for this machine and input. -/ +def ComputesSuchThat (tm : MultiTapeTM k Symbol State) + (input output : List Symbol) (P : MultiTapeTM k Symbol State → List Symbol → Prop) : Prop := + tm.Computes input output ∧ P tm input + +/-- A condition on a computation can be weakened. -/ +theorem ComputesSuchThat.mono {output : List Symbol} + {P Q : MultiTapeTM k Symbol State → List Symbol → Prop} + (h : tm.ComputesSuchThat input output P) (hPQ : P tm input → Q tm input) : + tm.ComputesSuchThat input output Q := + ⟨h.1, hPQ h.2⟩ + +/-- The machine computes `output` from `input` within the given time bound. -/ +def ComputesInTime (tm : MultiTapeTM k Symbol State) + (input output : List Symbol) (t : ℕ) : Prop := + tm.ComputesSuchThat input output (fun tm input ↦ tm.RunsInTime input t) + +/-- The machine computes `output` from `input` within the given space bound. -/ +def ComputesInSpace (tm : MultiTapeTM k Symbol State) + (input output : List Symbol) (s : ℕ) : Prop := + tm.ComputesSuchThat input output (fun tm input ↦ tm.RunsInSpace input s) + /-- The machine computes `output` from `input` within the shared time and space bounds. -/ def ComputesInTimeAndSpace (tm : MultiTapeTM k Symbol State) (input output : List Symbol) (t s : ℕ) : Prop := - tm.Computes input output ∧ tm.RunsInTime input t ∧ tm.RunsInSpace input s + tm.ComputesSuchThat input output (fun tm input ↦ + tm.RunsInTime input t ∧ tm.RunsInSpace input s) + +/-- The machine computes `f` relative to given encodings. For each argument `a`, the predicate +`P a` holds for this machine and the encoded input `encIn a`. -/ +def ComputesFunSuchThat {α β : Type*} (tm : MultiTapeTM k Symbol State) + (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (f : α → β) + (P : α → MultiTapeTM k Symbol State → List Symbol → Prop) : Prop := + ∀ a, tm.ComputesSuchThat (encIn a) (encOut (f a)) (P a) + +/-- Conditions on a function computation can be weakened independently on every input. -/ +theorem ComputesFunSuchThat.mono {α β : Type*} + {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol} {f : α → β} + {P Q : α → MultiTapeTM k Symbol State → List Symbol → Prop} + (h : tm.ComputesFunSuchThat encIn encOut f P) + (hPQ : ∀ a, P a tm (encIn a) → Q a tm (encIn a)) : + tm.ComputesFunSuchThat encIn encOut f Q := + fun a ↦ (h a).mono (hPQ a) + +/-- The machine computes `f` relative to given encodings within the given time bound. -/ +def ComputesFunInTime {α β : Type*} (tm : MultiTapeTM k Symbol State) + (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (f : α → β) (t : α → ℕ) : Prop := + tm.ComputesFunSuchThat encIn encOut f (fun a tm input ↦ tm.RunsInTime input (t a)) + +/-- The machine computes `f` relative to given encodings within the given space bound. -/ +def ComputesFunInSpace {α β : Type*} (tm : MultiTapeTM k Symbol State) + (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (f : α → β) (s : α → ℕ) : Prop := + tm.ComputesFunSuchThat encIn encOut f (fun a tm input ↦ tm.RunsInSpace input (s a)) /-- The machine computes `f` relative to given encodings within the given time and space bounds. -/ def ComputesFunInTimeAndSpace {α β : Type*} (tm : MultiTapeTM k Symbol State) (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (f : α → β) (t s : α → ℕ) : Prop := - ∀ a, tm.ComputesInTimeAndSpace (encIn a) (encOut (f a)) (t a) (s a) + tm.ComputesFunSuchThat encIn encOut f + (fun a tm input ↦ tm.RunsInTime input (t a) ∧ tm.RunsInSpace input (s a)) /-- Resource bounds can be weakened independently on every input. -/ theorem ComputesFunInTimeAndSpace.mono {α β : Type*} @@ -345,15 +408,47 @@ theorem ComputesFunInTimeAndSpace.mono {α β : Type*} (h : tm.ComputesFunInTimeAndSpace encIn encOut f t s) (ht : ∀ a, t a ≤ t' a) (hs : ∀ a, s a ≤ s' a) : tm.ComputesFunInTimeAndSpace encIn encOut f t' s' := - fun a ↦ ⟨(h a).1, (h a).2.1.mono (ht a), (h a).2.2.mono (hs a)⟩ + ComputesFunSuchThat.mono h fun a ⟨hₜ, hₛ⟩ ↦ ⟨hₜ.mono (ht a), hₛ.mono (hs a)⟩ + +/-- Computability by a deterministic machine with a binary tape alphabet and finitely many states. +For each argument `a`, the predicate `P a` holds for this machine and the encoded input `encIn a`. +-/ +def ComputableSuchThat {α β : Type*} + (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) + (P : ∀ {k : ℕ} {State : Type}, α → MultiTapeTM k Bool State → List Bool → Prop) : Prop := + ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), + tm.ComputesFunSuchThat encIn encOut f P + +/-- Conditions on computability can be weakened independently on every input. -/ +theorem ComputableSuchThat.mono {α β : Type*} + {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} + {P Q : ∀ {k : ℕ} {State : Type}, α → MultiTapeTM k Bool State → List Bool → Prop} + (h : ComputableSuchThat f encIn encOut P) + (hPQ : ∀ {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) a, + P a tm (encIn a) → Q a tm (encIn a)) : + ComputableSuchThat f encIn encOut Q := by + obtain ⟨k, State, hfinite, tm, htm⟩ := h + exact ⟨k, State, hfinite, tm, htm.mono (hPQ tm)⟩ + +/-- Computability by a deterministic machine with a binary tape alphabet and finitely many states, +within the supplied input-indexed time bound. -/ +def ComputableInTime {α β : Type*} + (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t : α → ℕ) : Prop := + ComputableSuchThat f encIn encOut (fun a tm input ↦ tm.RunsInTime input (t a)) + +/-- Computability by a deterministic machine with a binary tape alphabet and finitely many states, +within the supplied input-indexed space bound. -/ +def ComputableInSpace {α β : Type*} + (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (s : α → ℕ) : Prop := + ComputableSuchThat f encIn encOut (fun a tm input ↦ tm.RunsInSpace input (s a)) /-- Computability by a deterministic machine with a binary tape alphabet and finitely many states, within the supplied input-indexed bounds. -/ def ComputableInTimeAndSpace {α β : Type*} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t s : α → ℕ) : Prop := - ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), - tm.ComputesFunInTimeAndSpace encIn encOut f t s + ComputableSuchThat f encIn encOut + (fun a tm input ↦ tm.RunsInTime input (t a) ∧ tm.RunsInSpace input (s a)) /-- There exists a binary Turing machine with finitely many states that, for every input `a`, computes `encOut (f a)` from `encIn a` in at most `t (encIn a).length` steps, @@ -369,45 +464,52 @@ theorem ComputableInTimeAndSpace.mono {α β : Type*} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s t' s' : α → ℕ} (h : ComputableInTimeAndSpace f encIn encOut t s) (ht : ∀ a, t a ≤ t' a) (hs : ∀ a, s a ≤ s' a) : - ComputableInTimeAndSpace f encIn encOut t' s' := by - obtain ⟨k, State, hfinite, tm, htm⟩ := h - exact ⟨k, State, hfinite, tm, htm.mono ht hs⟩ + ComputableInTimeAndSpace f encIn encOut t' s' := + ComputableSuchThat.mono h fun _ a ⟨hₜ, hₛ⟩ ↦ ⟨hₜ.mono (ht a), hₛ.mono (hs a)⟩ open scoped Classical in /-- The Boolean indicator function of a set. -/ noncomputable def indicator {α : Type*} (L : Set α) : α → Bool := fun x => if x ∈ L then true else false +/-- A set is decidable within the given input-indexed space bound when its Boolean indicator is +computable in that bound. -/ +def DecidableInSpace {α : Type*} (L : Set α) (enc : α ↪ List Bool) (s : α → ℕ) : Prop := + ComputableInSpace (indicator L) enc ⟨fun b ↦ [b], by intro a b h; simpa using h⟩ s + /-- A set is decidable within the given input-indexed bounds when its Boolean indicator is computable in those bounds. -/ def DecidableInTimeAndSpace {α : Type*} (L : Set α) (enc : α ↪ List Bool) (t s : α → ℕ) : Prop := ComputableInTimeAndSpace (indicator L) enc ⟨fun b ↦ [b], by intro a b h; simpa using h⟩ t s -/-- If a deterministic machine repeats a non-halting configuration, it never halts, -because the sequence between the two configurations will loop forever. -Note that this can be applied to two arbitrary and different time steps `t` and `t + Δ` -using `Function.iterate_add_apply`. -/ -lemma not_halts_of_repeat_nonhalt - (cfg : Cfg k Symbol State input) - (h_not_halt : cfg.state ≠ none) - (t : ℕ) - (heq : tm.runFrom cfg (t + 1) = cfg) : - ∀ t', (tm.runFrom cfg t').state ≠ none := by - intro t' - -- The configuration will repeat every `t + 1` steps. - have hloop : ∀ n, tm.runFrom cfg (n * (t + 1)) = cfg := by - intro n - unfold runFrom - rw [Nat.mul_comm, Function.iterate_mul] - exact Function.iterate_fixed heq n - by_contra hnh - -- Assuming the machine halts at step `t'`, it is also halted at step `t' * (t + 1)` - have h₁ : (tm.runFrom cfg (t' * (t + 1))).state = none := by - have hle : t' ≤ t' * (t + 1) := by grind - rwa [tm.runFrom_eq_of_halt cfg hle hnh] - simp [hloop t', h_not_halt] at h₁ - end MultiTapeTM +namespace MultiTapeNTM.RunPath + +variable {tm : MultiTapeTM k Symbol State} {input : List Symbol} + +/-- A deterministic path that ends halted never repeats a running configuration: from a repeated +configuration the machine would cycle forever. -/ +lemma injOn_running (p : tm.RunPath input) + (h : p.last.Halted) : Set.InjOn p {i | ¬(p i).Halted} := by + -- a repeat `p i = p j` with `i < j` is followed by the repeat `p (i + 1) = p (j + 1)`, so halting + -- at the end comes back to `p j` + have halted (j : Fin (p.length + 1)) : ∀ i < j, p i = p j → (p j).Halted := by + induction j using Fin.reverseInduction with + | last => exact fun _ _ _ ↦ h + | cast j ih => + intro i hij heq + obtain ⟨i, rfl⟩ := Fin.exists_castSucc_eq.mpr (Fin.ne_last_of_lt hij) + rw [Fin.castSucc_lt_castSucc_iff] at hij + have hsucc : p i.succ = p j.succ := by + rw [← MultiTapeTM.step_iff.mp (p.step i), ← MultiTapeTM.step_iff.mp (p.step j), heq] + exact p.halted_mono (Fin.succ_le_castSucc_iff.mpr hij) + (hsucc ▸ ih _ (Fin.succ_lt_succ_iff.mpr hij) hsucc : (p i.succ).Halted) + intro i hi j hj hij + rcases lt_trichotomy i j with hlt | rfl | hlt + exacts [(hj (halted j i hlt hij)).elim, rfl, (hi (halted i j hlt hij.symm)).elim] + +end MultiTapeNTM.RunPath + end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/InputShortening.lean b/Cslib/Computability/Machines/Turing/MultiTape/InputShortening.lean new file mode 100644 index 000000000..d3cefba21 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/InputShortening.lean @@ -0,0 +1,479 @@ +/- +Copyright (c) 2026 Aviv Bar Natan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aviv Bar Natan +-/ +module + +public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound +public import Mathlib.Data.Finset.Sort +public import Mathlib.Data.Fintype.Pigeonhole +public import Mathlib.Order.Atoms.Finite +public import Mathlib.Order.Cover +public import Mathlib.Order.Interval.Basic + +/-! +# Input shortening for multi-tape Turing machines + +Consider a deterministic Turing machine and a computation path on an input that ends halted. For +each input cell, we record the sequence of storages (`Storage`) of the running configurations of +the path that read that cell. If two distinct cells contain the same symbol and have the same +sequence, then deleting the symbols after the first cell through the second preserves every +storage reached by a step on either retained side. This property is the main ingredient in the +proof of `SPACE(o(log log n)) = SPACE(1)`. + +The proof idea follows [Katz2007], §1.2, Theorem 4. + +## Design + +Collapsing the deleted cells onto the first cell maps the steps that stay on one retained side to +steps on the shortened input (`InputCut.stepHom`), so it maps such run paths with `RelSeries.map`. +The image forgets the output: the machine never reads it, and paired visits to the two endpoints +have equal storages but possibly different outputs. Their images are then equal configurations of +`MultiTapeTM.eraseOutput`, so the mapped segments of the path join with `RelSeries.smash`. + +## Main definitions + +* `MultiTapeNTM.RunPath.visits`: the indices of the running configurations reading a position. +* `MultiTapeNTM.RunPath.visitSequence`: the storages at those indices, in chronological order. +* `MultiTapeTM.eraseOutput`, `MultiTapeTM.eraseOutputHom`: the machine with its output writes + erased, and the map erasing the output, which preserves steps. +* `InputCut`: an ordered pair of input-symbol indices describing the endpoints of a deletion. +* `InputCut.shortened`: the input with the symbols after the first endpoint through the second + deleted. +* `InputCut.SameSide`: two input-head positions on one retained side of the cut. +* `InputCut.cfg`: a configuration seen on the shortened input, with its output erased. +* `InputCut.stepHom`: `cfg` as a homomorphism from the steps on one retained side. + +## Main results + +* `MultiTapeNTM.RunPath.storage_injOn_visits`: distinct running visits to a position in a path that + ends halted have distinct storages. +* `InputCut.exists_storage_eq`: equal boundary symbols and visit sequences preserve the storage + reached by a step on a retained side, including a step that halts. +* `MultiTapeTM.exists_shorter_input_storage`: a sufficiently long input to a machine running in + bounded space has a shorter input reaching any storage of a halting computation path. + +## References + +* [Jonathan Katz, *Notes on Complexity Theory, Lecture 5*][Katz2007], + §1.2, Theorem 4, pp. 5-2–5-4. +-/ + +@[expose] public section + +namespace Turing + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +namespace MultiTapeTM + +/-- `tm` with its output writes erased. A machine never reads its output tape, so the erased machine +takes the same steps up to the output. -/ +noncomputable def eraseOutput (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol State := + tm.adapt { read := id, action := fun _ a => { a with output := none } } + +/-- Erasing the output preserves steps, so it maps run paths of `tm` to run paths of +`tm.eraseOutput`. -/ +noncomputable def eraseOutputHom (tm : MultiTapeTM k Symbol State) : + (tm.stepRel input).Hom (tm.eraseOutput.stepRel input) := + follows_adapt.stepHom (fun c => { c with output := [] }) (fun _ => Option.map_id_apply) + (fun _ => rfl) fun _ _ => by simp [Action.apply] + +end MultiTapeTM + +namespace MultiTapeNTM.RunPath + +variable {ntm : MultiTapeNTM k Symbol State} + +/-- The indices at which a run path reads input position `pos` in a running configuration. -/ +def visits (p : ntm.RunPath input) (pos : ℕ) : Finset (Fin (p.length + 1)) := + {i | (p i).inputPos.val = pos ∧ ¬(p i).Halted} + +@[simp] +lemma mem_visits {p : ntm.RunPath input} {pos : ℕ} {i : Fin (p.length + 1)} : + i ∈ p.visits pos ↔ (p i).inputPos.val = pos ∧ ¬(p i).Halted := by + simp [visits] + +/-- The storages at the running visits to `pos`, in chronological order. -/ +def visitSequence (p : ntm.RunPath input) (pos : ℕ) : List (Storage Symbol State k) := + ((p.visits pos).sort (· ≤ ·)).map fun i ↦ (p i).storage + +/-- In a deterministic path that ends halted, distinct running visits to a position have distinct +storages: they would be equal configurations of the machine with its output erased. -/ +lemma storage_injOn_visits {tm : MultiTapeTM k Symbol State} (p : tm.RunPath input) + (h : p.last.Halted) (pos : ℕ) : Set.InjOn (fun i ↦ (p i).storage) (p.visits pos) := by + intro i hi j hj hij + simp only [Finset.mem_coe, mem_visits] at hi hj + refine injOn_running (tm := tm.eraseOutput) (p.map tm.eraseOutputHom) h hi.2 hj.2 ?_ + simp only [Cfg.storage, Storage.mk.injEq] at hij + exact Cfg.ext hij.1 (Fin.ext (hi.1.trans hj.1.symm)) hij.2.1 hij.2.2 rfl + +end MultiTapeNTM.RunPath + +/-- An ordered pair of input-symbol indices. The cut deletes the symbols after the first +through the second. Equal endpoints give an empty deletion. +`fst` and `snd` are zero-based list indices. `left` and `right` are the corresponding +input-head positions, offset by one because position `0` is the left endmarker. -/ +abbrev InputCut (input : List Symbol) := NonemptyInterval (Fin input.length) + +namespace InputCut + +variable (cut : InputCut input) + +/-- The head position of the retained endpoint: position `0` is the left endmarker. -/ +def left : ℕ := cut.fst.val + 1 + +/-- The head position of the right endpoint: input symbol `i` is read at position `i + 1`. -/ +def right : ℕ := cut.snd.val + 1 + +/-- The input obtained by deleting the cells after `left` through `right`. -/ +def shortened : List Symbol := + input.take cut.left ++ input.drop cut.right + +/-- Two input positions lie on the same retained side of the cut. -/ +def SameSide (p q : ℕ) : Prop := + (p ≤ cut.left ∧ q ≤ cut.left) ∨ (cut.right ≤ p ∧ cut.right ≤ q) + +/-- Adding back the deleted cells recovers the original input length. -/ +lemma length_shortened_add : + cut.shortened.length + (cut.right - cut.left) = input.length := by + grind [shortened, left, right, cut.fst_le_snd] + +/-- Collapse the deleted cells onto the left endpoint and shift later positions left. -/ +def inputPos (p : Fin (input.length + 2)) : Fin (cut.shortened.length + 2) := + ⟨min p.val cut.left + (p.val - cut.right), by + have := cut.length_shortened_add + grind [left, right, cut.fst_le_snd, Fin.le_def]⟩ + +/-- Collapsing the cut commutes with an input-head move that stays on one retained side. -/ +lemma inputPos_moveInputPos {p : Fin (input.length + 2)} {m : SignType} + (h : cut.SameSide p (moveInputPos p m)) : + cut.inputPos (moveInputPos p m) = moveInputPos (cut.inputPos p) m := by + have := val_moveInputPos_eq p m + have := val_moveInputPos_eq (cut.inputPos p) m + apply Fin.ext + cases m <;> grind [SameSide, inputPos, left, right, SignType.cast, + Fin.le_def, cut.fst_le_snd, cut.length_shortened_add] + +/-- A configuration on the original input, seen on the shortened input with its output erased. -/ +def cfg (c : Cfg k Symbol State input) : Cfg k Symbol State cut.shortened := + ⟨c.state, cut.inputPos c.inputPos, c.workTapes, c.workTapePos, []⟩ + +/-- Outside the deleted cells, the collapsed configuration reads the same symbol when the endpoints +carry the same symbol. -/ +lemma inputSymbol_cfg (hsym : input[cut.fst] = input[cut.snd]) {c : Cfg k Symbol State input} + (hp : c.inputPos.val ≤ cut.left ∨ cut.right ≤ c.inputPos.val) : + (cut.cfg c).inputSymbol = c.inputSymbol := by + have he {l : List Symbol} (c : Cfg k Symbol State l) : + c.inputSymbol = if c.inputPos.val = 0 then none else l[c.inputPos.val - 1]? := by + grind [Cfg.inputSymbol] + have hb : input[cut.left - 1]? = input[cut.right - 1]? := by + simpa [left, right, Fin.getElem_fin] using congrArg some hsym + simp only [he, cfg, inputPos, shortened, List.getElem?_append, List.length_take, + List.getElem?_take, List.getElem?_drop] at * + grind [left, right, cut.fst_le_snd, Fin.le_def] + +variable {tm : MultiTapeTM k Symbol State} + +/-- The steps of `tm` that stay on one retained side of the cut. -/ +abbrev sideStepRel (tm : MultiTapeTM k Symbol State) : + SetRel (Cfg k Symbol State input) (Cfg k Symbol State input) := + {(c, c') | tm.Step c c' ∧ cut.SameSide c.inputPos c'.inputPos} + +/-- When the endpoints carry the same symbol, collapsing the cut maps the steps on either retained +side to steps of `tm.eraseOutput` on the shortened input: `cfg` agrees with the adapter erasing the +output on such steps. -/ +noncomputable def stepHom (hsym : input[cut.fst] = input[cut.snd]) : + (cut.sideStepRel tm).Hom (tm.eraseOutput.stepRel cut.shortened) := + ⟨cut.cfg, fun ⟨hstep, hside⟩ ↦ MultiTapeTM.follows_adapt.step cut.cfg hstep Option.map_id_apply + (HeadSymbols.ext (cut.inputSymbol_cfg hsym (by unfold SameSide at hside; omega)) rfl) + fun _ ↦ by rintro rfl; exact Cfg.ext rfl (cut.inputPos_moveInputPos hside).symm rfl rfl rfl⟩ + +/-! ### Simulating a computation path on the shortened input -/ + +open MultiTapeNTM MultiTapeNTM.RunPath + +/-- The image of `c` on the shortened input is the last configuration of a computation path of the +machine with its output erased. -/ +private abbrev Reached (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) : Prop := + ∃ q : tm.eraseOutput.ComputationPath cut.shortened, q.last = cut.cfg c + +/-- The image of the initial configuration is reached. -/ +private lemma reached_head {p : tm.ComputationPath input} : cut.Reached tm p.toRunPath.head := + ⟨⟨RelSeries.singleton _ (tm.eraseOutput.initCfg cut.shortened), rfl⟩, by + rw [p.head_eq] + exact Cfg.ext rfl (Fin.ext (by simp [cfg, inputPos, Cfg.init, left, right])) rfl rfl rfl⟩ + +/-- The running visits to the two endpoints, paired in chronological order, with the same image on +the shortened input. -/ +private structure Pairing (p : tm.RunPath input) where + /-- The `n`-th visit to the left endpoint is paired with the `n`-th visit to the right one. -/ + orderIso : p.visits cut.left ≃o p.visits cut.right + /-- Paired visits have the same image on the shortened input. -/ + cfg_eq (u : p.visits cut.left) : cut.cfg (p u.val) = cut.cfg (p (orderIso u).val) + +/-- Equal visit sequences pair the visits of the same index, which have equal storages. -/ +private def pairing {p : tm.RunPath input} + (hseq : p.visitSequence cut.left = p.visitSequence cut.right) : cut.Pairing p := by + have hcard : (p.visits cut.right).card = (p.visits cut.left).card := by + simpa [visitSequence] using congrArg List.length hseq.symm + let l := (p.visits cut.left).orderIsoOfFin rfl + let r := (p.visits cut.right).orderIsoOfFin hcard + refine ⟨l.symm.trans r, fun u ↦ ?_⟩ + obtain ⟨n, rfl⟩ := l.surjective u + have hs : (p (l n)).storage = (p (r n)).storage := by + simpa [visitSequence, hcard, l, r, Finset.coe_orderIsoOfFin_apply, + Finset.orderEmbOfFin_apply] using congrArg (·[n.val]?) hseq + have hl := (mem_visits.mp (l n).property).1 + have hr := (mem_visits.mp (r n).property).1 + simp only [Cfg.storage, Storage.mk.injEq] at hs + simp only [OrderIso.trans_apply, OrderIso.symm_apply_apply] + refine Cfg.ext hs.1 (Fin.ext ?_) hs.2.1 hs.2.2 rfl + grind [cfg, inputPos, left, right, cut.fst_le_snd, Fin.le_def] + +variable {cut} (hsym : input[cut.fst] = input[cut.snd]) +include hsym + +/-- A step on a retained side extends a computation path on the shortened input. -/ +private lemma Reached.step {c c' : Cfg k Symbol State input} (h : cut.Reached tm c) + (hstep : tm.Step c c') (hside : cut.SameSide c.inputPos c'.inputPos) : + cut.Reached tm c' := by + obtain ⟨q, hq⟩ := h + have hr : (q.last, cut.cfg c') ∈ tm.eraseOutput.stepRel cut.shortened := + hq ▸ (cut.stepHom hsym).map_rel (show (c, c') ∈ cut.sideStepRel tm from ⟨hstep, hside⟩) + exact ⟨⟨q.toRunPath.snoc _ hr, (RelSeries.head_snoc ..).trans q.head_eq⟩, + RelSeries.last_snoc q.toRunPath _ hr⟩ + +/-- A run path on a retained side extends a computation path on the shortened input. -/ +private lemma Reached.path {p : tm.RunPath input} (h : cut.Reached tm p.head) + (hp : (∀ c ∈ p, c.inputPos.val ≤ cut.left) ∨ ∀ c ∈ p, cut.right ≤ c.inputPos.val) : + cut.Reached tm p.last := + -- `p` is a series of side steps, which `stepHom` maps + let s : RelSeries (cut.sideStepRel tm) := ⟨p.length, p, fun i ↦ ⟨p.step i, + hp.imp (fun h ↦ ⟨h _ ⟨_, rfl⟩, h _ ⟨_, rfl⟩⟩) fun h ↦ ⟨h _ ⟨_, rfl⟩, h _ ⟨_, rfl⟩⟩⟩⟩ + let ⟨q, hq⟩ := h + ⟨⟨q.toRunPath.smash (s.map (cut.stepHom hsym)) hq, + (RelSeries.head_smash _).trans q.head_eq⟩, RelSeries.last_smash hq⟩ + +/-- From `a` up to the next running visit `v` to `pos`, the path stays on the side of `pos` where +it is at `a`, so the image of `p a` reaches that of `p v`. -/ +private lemma Reached.slice {p : tm.RunPath input} {pos : ℕ} {a : Fin (p.length + 1)} + {v : p.visits pos} (hfirst : IsLeast {w : p.visits pos | a ≤ w.val} v) + (hside : ((p a).inputPos.val ≤ pos ∧ pos ≤ cut.left) ∨ + (pos ≤ (p a).inputPos.val ∧ cut.right ≤ pos)) + (h : cut.Reached tm (p a)) : cut.Reached tm (p v.val) := by + obtain ⟨hav, hnext⟩ := hfirst + let s := (p.take v.val).drop ⟨a, Nat.lt_succ_of_le hav⟩ + have hs : s.head = p a := by simp [s, RelSeries.take] + have hne (i : Fin s.length) : (s i.castSucc).inputPos.val ≠ pos := by + intro hi + have hi' : i.val + a.val < v.val.val := by + have : i.val < v.val.val - a.val := i.isLt + omega + exact (hnext (a := ⟨⟨_, hi'.trans v.val.isLt⟩, mem_visits.mpr + ⟨hi, mt (p.halted_mono hi'.le) (mem_visits.mp v.property).2⟩⟩) + (show a.val ≤ i.val + a.val by omega)).not_gt hi' + simpa [s] using Reached.path hsym (p := s) (hs ▸ h) (by + rcases hside with hl | hr + · exact .inl fun c hc => ((inputPos_side s hne hc).1 (hs.symm ▸ hl.1)).trans hl.2 + · exact .inr fun c hc => hr.2.trans ((inputPos_side s hne hc).2 (hs.symm ▸ hr.1))) + +/-- Between consecutive running visits `u ⋖ v` to `pos`, the path continues on the side its first +step enters, so the image of the visit `u` reaches that of `v`. -/ +private lemma Reached.covBy {p : tm.RunPath input} {pos : ℕ} {u v : p.visits pos} (huv : u ⋖ v) + (h : cut.Reached tm (p u.val)) + (hside : ((tm.step (p u.val)).inputPos.val ≤ pos ∧ pos ≤ cut.left) ∨ + (pos ≤ (tm.step (p u.val)).inputPos.val ∧ cut.right ≤ pos)) : + cut.Reached tm (p v.val) := by + have hlt : u.val.val < p.length := lt_of_lt_of_le huv.lt (Nat.lt_succ_iff.mp v.val.isLt) + have hu := (mem_visits.mp u.property).1 + have hpi : tm.Step (p u.val) (p (⟨u.val, hlt⟩ : Fin p.length).succ) := p.step ⟨u.val, hlt⟩ + rw [MultiTapeTM.step_iff.mp hpi] at hside + refine Reached.slice hsym ?_ hside (h.step hsym hpi (by unfold SameSide; omega)) + exact ⟨Nat.succ_le_of_lt huv.lt, fun _ hw => huv.ge_of_gt hw⟩ + +/-- At paired visits, the step from the left visit stays left or that from the right visit stays +right: both read the same symbol with the same storage, so they move the input head alike. -/ +private lemma Pairing.step_sides {p : tm.RunPath input} (e : cut.Pairing p) + (u : p.visits cut.left) : + (tm.step (p u.val)).inputPos.val ≤ cut.left ∨ + cut.right ≤ (tm.step (p (e.orderIso u).val)).inputPos.val := by + have hl := mem_visits.mp u.property + have hr := (mem_visits.mp (e.orderIso u).property).1 + have he := e.cfg_eq u + have hw : (p u.val).workTapeSymbols = (p (e.orderIso u).val).workTapeSymbols := + congrArg (·.workTapeSymbols) he + obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp hl.2 + rw [MultiTapeTM.step_inputPos_of_state hq, + MultiTapeTM.step_inputPos_of_state (show (p (e.orderIso u).val).state = some q from + (congrArg Cfg.state he).symm.trans hq), + ← cut.inputSymbol_cfg hsym (.inl hl.1.le), he, cut.inputSymbol_cfg hsym (.inr hr.ge), + hw] + generalize (tm.tr q _ _).inputTape = m + have := val_moveInputPos_eq (p u.val).inputPos m + have := val_moveInputPos_eq (p (e.orderIso u).val).inputPos m + cases m <;> simp -failIfUnchanged [SignType.cast] at * <;> omega + +/-- Every running visit to the left endpoint is reached, by induction over the visits. -/ +private lemma Pairing.reached {p : tm.ComputationPath input} (e : cut.Pairing p.toRunPath) + (u : visits p.toRunPath cut.left) : cut.Reached tm (p.toRunPath u.val) := by + induction u using WellFoundedLT.induction with | ind u ih => + by_cases hu : IsMin u + · exact Reached.slice hsym ⟨Fin.zero_le _, fun w _ => (le_total u w).elim id (hu ·)⟩ + (.inl ⟨by simp [show p.toRunPath 0 = _ from p.head_eq, left], le_rfl⟩) (reached_head cut) + obtain ⟨w, hwu⟩ := not_isMin_iff.mp hu + obtain ⟨v, -, hvu⟩ := exists_le_covBy_of_lt hwu + rcases e.step_sides hsym v with hl | hr + · exact Reached.covBy hsym hvu (ih v hvu.lt) (.inl ⟨hl, le_rfl⟩) + · have := ih v hvu.lt + rw [Reached, e.cfg_eq] at this ⊢ + exact Reached.covBy hsym ((apply_covBy_apply_iff e.orderIso).mpr hvu) this (.inr ⟨hr, le_rfl⟩) + +/-- Every running configuration outside the deleted cells is reached, by induction over the +path. -/ +private lemma Pairing.reached_of_not_halted {p : tm.ComputationPath input} + (e : cut.Pairing p.toRunPath) {c : Cfg k Symbol State input} (hc : c ∈ p.toRunPath) + (ht : ¬c.Halted) (hout : c.inputPos.val ≤ cut.left ∨ cut.right ≤ c.inputPos.val) : + cut.Reached tm c := by + obtain ⟨t, rfl⟩ := hc + induction t using Fin.induction with + | zero => exact reached_head cut + | succ t ih => + by_cases hb : (p.toRunPath t.succ).inputPos.val = cut.left + · exact e.reached hsym ⟨_, mem_visits.mpr ⟨hb, ht⟩⟩ + by_cases hb' : (p.toRunPath t.succ).inputPos.val = cut.right + · have := e.reached hsym (e.orderIso.symm ⟨_, mem_visits.mpr ⟨hb', ht⟩⟩) + rwa [Reached, e.cfg_eq, OrderIso.apply_symm_apply] at this + have hm := abs_le.mp (Step.inputPos_le (p.step t)) + have hside : cut.SameSide (p.toRunPath t.castSucc).inputPos (p.toRunPath t.succ).inputPos := by + unfold SameSide + omega + refine (ih (mt (halted_mono _ (Fin.castSucc_lt_succ ..).le) ht) ?_).step hsym (p.step t) hside + unfold SameSide at hside + omega + +omit hsym in +variable (cut) in +/-- **Input shortening.** If the endpoints of the cut carry the same symbol and a computation path +visits them with the same storages, a step on a retained side from a running configuration of the +path reaches the same storage on the shortened input. -/ +theorem exists_storage_eq (hsym : input[cut.fst] = input[cut.snd]) + {path : tm.ComputationPath input} + (hseq : visitSequence path.toRunPath cut.left = visitSequence path.toRunPath cut.right) + {c : Cfg k Symbol State input} (hc : c ∈ path.toRunPath) (hrun : ¬c.Halted) + (hside : cut.SameSide c.inputPos (tm.step c).inputPos) : + ∃ q : tm.ComputationPath cut.shortened, q.last.storage = (tm.step c).storage := by + obtain ⟨q, hq⟩ := ((cut.pairing hseq).reached_of_not_halted hsym hc hrun + (by unfold SameSide at hside; omega)).step hsym (MultiTapeTM.step_iff.mpr rfl) hside + -- the path of the same length of `tm` erases to `q` + refine ⟨.ofDeterministic tm cut.shortened q.time, ?_⟩ + rw [q.eq_ofDeterministic] at hq + have hp := RunPath.map_ofDeterministic tm.eraseOutputHom (tm.initCfg cut.shortened) q.time + exact (congrArg (·.last.storage) hp).trans (congrArg Cfg.storage hq) + +end InputCut + +namespace MultiTapeTM + +variable {tm : MultiTapeTM k Symbol State} + +open MultiTapeNTM MultiTapeNTM.RunPath + +/-- On a sufficiently long input, two cells on the same side of `pos` carry the same symbol and +visit sequence, and deleting between them shortens the input. -/ +private lemma exists_inputCut [Fintype Symbol] [Fintype State] {s : ℕ} + {path : tm.ComputationPath input} (hs : path.space ≤ s) (hhalt : path.last.Halted) + (hlen : 2 * Fintype.card Symbol * + (storageBound Symbol State k s + 1) ^ storageBound Symbol State k s + 1 < input.length) + (pos : ℕ) : + ∃ cut : InputCut input, cut.shortened.length < input.length ∧ + input[cut.fst] = input[cut.snd] ∧ + visitSequence path.toRunPath cut.left = visitSequence path.toRunPath cut.right ∧ + (cut.left < pos ↔ cut.right < pos) := by + classical + let P := path.toRunPath + -- Every prefix fits in the windows given by the space of this path. + let w := spaceUsedByTape P + let B := storageBound Symbol State k s + have hS (t : Fin (path.length + 1)) : (P t).storage.FitsIn w := by + let q : tm.ComputationPath input := ⟨P.take t, by simp [P, path.head_eq]⟩ + exact Storage.FitsIn_mono + (fun j => Finset.card_le_card (visitedByTapeHead_take_subset P t j)) q.storage_fitsIn + have hfits {pos n : ℕ} {x} (hx : (visitSequence P pos)[n]? = some x) : x.FitsIn w := by + obtain ⟨t, -, rfl⟩ := List.mem_map.mp (List.mem_of_getElem? hx) + exact hS t + have hcard : Fintype.card (BoundedStorage Symbol State w) ≤ B := card_boundedStorage_le hs + have hlength (pos : ℕ) : (visitSequence P pos).length ≤ B := by + simp only [visitSequence, List.length_map, Finset.length_sort] + exact (Finset.card_le_card_of_injOn (fun t ↦ (P t).storage.toBounded w) + (fun _ _ ↦ Finset.mem_coe.mpr (Finset.mem_univ _)) fun u hu v hv h ↦ + storage_injOn_visits P hhalt pos hu hv (Storage.toBounded_injOn w (hS u) (hS v) h)).trans + (by simpa using hcard) + -- Record the side of `pos`, the input symbol, and the bounded visit sequence. + let f (j : Fin input.length) : Bool × Symbol × (Fin B → Option (BoundedStorage Symbol State w)) := + (decide (j.val + 1 < pos), input[j], fun n ↦ ((visitSequence P (j.val + 1))[n.val]?).map + (·.toBounded w)) + have hsig : Fintype.card (Bool × Symbol × (Fin B → Option (BoundedStorage Symbol State w))) < + input.length := by + rw [Fintype.card_prod, Fintype.card_prod, Fintype.card_bool, Fintype.card_fun, + Fintype.card_option, Fintype.card_fin, ← mul_assoc] + calc + _ ≤ 2 * Fintype.card Symbol * (B + 1) ^ B := by gcongr; omega + _ < input.length := by dsimp only [B]; omega + obtain ⟨a, b, hab, hf⟩ : ∃ a b, a < b ∧ f a = f b := by + obtain ⟨a, b, hne, hf⟩ := Fintype.exists_ne_map_eq_of_card_lt f (by simpa using hsig) + grind + obtain ⟨hside, hsym, hseq⟩ := (by simpa only [f, Prod.mk.injEq, decide_eq_decide] using hf) + have hseq' : visitSequence P (a.val + 1) = visitSequence P (b.val + 1) := by + apply List.ext_getElem?' + intro r hr + have he := congrFun hseq ⟨r, hr.trans_le (max_le (hlength _) (hlength _))⟩ + rcases ha : (visitSequence P (a.val + 1))[r]? with _ | x <;> + rcases hb : (visitSequence P (b.val + 1))[r]? with _ | y <;> + simp only [ha, hb, Option.map_none, Option.map_some, reduceCtorEq, Option.some.injEq] + at he ⊢ + exact Storage.toBounded_injOn w (hfits ha) (hfits hb) he + let cut : InputCut input := ⟨⟨a, b⟩, hab.le⟩ + refine ⟨cut, ?_, hsym, hseq', hside⟩ + have := cut.length_shortened_add + change cut.shortened.length + (b.val + 1 - (a.val + 1)) = input.length at this + omega + +/-- **Input shortening.** A sufficiently long input to a machine running in space `s` has a shorter +input on which a computation path reaches any storage of a halting computation path. -/ +theorem exists_shorter_input_storage [Fintype Symbol] [Fintype State] {s : ℕ} + (hs : tm.RunsInSpace input s) {path : tm.ComputationPath input} (hhalt : path.last.Halted) + (hlen : 2 * Fintype.card Symbol * + (storageBound Symbol State k s + 1) ^ storageBound Symbol State k s + 1 < input.length) + {d : Cfg k Symbol State input} (hd : d ∈ path.toRunPath) : + ∃ input' : List Symbol, input'.length < input.length ∧ + ∃ q : tm.ComputationPath input', q.last.storage = d.storage := by + let P := path.toRunPath + obtain ⟨j, rfl⟩ := hd + induction j using Fin.induction with + | zero => + -- the initial storage does not depend on the input + refine ⟨[], by simp; omega, .ofDeterministic tm [] 0, ?_⟩ + change (tm.initCfg []).storage = P.head.storage + rw [path.head_eq] + rfl + | succ i ih => + by_cases hi : (P i.castSucc).Halted + · rw [(MultiTapeNTM.step_of_halt hi).mp (P.step i)] + exact ih + -- Matching cells on the same side of both head positions retain this step. + obtain ⟨cut, hshort, hsym, hseq, hside⟩ := + exists_inputCut (hs path) hhalt hlen (max (P i.castSucc).inputPos.val (P i.succ).inputPos.val) + refine ⟨cut.shortened, hshort, ?_⟩ + have hstep : tm.step (P i.castSucc) = P i.succ := step_iff.mp (P.step i) + rw [← hstep] + refine cut.exists_storage_eq hsym hseq ⟨_, rfl⟩ hi ?_ + have := abs_le.mp (Step.inputPos_le (P.step i)) + rw [hstep] + unfold InputCut.SameSide + omega + +end MultiTapeTM + +end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/LoglognEqualsNoSpace.lean b/Cslib/Computability/Machines/Turing/MultiTape/LoglognEqualsNoSpace.lean new file mode 100644 index 000000000..d4594a7cc --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/LoglognEqualsNoSpace.lean @@ -0,0 +1,137 @@ +/- +Copyright (c) 2026 Aviv Bar Natan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aviv Bar Natan +-/ +module + +public import Cslib.Computability.Machines.Turing.MultiTape.InputShortening +public import Cslib.Foundations.Analysis.Asymptotics +public import Mathlib.Computability.Language + +/-! +# Subloglog space equals constant space + +A halting deterministic machine whose space usage is `o(log log n)` uses uniformly bounded space. +The proof idea follows [Katz2007], §1.2, Theorem 4. Its main ingredient is formalized in +`Cslib.Computability.Machines.Turing.MultiTape.InputShortening`. + +## Main results + +* `exists_const_space_of_isLittleO_log_log`: the same machine uses constant space on every input. +* `ComputableInSpace.exists_const_space`: a function computable in subloglog space is computable in + constant space. +* `DecidableInSpace.exists_const_space`: a language decidable in subloglog space is decidable in + constant space. +* `loglogn_equals_no_space`: `SPACE(o(log log n)) = SPACE(1)` for binary languages. + +## References + +* [Jonathan Katz, *Notes on Complexity Theory, Lecture 5*][Katz2007], + §1.2, Theorem 4, pp. 5-2–5-4. +-/ + +@[expose] public section + +open Filter Asymptotics + +namespace Turing.MultiTapeTM + +/-- For `s(n) = o(log log n)`, sufficiently long inputs exceed the shortening threshold. -/ +private lemma eventually_visit_bound_lt {Symbol State : Type*} [Fintype Symbol] [Fintype State] + (k : ℕ) {s : ℕ → ℕ} + (hs : (fun n ↦ (s n : ℝ)) =o[atTop] (fun n ↦ Real.log (Real.log (n : ℝ)))) : + ∀ᶠ n in atTop, 2 * Fintype.card Symbol * + (storageBound Symbol State k (s n) + 1) ^ storageBound Symbol State k (s n) + 1 < n := by + obtain ⟨a, c, hbound⟩ := storageBound_pow_le_pow_pow (Symbol := Symbol) (State := State) (k := k) + (2 * Fintype.card Symbol) + have hlog := Real.tendsto_log_atTop.comp (tendsto_natCast_atTop_atTop (R := ℝ)) + have hc : (fun _ : ℕ ↦ (a : ℝ)) =o[atTop] (fun n ↦ Real.log (Real.log (n : ℝ))) := + Real.isLittleO_const_log_atTop.comp_tendsto hlog + have hlin : (fun n ↦ ((a + c * s n : ℕ) : ℝ)) =o[atTop] + (fun n ↦ Real.log (Real.log (n : ℝ))) := by + simpa only [Nat.cast_add, Nat.cast_mul] using hc.add (hs.const_mul_left (c : ℝ)) + have hsmall : (fun n ↦ ((2 ^ (2 ^ (a + c * s n)) : ℕ) : ℝ)) =o[atTop] + (fun n ↦ (n : ℝ)) := + (hlin.natCast_const_pow hlog (by decide)).natCast_const_pow + tendsto_natCast_atTop_atTop (by decide) + have hsmall' := hsmall.add ((isLittleO_const_id_atTop (1 : ℝ)).comp_tendsto + tendsto_natCast_atTop_atTop) + have hpos : ∀ᶠ n : ℕ in atTop, 0 < ‖(n : ℝ)‖ := by + simpa using eventually_gt_atTop (0 : ℕ) + filter_upwards [hsmall'.eventuallyLT_norm_of_eventually_pos hpos] with n hn + have hn' : 2 ^ (2 ^ (a + c * s n)) + 1 < n := by + simpa only [Function.comp_apply, ← Nat.cast_add_one, Real.norm_natCast, Nat.cast_lt] using hn + exact (Nat.add_le_add_right (hbound (s n)) 1).trans_lt hn' + +/-- A halting machine whose space usage is `o(log log n)` has a uniform constant space bound. +The bound applies to the same machine on every input. -/ +theorem exists_const_space_of_isLittleO_log_log {k : ℕ} {Symbol State : Type*} + [Finite Symbol] [Finite State] {tm : MultiTapeTM k Symbol State} {s : ℕ → ℕ} + (hhalt : ∀ input, ∃ p : tm.ComputationPath input, p.last.Halted) + (hspace : ∀ input, tm.RunsInSpace input (s input.length)) + (hs : (fun n ↦ (s n : ℝ)) =o[atTop] (fun n ↦ Real.log (Real.log (n : ℝ)))) : + ∃ C : ℕ, ∀ input, tm.RunsInSpace input C := by + classical + let : Fintype Symbol := Fintype.ofFinite Symbol + let : Fintype State := Fintype.ofFinite State + obtain ⟨N, hN⟩ := Filter.eventually_atTop.mp + (eventually_visit_bound_lt (Symbol := Symbol) (State := State) k hs) + let R := (Finset.range N).sup s + have hhead : ∀ input (p : tm.ComputationPath input) i, + (p.last.storage.workTapePos i).natAbs ≤ R := by + intro input + induction input using (measure List.length).wf.induction with + | h input ih => + intro p i + by_cases hsmall : input.length < N + · have hw := MultiTapeNTM.RunPath.inWindow_of_space_le (p := p.toRunPath) + (fun i ↦ by simp [p.head_eq, Cfg.init]) (hspace input p) + exact (mem_window.mp (hw _ (RelSeries.last_mem _) i)).trans + (Finset.le_sup (Finset.mem_range.mpr hsmall)) + obtain ⟨q, hq⟩ := hhalt input + obtain ⟨input', hshort, p', hstore⟩ := tm.exists_shorter_input_storage + (hspace input) hq (hN input.length (by omega)) (p.last_mem_of_halted hq) + rw [← hstore] + exact ih input' hshort p' i + refine ⟨k * (2 * R + 1), fun input p ↦ MultiTapeNTM.RunPath.InWindow.space_le ?_⟩ + rintro c ⟨j, rfl⟩ i + exact mem_window.mpr (hhead input ⟨p.take j, by simpa using p.head_eq⟩ i) + +/-- A function computable in subloglog space is computable in constant space. -/ +theorem ComputableInSpace.exists_const_space {β : Type*} {f : List Bool → β} + {encOut : β ↪ List Bool} {s : ℕ → ℕ} + (h : ComputableInSpace f (.refl _) encOut (fun input ↦ s input.length)) + (hs : (fun n ↦ (s n : ℝ)) =o[atTop] (fun n ↦ Real.log (Real.log (n : ℝ)))) : + ∃ C : ℕ, ComputableInSpace f (.refl _) encOut (fun _ ↦ C) := by + obtain ⟨k, State, hfinite, tm, htm⟩ := h + let : Finite State := hfinite + have hhalt : ∀ input, ∃ p : tm.ComputationPath input, p.last.Halted := by + intro input + obtain ⟨t, ht, _⟩ := (htm input).1 + exact ⟨.ofDeterministic tm input t, ht⟩ + obtain ⟨C, hC⟩ := tm.exists_const_space_of_isLittleO_log_log hhalt (fun input ↦ (htm input).2) hs + exact ⟨C, k, State, hfinite, tm, fun input ↦ ⟨(htm input).1, hC input⟩⟩ + +/-- A language decidable in subloglog space is decidable in constant space. -/ +theorem DecidableInSpace.exists_const_space {L : Language Bool} {s : ℕ → ℕ} + (h : DecidableInSpace L (.refl _) (fun input ↦ s input.length)) + (hs : (fun n ↦ (s n : ℝ)) =o[atTop] (fun n ↦ Real.log (Real.log (n : ℝ)))) : + ∃ C : ℕ, DecidableInSpace L (.refl _) (fun _ ↦ C) := + ComputableInSpace.exists_const_space h hs + +/-- `SPACE(o(log log n)) = SPACE(1)` for binary languages. -/ +theorem loglogn_equals_no_space (L : Language Bool) : + (∃ s : ℕ → ℕ, + (fun n ↦ (s n : ℝ)) =o[atTop] (fun n ↦ Real.log (Real.log (n : ℝ))) ∧ + DecidableInSpace L (.refl _) (fun input ↦ s input.length)) ↔ + (∃ C : ℕ, DecidableInSpace L (.refl _) (fun _ ↦ C)) := by + constructor + · rintro ⟨s, hs, h⟩ + exact h.exists_const_space hs + · rintro ⟨C, h⟩ + refine ⟨fun _ ↦ C, ?_, h⟩ + exact Real.isLittleO_const_log_atTop.comp_tendsto + (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 447e62baa..d391260c6 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/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.step`, `Follows.runningStepHom`, `Follows.stepHom`: a configuration map that agrees with + the adapter maps steps to steps, so it is a homomorphism of step relations and maps run paths * `RunsInTime`: every computation path of at least the given length ends in a halted configuration @@ -141,6 +145,10 @@ lemma length_output_mono (p : ntm.RunPath input) : have : ntm.Step (p i.castSucc) (p i.succ) := p.step i grind [Step, Action.apply_output] +/-- Once halted, a run path stays halted. -/ +lemma halted_mono (p : ntm.RunPath input) : Monotone fun i ↦ (p i).Halted := + Fin.monotone_iff_le_succ.mpr fun i h ↦ (step_of_halt h).mp (p.step i) ▸ h + /-- Once a run path is halted, its configuration stays unchanged. -/ lemma last_eq_of_head_halted (p : ntm.RunPath input) (h : p.head.Halted) : p.last = p.head := by induction p using RelSeries.inductionOn' with @@ -173,20 +181,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 +204,90 @@ 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`: the symbols the inner machine reads, computed from those +under the heads of the outer machine, and the outer action performing each inner action. -/ +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. -/ +@[simps] +def Adapter.mapState {State' : Type*} (φ : Option State → Option State') : + Adapter k k Symbol State State' := + ⟨id, fun _ => Action.mapState φ⟩ + +/-- `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 a step.** If `ntm'` follows `ntm`, and the map `f` relabels the state of +`c` through `state`, reads through `adapter` what `c` reads, and carries the action of a step from +`c` to its adaptation, then `f` maps the step to a step of `ntm'`. -/ +lemma step (h : ntm'.Follows ntm state adapter) + (f : Cfg k Symbol State input → Cfg k' Symbol State' input') {c c' : Cfg k Symbol State input} + (hstep : ntm.Step c c') (hstate : c.state.map state = (f c).state) + (hread : adapter.read (f c).headSymbols = c.headSymbols) + (haction : ∀ action, action.apply c = c' → + (adapter.action (f c).headSymbols action).apply (f c) = f c') : + ntm'.Step (f c) (f c') := by + rcases hq : c.state with _ | q + · rw [(step_of_halt hq).mp hstep] + exact (step_of_halt (show (f c).state = none by rw [← hstate, hq]; rfl)).mpr rfl + · simp only [Step, hq, Option.map_some] at hstep hstate + obtain ⟨action, hTr, rfl⟩ := hstep + rw [Step, ← hstate] + exact ⟨_, h q _ action (by rwa [hread]), (haction action rfl).symm⟩ + +/-- **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') := + ⟨f, fun {c _} ⟨hrunning, hstep⟩ ↦ (Option.ne_none_iff_exists'.mp hrunning).elim fun q hq ↦ + h.step f hstep (by rw [hq, hstate c q hq]; rfl) (hread c) fun action h ↦ h ▸ haction c action⟩ + +/-- **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') := + ⟨f, fun hstep ↦ h.step f hstep (hstate _) (hread _) fun action h ↦ h ▸ haction _ action⟩ + +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]) + end MultiTapeNTM end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean index db56718d5..cefff3ef5 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean +++ b/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 -/ diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean index 9faac83bc..1793908d2 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean @@ -19,8 +19,8 @@ tape `j`. The remaining tapes are left unchanged. The configuration map `embed e cfg extraTapes extraPos` places `cfg` on the selected tapes and initialises the remaining tapes from `extraTapes` and `extraPos`. -The main lemmas show that one step and an entire run path of the larger machine mirror the -corresponding step and run path of `tm`. +The configuration map is a homomorphism of step relations (`embedHom`), so each run path of `tm` +maps to a run path of the larger machine. ## Main definitions @@ -34,7 +34,6 @@ corresponding step and run path of `tm`. ## Main results -* `Turing.MultiTapeTM.step_embed`: the one-step mirroring lemma. * `Turing.MultiTapeTM.space_map_embedHom_le`: the space bound for a mapped path. * `Turing.MultiTapeTM.oneTapeCfg`: the one-tape view of a configuration. * `Turing.MultiTapeTM.runFrom_tapeEmb`: the run of a one-tape machine placed on work tape `i`. @@ -64,14 +63,12 @@ public lemma partialInv_isPartialInv (e : Fin k ↪ Fin k') : moves. -/ @[expose] public noncomputable def extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : MultiTapeTM k' Symbol State := - ofTr tm.q₀ fun q inp work => - let a := tm.tr q inp fun j => work (e j) - { inputTape := a.inputTape - workTapes := fun l => match partialInv e l with - | some j => a.workTapes j - | none => (none, 0) - output := a.output - state := a.state } + tm.adapt + { read := fun heads => ⟨heads.inputSymbol, heads.workTapeSymbols ∘ e⟩ + action := fun _ a => + { a with workTapes := fun l => match partialInv e l with + | some j => a.workTapes j + | none => (none, 0) } } @[simp] public lemma extendTapes_q₀ (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : @@ -106,11 +103,6 @@ public lemma partialInv_eq_some (e : Fin k ↪ Fin k') {l : Fin k'} {j : Fin k} (h : partialInv e l = some j) : e j = l := (partialInv_isPartialInv e j l).mp h -@[simp] -public lemma embed_inputSymbol (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) - (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : - (embed e cfg extraTapes extraPos).inputSymbol = cfg.inputSymbol := rfl - @[simp] public lemma embed_workTapes_embed (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) : @@ -129,30 +121,18 @@ public lemma embed_workTapeSymbols_embed (e : Fin k ↪ Fin k') (cfg : Cfg k Sym (embed e cfg extraTapes extraPos).workTapeSymbols (e j) = cfg.workTapeSymbols j := by simp [Cfg.workTapeSymbols] -/-- Reindexing is a step-semiconjugation: the reindexed machine acts on the embedded tapes exactly -as `tm` does, and never touches the extra tapes. -/ -public lemma step_embed (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') - (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : - Function.Semiconj (embed (input := input) e · extraTapes extraPos) tm.step - (tm.extendTapes e).step := by - intro cfg - symm - cases hq : cfg.state with - | none => simp [embed, hq] - | some q => - rw [step_of_state (cfg := embed e cfg extraTapes extraPos) hq, step_of_state hq] - simp only [extendTapes, tr_ofTr, embed_inputSymbol, embed_workTapeSymbols_embed] - refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> simp only [Action.apply, embed] <;> - cases partialInv e l <;> simp - /-- `embed` as a homomorphism of step relations: each step `c → c'` of `tm` becomes the step `embed c → embed c'` of the reindexed machine, so a run path of `tm` maps to a run path of the -reindexed machine, with the extra tapes held fixed. `stepHom` builds it from `step_embed`, which -says that `embed` commutes with the step functions. -/ +reindexed machine, with the extra tapes held fixed. `Follows.stepHom` builds it, since `embed` +agrees with the adapter defining `extendTapes`. -/ @[expose, simps! apply] public noncomputable def embedHom (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (tm.stepRel input).Hom ((tm.extendTapes e).stepRel input) := - stepHom (embed e · extraTapes extraPos) (step_embed tm e extraTapes extraPos) + follows_adapt.stepHom (embed e · extraTapes extraPos) (fun _ => Option.map_id_apply) + (fun c => HeadSymbols.ext rfl (funext (embed_workTapeSymbols_embed e c extraTapes extraPos))) + fun c a => by + refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> simp only [Action.apply, embed] <;> + cases partialInv e l <;> simp section Space @@ -243,12 +223,10 @@ public theorem TransformsTapes.tapeEmb {tm : MultiTapeTM 1 Symbol State} (fun _ => 0) = wordsCfg input q (Function.update ws i (v 0)) o := by rw [embed_tapeEmb] refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> by_cases hl : l = i <;> simp [hl, wordsCfg] - refine ⟨Function.update ws i (v 0), emitted, ⟨v, hQ, rfl⟩, - p.map (embedHom tm (MultiTapeTM.tapeEmb i) (fun l => tapeOfList (ws l)) (fun _ => 0)), - ?_, ?_, htime, (space_map_embedHom_le ..).trans (Nat.add_le_add_right hspace _)⟩ - · simp only [RelSeries.head_map, hhead, embedHom_apply, hplace, Function.update_eq_self] - rfl - · simp only [RelSeries.last_map, hlast, embedHom_apply, hplace] + exact ⟨Function.update ws i (v 0), emitted, ⟨v, hQ, rfl⟩, + p.map (embedHom tm (MultiTapeTM.tapeEmb i) (fun l => tapeOfList (ws l)) fun _ => 0), + by simp [hhead, hplace], by simp [hlast, hplace], htime, + (space_map_embedHom_le ..).trans (Nat.add_le_add_right hspace _)⟩ end OneTape diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean index 9c9497046..c59bd0e0b 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean @@ -26,8 +26,8 @@ reading the flag. Reading blank on both the virtual input tape and the flag tape boundary. The configuration map `inCfg` places the simulated input on the virtual input tape, places the -marker on the flag tape, and leaves the real input tape unused. The main lemmas show that one step -and an entire run path of the redirected machine mirror the corresponding step and run path of `tm`. +marker on the flag tape, and leaves the real input tape unused. It is a homomorphism of step +relations (`inCfgHom`), so each run path of `tm` maps to a run path of the redirected machine. -/ namespace Turing.MultiTapeTM @@ -50,12 +50,15 @@ are. -/ moved. -/ @[expose] public noncomputable def inputFromTape (tm : MultiTapeTM k Symbol State) : MultiTapeTM (k + 2) Symbol State := - ofTr tm.q₀ fun q _ work => - let a := tm.tr q (work (Fin.natAdd k 0)) fun j => work (j.castAdd 2) - let m := clampMove (work (Fin.natAdd k 0)) (work (Fin.natAdd k 1)) a.inputTape - { a with - inputTape := 0 - workTapes := Fin.append a.workTapes fun _ => (none, m) } + tm.adapt + { read := fun heads => + ⟨heads.workTapeSymbols (Fin.natAdd k 0), heads.workTapeSymbols ∘ Fin.castAdd 2⟩ + action := fun heads a => + let m := clampMove (heads.workTapeSymbols (Fin.natAdd k 0)) + (heads.workTapeSymbols (Fin.natAdd k 1)) a.inputTape + { a with + inputTape := 0 + workTapes := Fin.append a.workTapes fun _ => (none, m) } } /-- A configuration of `tm` on `input`, as the redirecting machine sees it, over an arbitrary ambient input: `input` sits on the virtual input tape with the head at cell `inputPos - 1`, the flag @@ -153,28 +156,19 @@ public lemma val_moveInputPos_sub_one_eq_clampMove (mark : Symbol) (c : Cfg k Sy rw [inputSymbolInner (c.inputPos.val - 1) (by omega) (by omega)] rcases m with _ | _ | _ <;> simp only [clampMove, SignType.cast] <;> omega -/-- **The redirection is a step-semiconjugation.** One step of the machine reading its input from -the virtual tape mirrors one step of the original, under the embedding `inCfg`. -/ -public lemma step_inCfg (tm : MultiTapeTM k Symbol State) (mark : Symbol) - (outerInput : List Symbol) : - Function.Semiconj (inCfg (input := input) mark · outerInput) tm.step tm.inputFromTape.step := by - intro c - symm - cases hq : c.state with - | none => simp [inCfg, hq] - | some q => - rw [step_of_state (cfg := inCfg mark c outerInput) hq, step_of_state hq] - simp only [inputFromTape, tr_ofTr, inCfg_workTapeSymbols_vip, inCfg_workTapeSymbols_flag, - inCfg_workTapeSymbols_castAdd] - refine Cfg.ext rfl (by simp [inCfg]) ?_ ?_ rfl <;> funext l <;> - induction l using Fin.addCases <;> simp [inCfg, val_moveInputPos_sub_one_eq_clampMove mark] - /-- The redirection preserves steps, so it maps run paths of `tm` to run paths of the redirected machine. -/ @[expose, simps! apply] public noncomputable def inCfgHom (tm : MultiTapeTM k Symbol State) (mark : Symbol) (outerInput : List Symbol) : (tm.stepRel input).Hom (tm.inputFromTape.stepRel outerInput) := - stepHom (inCfg mark · outerInput) (step_inCfg tm mark outerInput) + follows_adapt.stepHom (inCfg mark · outerInput) (fun _ => Option.map_id_apply) + (fun c => HeadSymbols.ext (inCfg_workTapeSymbols_vip c) + (funext (inCfg_workTapeSymbols_castAdd c))) fun c a => by + simp only [Cfg.headSymbols_workTapeSymbols, inCfg_workTapeSymbols_vip, + inCfg_workTapeSymbols_flag] + refine Cfg.ext rfl (by simp [inCfg]) ?_ ?_ rfl <;> funext l <;> + induction l using Fin.addCases <;> + simp [inCfg, Action.apply, val_moveInputPos_sub_one_eq_clampMove mark] /-- **Space of the input-redirected path.** The `k` inner tapes visit exactly what the original path visits; the two extra tapes (virtual input, flag) each move only with the simulated input diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean index 6fbf45675..e06c5bbf7 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean @@ -18,8 +18,8 @@ frontier. Since the output is append-only, the frontier position is a *function of the configuration* — the length of the output so far — so the redirected machine mirrors the original through the -configuration map `outCfg`. The main lemmas show that one step and an entire run path of the -redirected machine mirror the corresponding step and run path of `tm`. +configuration map `outCfg`, a homomorphism of step relations (`outCfgHom`), so each run path of `tm` +maps to a run path of the redirected machine. -/ namespace Turing.MultiTapeTM @@ -30,16 +30,16 @@ variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} at the write frontier. -/ @[expose] public noncomputable def outputToTape (tm : MultiTapeTM k Symbol State) : MultiTapeTM (k + 1) Symbol State := - ofTr tm.q₀ fun q inp work => - let a := tm.tr q inp fun j => work j.castSucc - { inputTape := a.inputTape - workTapes := Fin.lastCases - (match a.output with - | none => (none, 0) - | some s => (some (some s), 1)) - (fun j => a.workTapes j) - output := none - state := a.state } + tm.adapt + { read := fun heads => ⟨heads.inputSymbol, heads.workTapeSymbols ∘ Fin.castSucc⟩ + action := fun _ a => + { a with + workTapes := Fin.lastCases + (match a.output with + | none => (none, 0) + | some s => (some (some s), 1)) + a.workTapes + output := none } } /-- A configuration of `tm`, as the redirected machine sees it: the output so far sits on the last work tape with the head at its end, and the real output is empty. -/ @@ -50,10 +50,6 @@ last work tape with the head at its end, and the real output is empty. -/ Fin.lastCases (c.output.length : ℤ) (fun j => c.workTapePos j), []⟩ -@[simp] -public lemma outCfg_inputSymbol (c : Cfg k Symbol State input) : - (outCfg c).inputSymbol = c.inputSymbol := rfl - @[simp] public lemma outCfg_workTapes_last (c : Cfg k Symbol State input) : (outCfg c).workTapes (Fin.last k) = tapeOfList c.output := by @@ -79,27 +75,14 @@ public lemma outCfg_workTapeSymbols_castSucc (c : Cfg k Symbol State input) (j : (outCfg c).workTapeSymbols j.castSucc = c.workTapeSymbols j := by simp [Cfg.workTapeSymbols] -/-- The redirection is a step-semiconjugation. -/ -public lemma step_outCfg (tm : MultiTapeTM k Symbol State) : - Function.Semiconj (outCfg (input := input)) tm.step tm.outputToTape.step := by - intro c - symm - cases hq : c.state with - | none => simp [outCfg, hq] - | some q => - rw [step_of_state (cfg := outCfg c) hq, step_of_state hq] - simp only [outputToTape, tr_ofTr, outCfg_inputSymbol, outCfg_workTapeSymbols_castSucc] - refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> induction l using Fin.lastCases with - | cast j => simp - | last => - cases h : (tm.tr q c.inputSymbol c.workTapeSymbols).output <;> - simp [h, tapeOfList_append_single, SignType.cast] - /-- The redirection preserves steps, so it maps run paths of `tm` to run paths of the redirected machine. -/ @[expose, simps! apply] public noncomputable def outCfgHom (tm : MultiTapeTM k Symbol State) : (tm.stepRel input).Hom (tm.outputToTape.stepRel input) := - stepHom outCfg (step_outCfg tm) + follows_adapt.stepHom outCfg (fun _ => Option.map_id_apply) + (fun c => HeadSymbols.ext rfl (funext (outCfg_workTapeSymbols_castSucc c))) fun c a => by + refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> induction l using Fin.lastCases <;> + cases h : a.output <;> simp [h, Action.apply, tapeOfList_append_single, SignType.cast] /-- The initial configuration of the redirected machine is the original's through `outCfg`. -/ public lemma initCfg_outputToTape (tm : MultiTapeTM k Symbol State) (input : List Symbol) : diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean index a6408af81..7dac60993 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean @@ -40,15 +40,17 @@ public instance [Finite State] : Finite (RepeatUntilBlankState State) := Finite.of_injective (fun q => match q with | .run q => some q | .check => none) fun q q' h => by cases q <;> cases q' <;> simp_all +/-- The state of the loop while `tm` runs: halting goes to `check`. -/ +def RepeatUntilBlank.runState (state : Option State) : Option (RepeatUntilBlankState State) := + some (state.elim .check .run) + /-- `tm`, with its halting transitions sent to the state `check`. From `check`, the machine halts if the cell under the head of tape `i` is blank and otherwise restarts `tm`, moving no head. -/ public noncomputable def repeatUntilBlank (i : Fin k) (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol (RepeatUntilBlankState State) := ofTr (.run tm.q₀) fun q inp work => match q with - | .run q => - let a := tm.tr q inp work - { a with state := some (a.state.elim .check .run) } + | .run q => (tm.tr q inp work).mapState RepeatUntilBlank.runState | .check => { inputTape := 0, workTapes := fun _ => (none, 0), output := none, state := (work i).map fun _ => .run tm.q₀ } @@ -57,37 +59,17 @@ namespace RepeatUntilBlank variable {i : Fin k} {tm : MultiTapeTM k Symbol State} -/-- A configuration of `tm` as a configuration of `repeatUntilBlank i tm`: a live state `q` becomes -`run q` and the halted state becomes `check`. -/ -def runCfg (cfg : Cfg k Symbol State input) : - Cfg k Symbol (RepeatUntilBlankState State) input := - cfg.mapState (fun st => some (st.elim .check .run)) - -@[simp] -lemma workTapePos_runCfg (cfg : Cfg k Symbol State input) : - (runCfg cfg).workTapePos = cfg.workTapePos := rfl - -@[simp] -lemma runCfg_wordsCfg_some (q : State) (ws : Fin k → List Symbol) (out : List Symbol) : - runCfg (input := input) (wordsCfg input (some q) ws out) = - wordsCfg input (some (.run q)) ws out := rfl - -@[simp] -lemma runCfg_wordsCfg_none (ws : Fin k → List Symbol) (out : List Symbol) : - runCfg (State := State) (input := input) (wordsCfg input none ws out) = - wordsCfg input (some .check) ws out := rfl - -lemma q₀_repeatUntilBlank : (repeatUntilBlank i tm).q₀ = .run tm.q₀ := rfl - -/-- On `tm`'s live configurations, the looping machine mirrors `tm` step for step. -/ -lemma step_runCfg (cfg : Cfg k Symbol State input) (h : ¬ cfg.Halted) : - (repeatUntilBlank i tm).step (runCfg cfg) = runCfg (tm.step cfg) := by - obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp h - have hstate : (runCfg cfg).state = some (RepeatUntilBlankState.run q) := by - simp [runCfg, Cfg.mapState, hq] - rw [step_of_state hstate, step_of_state hq] - simp only [repeatUntilBlank, tr_ofTr] - rfl +/-- While `tm` runs, the loop follows it, with halting going to `check`. -/ +lemma follows_run : (repeatUntilBlank i tm).Follows tm .run (.mapState runState) := + fun _ _ _ h => tr_iff.mp h ▸ rfl + +/-- A configuration of `tm` as one of `repeatUntilBlank i tm`, a live state `q` becoming `run q` and +the halted state `check`: the loop mirrors the running steps of `tm`. -/ +@[simps! apply] +noncomputable def runHom (i : Fin k) : + (tm.runningStepRel input).Hom ((repeatUntilBlank i tm).stepRel input) := + follows_run.runningStepHom (Cfg.mapState runState) + (fun _ _ => congrArg runState) (fun _ => rfl) fun _ _ => rfl /-- From `check` on a `wordsCfg` configuration, the machine halts if the word on tape `i` is empty and otherwise restarts `tm`, leaving the words unchanged. -/ @@ -114,11 +96,10 @@ lemma exists_round {P : (input : List Symbol) → (Fin k → List Symbol) → Pr p.length ≤ t + 1 ∧ p.InWindow s := by obtain ⟨w', e, hQ, p, hhead, hlast, htime, hspace⟩ := h input w out hP obtain ⟨q, hqhead, hqlast, hqlen, hqmem⟩ := p.exists_running (by rw [hlast]; rfl) - let f := runningStepHom (tm' := repeatUntilBlank i tm) (input := input) runCfg step_runCfg - have hcheck : (repeatUntilBlank i tm).Step (q.map f).last + have hcheck : (repeatUntilBlank i tm).Step (q.map (runHom i)).last (wordsCfg input (if w' i = [] then none else some (.run tm.q₀)) w' (out ++ e)) := by - simp [f, hqlast, hlast, step_check] - refine ⟨w', e, hQ, (q.map f).snoc _ hcheck, by simp [f, hqhead, hhead], by simp, + simp [hqlast, hlast, runState, step_check] + refine ⟨w', e, hQ, (q.map (runHom i)).snoc _ hcheck, by simp [hqhead, hhead, runState], by simp, by simp [MultiTapeNTM.RunPath.time] at htime ⊢; lia, ?_⟩ -- the heads of `tm` stay within `[-s, s]`, and reading tape `i` moves none of them have hwin := MultiTapeNTM.RunPath.inWindow_of_space_le (p := p) (by simp [hhead]) hspace @@ -149,7 +130,7 @@ public theorem transformsTapes_repeatUntilBlank (i : Fin k) {tm : MultiTapeTM k (fun input _ ws' emitted => R input ws' emitted) ((rounds + 1) * (t + 1)) (2 * k * s + k) := by intro input ws out hP0 - rw [q₀_repeatUntilBlank] + rw [show (repeatUntilBlank i tm).q₀ = .run tm.q₀ from rfl] set start := wordsCfg (State := RepeatUntilBlankState State) input (some (.run tm.q₀)) ws out with hstart -- after `n ≤ rounds` rounds, the loop has a run path of at most `n * (t + 1)` steps within @@ -161,10 +142,8 @@ public theorem transformsTapes_repeatUntilBlank (i : Fin k) {tm : MultiTapeTM k intro n hn induction n with | zero => - refine ⟨.singleton _ start, ws, [], rfl, by simp [hstart], by simp, ?_, hP0⟩ - rintro _ ⟨_, rfl⟩ l - change start.workTapePos l ∈ _ - simp [hstart, mem_window] + exact ⟨.singleton _ start, ws, [], rfl, by simp [hstart], by simp, + fun _ ⟨_, h⟩ _ => h ▸ by simp [RelSeries.singleton, hstart, mem_window], hP0⟩ | succ n ih => obtain ⟨p, wsn, acc, hhead, hlast, hlen, hwin, hPn⟩ := ih (by lia) obtain ⟨wsn', e, hQ, q, hqhead, hqlast, hqlen, hqwin⟩ := diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean index 80ce75b66..dea0a89ab 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean @@ -24,8 +24,8 @@ second. ## Main results * `Turing.MultiTapeTM.seq`: the composed machine. -* `Turing.MultiTapeTM.exists_runPath_seq`: run paths compose, and the configurations of the - composed path are those of the two paths up to their states. +* `Turing.MultiTapeTM.exists_runPath_seq`: run paths compose, and the composed path visits only + cells that the two paths visit. * `Turing.MultiTapeTM.transformsTapes_seq`: transformations compose, bounds adding. -/ @@ -35,6 +35,12 @@ namespace Turing.MultiTapeTM variable {k : ℕ} {Symbol State₀ State₁ : Type*} {input : List Symbol} +/-- The state of the sequential composition while `tm₀` runs: halting hands over to `tm₁` in its +initial state. -/ +def Sequential.leftState (tm₁ : MultiTapeTM k Symbol State₁) (state : Option State₀) : + Option (State₀ ⊕ State₁) := + some (state.elim (.inr tm₁.q₀) .inl) + /-- The sequential composition of `tm₀` and `tm₁`: it behaves like `tm₀` until `tm₀` would halt, at which point it switches to the initial state of `tm₁` and behaves like `tm₁`. The switch is folded into the halting transition of `tm₀`, so it costs no step. -/ @@ -42,12 +48,8 @@ noncomputable def seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTape MultiTapeTM k Symbol (State₀ ⊕ State₁) := ofTr (.inl tm₀.q₀) fun q inp work => match q with - | .inl q₀ => - let a := tm₀.tr q₀ inp work - { a with state := some (a.state.elim (.inr tm₁.q₀) .inl) } - | .inr q₁ => - let a := tm₁.tr q₁ inp work - { a with state := a.state.map .inr } + | .inl q₀ => (tm₀.tr q₀ inp work).mapState (Sequential.leftState tm₁) + | .inr q₁ => (tm₁.tr q₁ inp work).mapState (Option.map .inr) variable {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} @@ -58,7 +60,7 @@ the initial state of the second phase. Under this map, the whole first phase of run of `tm₀`, *including* its halting step. -/ def leftCfg (tm₁ : MultiTapeTM k Symbol State₁) (cfg : Cfg k Symbol State₀ input) : Cfg k Symbol (State₀ ⊕ State₁) input := - cfg.mapState (fun st => some (st.elim (.inr tm₁.q₀) .inl)) + cfg.mapState (leftState tm₁) /-- A configuration of the second phase. Under this map, the second phase of `seq` mirrors the run of `tm₁`. -/ @@ -66,66 +68,51 @@ def rightCfg (cfg : Cfg k Symbol State₁ input) : Cfg k Symbol (State₀ ⊕ State₁) input := cfg.mapState (Option.map .inr) -lemma step_leftCfg (cfg : Cfg k Symbol State₀ input) (h : cfg.state ≠ none) : - (tm₀.seq tm₁).step (leftCfg tm₁ cfg) = leftCfg tm₁ (tm₀.step cfg) := by - obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp h - have h1 : (leftCfg tm₁ cfg).state = some (Sum.inl q : State₀ ⊕ State₁) := by - simp [leftCfg, Cfg.mapState, hq] - rw [step_of_state h1, step_of_state hq] - simp only [seq, tr_ofTr] - rfl - -lemma step_rightCfg (cfg : Cfg k Symbol State₁ input) : - (tm₀.seq tm₁).step (rightCfg cfg) = rightCfg (tm₁.step cfg) := by - cases hq : cfg.state with - | none => - have h1 : (rightCfg (State₀ := State₀) cfg).state = none := by simp [rightCfg, Cfg.mapState, hq] - rw [step_of_halt h1, step_of_halt hq] - | some q => - have h1 : (rightCfg (State₀ := State₀) cfg).state = some (Sum.inr q : State₀ ⊕ State₁) := by - simp [rightCfg, hq] - rw [step_of_state h1, step_of_state hq] - simp only [seq, tr_ofTr] - rfl - -@[simp] -lemma forgetState_leftCfg (cfg : Cfg k Symbol State₀ input) : - (leftCfg tm₁ cfg).forgetState = cfg.forgetState := rfl - -@[simp] -lemma forgetState_rightCfg (cfg : Cfg k Symbol State₁ input) : - (rightCfg (State₀ := State₀) cfg).forgetState = cfg.forgetState := rfl +/-- In its first phase, `seq tm₀ tm₁` follows `tm₀`, with halting handing over to `tm₁`. -/ +lemma follows_left : (tm₀.seq tm₁).Follows tm₀ .inl (.mapState (leftState tm₁)) := + fun _ _ _ h => tr_iff.mp h ▸ rfl + +/-- In its second phase, `seq tm₀ tm₁` follows `tm₁`. -/ +lemma follows_right : (tm₀.seq tm₁).Follows tm₁ .inr (.mapState (Option.map .inr)) := + fun _ _ _ h => tr_iff.mp h ▸ rfl + +/-- The first phase of `seq tm₀ tm₁` mirrors the running steps of `tm₀`. -/ +@[simps! apply] +noncomputable def leftCfgHom : (tm₀.runningStepRel input).Hom ((tm₀.seq tm₁).stepRel input) := + follows_left.runningStepHom (leftCfg tm₁) + (fun _ _ => congrArg (leftState tm₁)) (fun _ => rfl) fun _ _ => rfl + +/-- The second phase of `seq tm₀ tm₁` mirrors the steps of `tm₁`. -/ +@[simps! apply] +noncomputable def rightCfgHom : (tm₁.stepRel input).Hom ((tm₀.seq tm₁).stepRel input) := + follows_right.stepHom rightCfg (fun _ => rfl) (fun _ => rfl) fun _ _ => rfl /-- A halted configuration of the first phase is the start of the second phase. -/ lemma leftCfg_of_halt {cfg : Cfg k Symbol State₀ input} (h : cfg.state = none) : leftCfg tm₁ cfg = rightCfg (cfg.withState (some tm₁.q₀)) := by - simp [leftCfg, rightCfg, Cfg.withState, Cfg.mapState, h] + simp [leftCfg, leftState, rightCfg, Cfg.withState, Cfg.mapState, h] end Sequential open Sequential in /-- **Sequential composition of runs.** A run path of `tm₀` to a halted configuration, followed by a -run path of `tm₁` to a halted configuration started where `tm₀` halted, gives a run path of `seq` -of at most as many steps, whose configurations are those of the two paths up to their states. -/ +run path of `tm₁` started where `tm₀` halted, gives a run path of `seq` of at most as many steps, +which visits only cells that the two paths visit. -/ theorem exists_runPath_seq {p₀ : tm₀.RunPath input} (h₀ : p₀.last.Halted) - {p₁ : tm₁.RunPath input} (h₁ : p₁.head = p₀.last.withState (some tm₁.q₀)) - (hp₁ : p₁.last.Halted) : + {p₁ : tm₁.RunPath input} (h₁ : p₁.head = p₀.last.withState (some tm₁.q₀)) : ∃ p : (tm₀.seq tm₁).RunPath input, p.head = leftCfg tm₁ p₀.head ∧ p.last = rightCfg p₁.last ∧ p.length ≤ p₀.length + p₁.length ∧ - ∀ c ∈ p, (∃ c₀ ∈ p₀, c.forgetState = c₀.forgetState) ∨ - ∃ c₁ ∈ p₁, c.forgetState = c₁.forgetState := by - -- `seq` takes the running steps of `tm₀`, then those of `tm₁` + ∀ i, p.visitedByTapeHead i ⊆ p₀.visitedByTapeHead i ∪ p₁.visitedByTapeHead i := by + -- `seq` takes the running steps of `tm₀`, then the steps of `tm₁` obtain ⟨q₀, hh₀, hl₀, hlen₀, hmem₀⟩ := p₀.exists_running h₀ - obtain ⟨q₁, hh₁, hl₁, hlen₁, hmem₁⟩ := p₁.exists_running hp₁ - let f₀ := runningStepHom (tm' := tm₀.seq tm₁) (input := input) (leftCfg tm₁) step_leftCfg - let f₁ := runningStepHom (tm' := tm₀.seq tm₁) (input := input) rightCfg - fun c _ => step_rightCfg c - refine ⟨(q₀.map f₀).smash (q₁.map f₁) (by simp [f₀, f₁, hl₀, hh₁, h₁, leftCfg_of_halt h₀]), - by simp [f₀, hh₀], by simp [f₁, hl₁], by simp; lia, fun c hc => ?_⟩ + refine ⟨(q₀.map leftCfgHom).smash (p₁.map rightCfgHom) + (by simp [hl₀, h₁, leftCfg_of_halt h₀]), by simp [hh₀], by simp, by simp; lia, + fun i z hz => ?_⟩ + obtain ⟨c, hc, rfl⟩ := (MultiTapeNTM.RunPath.mem_visitedByTapeHead _).mp hz rcases RelSeries.mem_or_mem_of_mem_smash hc with hc | hc <;> obtain ⟨c', hc', rfl⟩ := RelSeries.exists_of_mem_map hc - · exact .inl ⟨c', hmem₀ c' hc', rfl⟩ - · exact .inr ⟨c', hmem₁ c' hc', rfl⟩ + · exact Finset.mem_union_left _ (p₀.mem_visitedByTapeHead.mpr ⟨c', hmem₀ c' hc', rfl⟩) + · exact Finset.mem_union_right _ (p₁.mem_visitedByTapeHead.mpr ⟨c', hc', rfl⟩) open Sequential in /-- **Sequential composition of transformations.** If the postcondition of the first @@ -147,18 +134,12 @@ theorem transformsTapes_seq obtain ⟨ws', e₀, hQ₀, p₀, hh₀, hl₀, ht₀, hs₀⟩ := h₀ input ws out hP₀ obtain ⟨ws'', e₁, hQ₁, p₁, hh₁, hl₁, ht₁, hs₁⟩ := h₁ input ws' (out ++ e₀) (hmid input ws ws' e₀ hP₀ hQ₀) - obtain ⟨p, hh, hl, ht, hmem⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁) (by rw [hl₀]; rfl) - (by simp [hh₁, hl₀]) (by rw [hl₁]; rfl) - refine ⟨ws'', e₀ ++ e₁, ⟨ws', e₀, e₁, hQ₀, hQ₁, rfl⟩, p, by simp [hh, hh₀, leftCfg]; rfl, - by simp [hl, hl₁, rightCfg], ht.trans (Nat.add_le_add ht₀ ht₁), ?_⟩ - -- every head position of the composed run is one of the first path or one of the second - refine (p.space_le_sum_card - (S := fun i => p₀.visitedByTapeHead i ∪ p₁.visitedByTapeHead i) fun c hc i => ?_).trans - (((Finset.sum_le_sum fun i _ => Finset.card_union_le _ _).trans_eq - Finset.sum_add_distrib).trans (Nat.add_le_add hs₀ hs₁)) - rcases hmem c hc with ⟨_, ⟨n, rfl⟩, he⟩ | ⟨_, ⟨n, rfl⟩, he⟩ <;> - rw [show c.workTapePos i = _ from congrArg (·.workTapePos i) he] - · exact Finset.mem_union_left _ (Finset.mem_image_of_mem _ (Finset.mem_univ n)) - · exact Finset.mem_union_right _ (Finset.mem_image_of_mem _ (Finset.mem_univ n)) + obtain ⟨p, hh, hl, ht, hvisited⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁) + (by rw [hl₀]; rfl) (by simp [hh₁, hl₀]) + -- the composed run visits only cells that one of the two runs visits + exact ⟨ws'', e₀ ++ e₁, ⟨ws', e₀, e₁, hQ₀, hQ₁, rfl⟩, p, by simp [hh, hh₀, leftCfg]; rfl, + by simp [hl, hl₁, rightCfg], ht.trans (Nat.add_le_add ht₀ ht₁), + ((Finset.sum_le_sum fun i _ => (Finset.card_le_card (hvisited i)).trans + (Finset.card_union_le _ _)).trans_eq Finset.sum_add_distrib).trans (Nat.add_le_add hs₀ hs₁)⟩ end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index d38e77461..71fa50417 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -13,9 +13,10 @@ public import Mathlib.Order.Lattice.Nat /-! # Head movement along run paths -This file collects how a step moves the work-tape heads and changes the work tapes, and what this -implies for the cells visited along a run path: a head moves by at most one cell per step, so it -visits every cell between its first and last positions, and a cell changes only under its head. +This file collects how a step moves the input and work-tape heads and changes the work tapes, and +what this implies for the cells visited along a run path: a head moves by at most one cell per +step, so it visits every cell between its first and last positions, and a cell changes only under +its head. -/ @@ -45,8 +46,32 @@ lemma Step.workTapes_eq_of_ne {c c' : Cfg k Symbol State input} (h : ntm.Step c rw [Action.apply_workTapes] cases ha : (a.workTapes i).1 <;> simp [ha, hz] +/-- The input head moves by at most one cell in a single step. -/ +lemma Step.inputPos_le {c c' : Cfg k Symbol State input} (h : ntm.Step c c') : + |(c'.inputPos.val : ℤ) - c.inputPos.val| ≤ 1 := by + unfold Step at h + split at h + · simp [h] + · obtain ⟨a, _, rfl⟩ := h + have := val_moveInputPos_eq c.inputPos a.inputTape + rcases ha : a.inputTape <;> grind [SignType.cast, Action.apply_inputPos] + namespace RunPath +/-- A path that avoids `pos` before its last configuration stays on the side of its head. -/ +lemma inputPos_side (p : ntm.RunPath input) {pos : ℕ} + (hne : ∀ i : Fin p.length, (p i.castSucc).inputPos.val ≠ pos) + {c : Cfg k Symbol State input} (hc : c ∈ p) : + (p.head.inputPos.val ≤ pos → c.inputPos.val ≤ pos) ∧ + (pos ≤ p.head.inputPos.val → pos ≤ c.inputPos.val) := by + obtain ⟨i, rfl⟩ := hc + induction i using Fin.induction with + | zero => exact ⟨id, id⟩ + | succ i ih => + have := abs_le.mp (Step.inputPos_le (p.step i)) + have := hne i + omega + /-- Every position between the first and the last position of a head along a path is visited, since the head moves by at most one cell per step. -/ lemma uIcc_workTapePos_subset_visitedByTapeHead (p : ntm.RunPath input) (i : Fin k) : diff --git a/Cslib/Foundations/Analysis/Asymptotics.lean b/Cslib/Foundations/Analysis/Asymptotics.lean new file mode 100644 index 000000000..ed8f5fc35 --- /dev/null +++ b/Cslib/Foundations/Analysis/Asymptotics.lean @@ -0,0 +1,38 @@ +/- +Copyright (c) 2026 Aviv Bar Natan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aviv Bar Natan +-/ + +module + +public import Cslib.Init +public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent +public import Mathlib.Analysis.SpecialFunctions.Log.Basic + +/-! +# Asymptotic bounds for exponentials + +A natural exponent negligible compared with `log g` gives a power negligible compared with `g`. +This can be applied repeatedly to bound iterated exponentials. +-/ + +@[expose] public section + +open Filter Asymptotics + +/-- If `f = o(log g)` and `g` tends to infinity, then `b ^ f = o(g)` for a fixed positive base. -/ +lemma Asymptotics.IsLittleO.natCast_const_pow {α : Type*} {l : Filter α} + {f : α → ℕ} {g : α → ℝ} + (h : (fun x ↦ (f x : ℝ)) =o[l] (fun x ↦ Real.log (g x))) + (hg : Tendsto g l atTop) {b : ℕ} (hb : 0 < b) : + (fun x ↦ ((b ^ f x : ℕ) : ℝ)) =o[l] g := by + have hb' : (0 : ℝ) < b := by exact_mod_cast hb + have hexp : (fun x ↦ Real.exp (Real.log b * (f x : ℝ))) =o[l] + (fun x ↦ Real.exp (Real.log (g x))) := by + rw [Real.isLittleO_exp_comp_exp_comp] + exact (IsEquivalent.refl.sub_isLittleO (h.const_mul_left (Real.log b))).symm.tendsto_atTop + (Real.tendsto_log_atTop.comp hg) + exact hexp.congr' + (Eventually.of_forall fun x ↦ by simp [mul_comm, Real.exp_nat_mul, Real.exp_log hb']) + ((hg.eventually_gt_atTop 0).mono fun x hx => Real.exp_log hx) diff --git a/references.bib b/references.bib index 5a8a1b452..8cda23690 100644 --- a/references.bib +++ b/references.bib @@ -288,6 +288,14 @@ @book{Holcombe1982 isbn={0-521-60492-3} } +@misc{Katz2007, + author = {Jonathan Katz}, + title = {Notes on Complexity Theory, Lecture 5}, + year = {2007}, + month = sep, + url = {https://www.cs.umd.edu/~jkatz/complexity/f05/lower_bounds.pdf} +} + @book{ KatzLindell2020, author = {Jonathan Katz and Yehuda Lindell},