feat(MultiTapeTM): loglogn_equals_no_space

Cslib.lean

@@ -68,6 +68,8 @@ 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.DeterministicToNondeterministic
+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.Sequential
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes
@@ -92,6 +94,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

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

@@ -244,6 +244,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.
@@ -273,13 +300,70 @@ lemma core_step_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input} (h : c₁.c
   simp only [Cfg.core, Cfg.storage, MultiTapeTM.step, hstate, hsym, hws]
   cases c₂.state <;> simp [hpos, hstate, hwt, hwp]
 
+namespace MultiTapeTM
+
+/-- Equal storages and scanned input symbols give equal next storages, and both input heads
+execute the same move. For halted configurations, this is the stationary move. -/
+lemma exists_step_move_of_storage_eq {input' : List Symbol}
+    {c : Cfg k Symbol State input} {c' : Cfg k Symbol State input'}
+    (hstore : c.storage = c'.storage) (hsym : c.inputSymbol = c'.inputSymbol) :
+    ∃ m, (tm.step c).storage = (tm.step c').storage ∧
+      (tm.step c).inputPos = moveInputPos c.inputPos m ∧
+      (tm.step c').inputPos = moveInputPos c'.inputPos m := by
+  rcases c with ⟨state, pos, tapes, heads, out⟩
+  rcases c' with ⟨state', pos', tapes', heads', out'⟩
+  simp only [Cfg.storage, Storage.mk.injEq] at hstore
+  rcases hstore with ⟨rfl, rfl, rfl⟩
+  cases state with
+  | none => exact ⟨0, rfl, (moveInputPos_zero _).symm, (moveInputPos_zero _).symm⟩
+  | some state =>
+    dsimp only [step]
+    unfold Cfg.workTapeSymbols
+    rw [hsym]
+    exact ⟨_, rfl, rfl, rfl⟩
+
+/-- Runs starting with the same core keep the same core. -/
+lemma core_runFrom_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input}
+    (h : c₁.core = c₂.core) (t : ℕ) :
+    (tm.runFrom c₁ t).core = (tm.runFrom c₂ t).core := by
+  induction t with
+  | zero => exact h
+  | succ t ih =>
+    simpa only [runFrom_succ_eq_step'] using core_step_eq_of_core_eq (tm := tm) ih
+
+/-- The cores up to and including the first halt are pairwise distinct. -/
+lemma core_runFrom_injOn {cfg : Cfg k Symbol State input} {T : ℕ}
+    (hhalt : (tm.runFrom cfg T).Halted)
+    (hfirst : ∀ t < T, ¬ (tm.runFrom cfg t).Halted) :
+    Set.InjOn (fun t => (tm.runFrom cfg t).core) (Set.Iic T) := by
+  intro a ha b hb heq
+  wlog hab : a ≤ b generalizing a b
+  · exact (this hb ha heq.symm (le_of_not_ge hab)).symm
+  by_contra hne
+  change b ≤ T at hb
+  have heq' := tm.core_runFrom_eq_of_core_eq heq (T - b)
+  rw [← runFrom_add, ← runFrom_add, Nat.add_sub_of_le hb] at heq'
+  exact hfirst (a + (T - b)) (by omega) ((congrArg (fun c => c.2.state) heq').trans hhalt)
+
 /-! ## The storages and cores of a space-bounded run
 
 These are the main results giving upper bounds on the number of storages and configuration cores
 reachable in bounded space.
 -/
 
-namespace MultiTapeTM
+/-- If every work head stays in `[-R, R]`, the run visits at most `k * (2 * R + 1)` cells. -/
+lemma spaceUsed_le_of_workTapePos_natAbs_le (cfg : Cfg k Symbol State input) (T R : ℕ)
+    (h : ∀ t ≤ T, ∀ i, ((tm.runFrom cfg t).workTapePos i).natAbs ≤ R) :
+    tm.spaceUsed cfg T ≤ k * (2 * R + 1) := by
+  calc tm.spaceUsed cfg T
+    _ ≤ ∑ _ : Fin k, (window R).card := by
+      apply Finset.sum_le_sum
+      intro i _
+      apply Finset.card_le_card
+      intro z hz
+      obtain ⟨t, ht, rfl⟩ := tm.mem_visitedByTapeHead.mp hz
+      exact mem_window.mpr (h t (by omega) i)
+    _ = k * (2 * R + 1) := by simp
 
 /-- The storage reached after `t` steps fits in the windows given by the per-tape space usage up
 to step `t`. -/

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

@@ -136,6 +136,36 @@ lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n
   · simp
     omega
 
+/-- Moving the input head adds the direction and clamps the result to the two endmarkers. -/
+lemma moveInputPos_val {n : ℕ} (p : Fin (n + 2)) (m : SignType) :
+    (moveInputPos p m).val = min (n + 1) ((p.val : ℤ) + (m.cast : ℤ)).toNat := by
+  simp only [moveInputPos]
+  split <;> simp_all <;> omega
+
+/-- An input-head move changes the position by at most one cell. -/
+lemma moveInputPos_bounds {n : ℕ} (p : Fin (n + 2)) (m : SignType) :
+    (moveInputPos p m).val ≤ p.val + 1 ∧ p.val ≤ (moveInputPos p m).val + 1 := by
+  rw [moveInputPos_val]
+  have := p.isLt
+  cases m <;> simp [SignType.cast] <;> omega
+
+/-- Equal input positions below the right endmarkers remain equal after the same move. -/
+lemma moveInputPos_same {n n' : ℕ} (p : Fin (n + 2)) (p' : Fin (n' + 2))
+    (hp : p.val = p'.val) (hn : p.val ≤ n) (hn' : p'.val ≤ n') (m : SignType) :
+    (moveInputPos p m).val = (moveInputPos p' m).val := by
+  rw [moveInputPos_val, moveInputPos_val]
+  cases m <;> simp [SignType.cast] <;> omega
+
+/-- Shifting a position and the right endmarker by the same amount commutes with a move,
+provided the smaller position is not the left endmarker. -/
+lemma moveInputPos_shift {n n' d : ℕ} (p : Fin (n + 2)) (p' : Fin (n' + 2))
+    (hp : p'.val + d = p.val) (hn : n' + d = n) (hp' : 0 < p'.val) (m : SignType) :
+    (moveInputPos p' m).val + d = (moveInputPos p m).val := by
+  rw [moveInputPos_val, moveInputPos_val]
+  have := p.isLt
+  have := p'.isLt
+  cases m <;> simp [SignType.cast] <;> omega
+
 /-- The symbol currently under the input tape head. -/
 def Cfg.inputSymbol (cfg : Cfg k Symbol State input) : Option Symbol :=
   if h₁ : cfg.inputPos = 0 then none
@@ -149,6 +179,18 @@ lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ)
     cfg.inputSymbol = some input[p] := by
   grind [Cfg.inputSymbol]
 
+/-- Read the input by zero-based optional indexing, returning `none` at either endmarker. -/
+lemma inputSymbol_eq_getElem? (cfg : Cfg k Symbol State input) :
+    cfg.inputSymbol = if cfg.inputPos.val = 0 then none else input[cfg.inputPos.val - 1]? := by
+  by_cases h₀ : cfg.inputPos = 0
+  · simp [Cfg.inputSymbol, h₀]
+  · have h₀' : cfg.inputPos.val ≠ 0 := fun h => h₀ (Fin.ext h)
+    rw [Cfg.inputSymbol, dite_eq_right h₀, ite_eq_right h₀']
+    split_ifs with hend
+    · simp [hend]
+    · have hi : cfg.inputPos.val - 1 < input.length := by have := cfg.inputPos.isLt; omega
+      simp [List.getElem?_eq_getElem hi]
+
 /-- The symbol read by work tape `i`. -/
 def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol :=
   cfg.workTapes i (cfg.workTapePos i)

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

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Order.Group.Abs
 public import Mathlib.Algebra.Order.Group.Int
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Basic.Sign.Defs
+public import Mathlib.Computability.Language
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Computability.Machines.Turing.MultiTape.Configuration
 
@@ -76,6 +77,7 @@ We define a number of structures and concepts related to multi-tape Turing machi
 * `ComputableInTimeAndSpaceOfLength`: the specialization to bounds on encoded input length.
 * `DecidableInTimeAndSpace`: a proof that a TM decides a language within a certain time
     and space bound.
+* `DecidableInSpace`: a language is decidable within a bound on space by input length.
 
 There are two ways to talk about the behaviour of a multi-tape Turing machine, and they are
 proven to be equivalent.
@@ -216,6 +218,15 @@ lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state
     tm.outputSymbol cfg = none := by
   simp [outputSymbol, h_halt]
 
+/-- The input head moves by at most one cell at each step. -/
+lemma inputPos_step_bounds (cfg : Cfg k Symbol State input) :
+    (tm.step cfg).inputPos.val ≤ cfg.inputPos.val + 1 ∧
+      cfg.inputPos.val ≤ (tm.step cfg).inputPos.val + 1 := by
+  unfold step
+  cases cfg.state with
+  | none => simp
+  | some q => exact moveInputPos_bounds _ _
+
 /-- The work-tape head moves by at most one cell in a single step. -/
 lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) :
     |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := by
@@ -292,9 +303,8 @@ lemma runFrom_output_eq_of_halt
     (tm : MultiTapeTM k Symbol State)
     (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t)
     (hhalt : (tm.runFrom cfg τ).state = none) :
-    (tm.runFrom cfg t).output = (tm.runFrom cfg τ).output := by
-  conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm]
-  rw [runFrom_add, runFrom_of_halt _ hhalt]
+    (tm.runFrom cfg t).output = (tm.runFrom cfg τ).output :=
+  congrArg Cfg.output (tm.runFrom_eq_of_halt cfg hle hhalt)
 
 /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps
 and uses exactly `s` space.
@@ -362,6 +372,16 @@ 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
 
+/-- A language is decidable using at most `s n` work-tape cells on inputs of length `n`.
+The last state before halting records the decision: `.inr true` accepts and
+`.inr false` rejects. -/
+def DecidableInSpace {Symbol : Type*} (L : Language Symbol) (s : ℕ → ℕ) : Prop :=
+  ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Symbol (State ⊕ Bool)),
+    ∀ input, ∃ t,
+      (tm.runFrom (tm.initCfg input) t).state = some (.inr (indicator L input)) ∧
+      (tm.runFrom (tm.initCfg input) (t + 1)).Halted ∧
+      tm.spaceUsed (tm.initCfg input) (t + 1) ≤ s input.length
+
 /-- This lemma translates between the relational notion and the iterated step notion. The latter
 can be more convenient especially for deterministic machines as we have here. -/
 @[scoped grind =]