From 786bbb54505b5ae4c8d86d88b9fc2e3fd70204b0 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 21:38:18 +0000 Subject: [PATCH 1/6] refactor(LogSpace): plain statements for query machines and compact configuration graphs (#474, #862) State the space theorems of query machines (`Turing.QueryMachine.computableInSpace`, `.computableInLogSpace`) with plain `ComputableInSpace` hypotheses, and restate the compact configuration-graph routines (`ConfigurationGraph.Radix`, `ConfigurationGraph.Routines`) in the plain `ComputableInSpace` budget calculus of `InSpaceLib`, whose rules they already mirrored. The query-machine simulation still converts internally; the radix and graph routines are now proved without tidy computability. Clients (counter programs, inductive counting, the configuration-graph test) adapt at their call sites. The public tidy surface drops by 11 statements (704 -> 693). This is the plain dependency for the log-squared Savitch simulation of #474 M3. Co-Authored-By: Claude Opus 5.5 --- .../LogSpace/ConfigurationGraph.lean | 2 +- .../LogSpace/ConfigurationGraph/Radix.lean | 14 +-- .../LogSpace/ConfigurationGraph/Routines.lean | 108 +++++++++--------- .../Complexity/LogSpace/CounterProgram.lean | 8 +- .../LogSpace/InductiveCounting/Callbacks.lean | 28 +++-- .../Complexity/LogSpace/QueryMachine.lean | 31 ++--- ComplexityTests/ConfigurationGraph.lean | 4 +- scripts/tidy_surface_baseline.json | 4 +- 8 files changed, 107 insertions(+), 92 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph.lean index 55d4d9019..fd1f28c84 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph.lean @@ -23,7 +23,7 @@ overflows already represents every reachable view, whatever the space of the mac The local edge routine uses one supplied input symbol, forces blank at the native boundary cells, and otherwise performs deterministic arithmetic in linear workspace in the binary radix, length -and vertex IDs. Its `ComputableTidilyInSpace` certificate is for an actual native tidy multi-tape +and vertex IDs. Its `ComputableInSpace` certificate is for an actual native multi-tape machine. The graph-to-source correctness theorem applies without a source halting assumption. ## Main definitions diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean index 13b5f220d..55e7a114c 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean @@ -33,11 +33,11 @@ namespace Turing.MultiTapeNTM.ConfigurationGraph variable {ι : Type} [Fintype ι] -open MultiTapeTM ComputableTidilyInSpace +open MultiTapeTM ComputableInSpace /-- Reading a fixed digit uses linear space in the binary radix and packed value. -/ theorem digit_inSpace (i : ℕ) : - ComputableTidilyInSpace (fun p : ℕ × ℕ => Cslib.Radix.digit p.1 p.2 i) + ComputableInSpace (fun p : ℕ × ℕ => Cslib.Radix.digit p.1 p.2 i) (encPair encNat encNat) encNat fun p => (encPair encNat encNat p).length := by induction i with | zero => exact budget_natMod (snd _ _) (fst _ _) @@ -47,17 +47,17 @@ theorem digit_inSpace (i : ℕ) : /-- Reading any one fixed component is a native deterministic linear-space routine. -/ theorem component_inSpace (i : ι) : - ComputableTidilyInSpace (fun p : ℕ × ℕ => Cslib.Radix.component p.1 p.2 i) + ComputableInSpace (fun p : ℕ × ℕ => Cslib.Radix.component p.1 p.2 i) (encPair encNat encNat) encNat fun p => (encPair encNat encNat p).length := digit_inSpace (Fintype.equivFin ι i).val /-- Packing a fixed tuple of computed components preserves a common space budget. -/ theorem pack_inSpace {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {B : α → ℕ} - {f : α → ι → ℕ} (hB : ComputableTidilyInSpace B enc encNat S) - (hf : ∀ i, ComputableTidilyInSpace (fun a => f a i) enc encNat S) + {f : α → ι → ℕ} (hB : ComputableInSpace B enc encNat S) + (hf : ∀ i, ComputableInSpace (fun a => f a i) enc encNat S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => Cslib.Radix.pack (B a) (f a)) enc encNat S := by - have hlist : ∀ l : List ι, ComputableTidilyInSpace + ComputableInSpace (fun a => Cslib.Radix.pack (B a) (f a)) enc encNat S := by + have hlist : ∀ l : List ι, ComputableInSpace (fun a => Nat.ofDigits (B a) (l.map (f a))) enc encNat S := by intro l induction l with diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Routines.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Routines.lean index 40fdfefd4..e0ddd7acd 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Routines.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Routines.lean @@ -34,32 +34,32 @@ by the caller. namespace Turing.MultiTapeNTM.ConfigurationGraph -open MultiTapeTM ComputableTidilyInSpace +open MultiTapeTM ComputableInSpace variable {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} private theorem and_inSpace {f g : α → Bool} - (hf : ComputableTidilyInSpace f enc encBool S) (hg : ComputableTidilyInSpace g enc encBool S) : - ComputableTidilyInSpace (fun a => f a && g a) enc encBool S := + (hf : ComputableInSpace f enc encBool S) (hg : ComputableInSpace g enc encBool S) : + ComputableInSpace (fun a => f a && g a) enc encBool S := budget_finite (fun p : Bool × Bool => p.1 && p.2) (budget_prod hf hg) private theorem or_inSpace {f g : α → Bool} - (hf : ComputableTidilyInSpace f enc encBool S) (hg : ComputableTidilyInSpace g enc encBool S) : - ComputableTidilyInSpace (fun a => f a || g a) enc encBool S := + (hf : ComputableInSpace f enc encBool S) (hg : ComputableInSpace g enc encBool S) : + ComputableInSpace (fun a => f a || g a) enc encBool S := budget_finite (fun p : Bool × Bool => p.1 || p.2) (budget_prod hf hg) private theorem all_inSpace {ι : Type} (l : List ι) {f : ι → α → Bool} - (hf : ∀ i, ComputableTidilyInSpace (f i) enc encBool S) + (hf : ∀ i, ComputableInSpace (f i) enc encBool S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => (l.map fun i => f i a).all id) enc encBool S := by + ComputableInSpace (fun a => (l.map fun i => f i a).all id) enc encBool S := by induction l with | nil => exact budget_const true hin | cons i l ih => exact and_inSpace (hf i) ih private theorem any_inSpace {ι : Type} (l : List ι) {f : ι → α → Bool} - (hf : ∀ i, ComputableTidilyInSpace (f i) enc encBool S) + (hf : ∀ i, ComputableInSpace (f i) enc encBool S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => l.any fun i => f i a) enc encBool S := by + ComputableInSpace (fun a => l.any fun i => f i a) enc encBool S := by induction l with | nil => exact budget_const false hin | cons i l ih => exact or_inSpace (hf i) ih @@ -68,22 +68,22 @@ variable {k : ℕ} {State : Type} [Fintype State] {B n u v : α → ℕ} {symbol : α → Option Bool} /-- Reading any fixed register preserves a common space budget. -/ -private theorem readRegisters_budget (hB : ComputableTidilyInSpace B enc encNat S) - (hu : ComputableTidilyInSpace u enc encNat S) (i : Register k) : - ComputableTidilyInSpace (fun a => readRegisters (B a) (u a) i) enc encNat S := +private theorem readRegisters_budget (hB : ComputableInSpace B enc encNat S) + (hu : ComputableInSpace u enc encNat S) (i : Register k) : + ComputableInSpace (fun a => readRegisters (B a) (u a) i) enc encNat S := budget_comp_linear (component_inSpace i) (budget_prod hB hu) /-- The ambient graph size is computable from the radix. -/ -theorem vertexBound_budget (hB : ComputableTidilyInSpace B enc encNat S) +theorem vertexBound_budget (hB : ComputableInSpace B enc encNat S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => vertexBound (k := k) (B a)) enc encNat S := + ComputableInSpace (fun a => vertexBound (k := k) (B a)) enc encNat S := budget_natPow hB hin (Fintype.card (Register k)) -private theorem valid_budget (hB : ComputableTidilyInSpace B enc encNat S) - (hn : ComputableTidilyInSpace n enc encNat S) - (hu : ComputableTidilyInSpace u enc encNat S) +private theorem valid_budget (hB : ComputableInSpace B enc encNat S) + (hn : ComputableInSpace n enc encNat S) + (hu : ComputableInSpace u enc encNat S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => valid (k := k) (State := State) (B a) (n a) (u a)) + ComputableInSpace (fun a => valid (k := k) (State := State) (B a) (n a) (u a)) enc encBool S := by have hr := readRegisters_budget (k := k) hB hu have hb := vertexBound_budget (k := k) hB hin @@ -101,21 +101,21 @@ private theorem valid_budget (hB : ComputableTidilyInSpace B enc encNat S) rfl private theorem inputSymbol_budget {p : α → ℕ} - (hn : ComputableTidilyInSpace n enc encNat S) - (hp : ComputableTidilyInSpace p enc encNat S) - (hs : ComputableTidilyInSpace symbol enc (encOption encBool) S) + (hn : ComputableInSpace n enc encNat S) + (hp : ComputableInSpace p enc encNat S) + (hs : ComputableInSpace symbol enc (encOption encBool) S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => inputSymbol (n a) (p a) (symbol a)) + ComputableInSpace (fun a => inputSymbol (n a) (p a) (symbol a)) enc (encOption encBool) S := by have hc := or_inSpace (budget_natIsZero hp) (budget_natEq hp (budget_natSucc hn)) simpa only [inputSymbol, Bool.or_eq_true, decide_eq_true_eq] using budget_ite hc (budget_const none hin) hs private theorem nextRegisters_budget {r : α → Register k → ℕ} - (hn : ComputableTidilyInSpace n enc encNat S) - (hr : ∀ i, ComputableTidilyInSpace (fun a => r a i) enc encNat S) + (hn : ComputableInSpace n enc encNat S) + (hr : ∀ i, ComputableInSpace (fun a => r a i) enc encNat S) (hin : (fun a => (enc a).length) ≼ S) (act : Action k Bool State) (i : Register k) : - ComputableTidilyInSpace (fun a => nextRegisters (n a) (r a) act i) enc encNat S := by + ComputableInSpace (fun a => nextRegisters (n a) (r a) act i) enc encNat S := by cases i with | inputPos => cases hm : act.inputTape with @@ -137,12 +137,12 @@ private theorem nextRegisters_budget {r : α → Register k → ℕ} budget_ite (budget_natIsZero (hr .output)) (budget_const (encB := encNat) (if b then 1 else 2) hin) (budget_const 2 hin) | head i | left i | right i => - have hh : ComputableTidilyInSpace + have hh : ComputableInSpace (fun a => (act.workTapes i).1.elim (r a (.head i)) symbolCode) enc encNat S := by cases (act.workTapes i).1 with | none => exact hr (.head i) | some b => exact budget_const _ hin - have hthree : ComputableTidilyInSpace (fun _ : α => 3) enc encNat S := budget_const 3 hin + have hthree : ComputableInSpace (fun _ : α => 3) enc encNat S := budget_const 3 hin cases hm : (act.workTapes i).2 <;> simp only [nextRegisters, tapeStep, hm] <;> first @@ -153,11 +153,11 @@ private theorem nextRegisters_budget {r : α → Register k → ℕ} | exact budget_natAdd hh (budget_natMul hthree (hr _)) private theorem matchesEntry_budget {r : α → Register k → ℕ} - (hn : ComputableTidilyInSpace n enc encNat S) - (hr : ∀ i, ComputableTidilyInSpace (fun a => r a i) enc encNat S) - (hs : ComputableTidilyInSpace symbol enc (encOption encBool) S) + (hn : ComputableInSpace n enc encNat S) + (hr : ∀ i, ComputableInSpace (fun a => r a i) enc encNat S) + (hs : ComputableInSpace symbol enc (encOption encBool) S) (hin : (fun a => (enc a).length) ≼ S) (t : Instruction k State) : - ComputableTidilyInSpace (fun a => matchesEntry (n a) (r a) (symbol a) t) enc encBool S := by + ComputableInSpace (fun a => matchesEntry (n a) (r a) (symbol a) t) enc encBool S := by have hc := budget_natEq (hr .control) (budget_const (stateCode (some t.1)) hin) have hi := budget_finite (encC := encBool) (fun b : Option Bool => decide (b = t.2.1)) (inputSymbol_budget hn (hr .inputPos) hs hin) @@ -171,22 +171,22 @@ private theorem matchesEntry_budget {r : α → Register k → ℕ} rfl private theorem fitsB_budget {r : α → Register k → ℕ} - (hB : ComputableTidilyInSpace B enc encNat S) - (hr : ∀ i, ComputableTidilyInSpace (fun a => r a i) enc encNat S) + (hB : ComputableInSpace B enc encNat S) + (hr : ∀ i, ComputableInSpace (fun a => r a i) enc encNat S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => fitsB (B a) (r a)) enc encBool S := by + ComputableInSpace (fun a => fitsB (B a) (r a)) enc encBool S := by simpa only [fitsB, List.all_map, Function.comp_def, id_eq] using all_inSpace (Finset.univ.toList : List (Register k)) (fun i => budget_natLt (hr i) hB) hin /-- Local edge evaluation preserves any budget covering the short arguments. -/ theorem edgeWithSymbol_budget (ntm : MultiTapeNTM k Bool State) - (hB : ComputableTidilyInSpace B enc encNat S) - (hn : ComputableTidilyInSpace n enc encNat S) - (hu : ComputableTidilyInSpace u enc encNat S) - (hv : ComputableTidilyInSpace v enc encNat S) - (hs : ComputableTidilyInSpace symbol enc (encOption encBool) S) + (hB : ComputableInSpace B enc encNat S) + (hn : ComputableInSpace n enc encNat S) + (hu : ComputableInSpace u enc encNat S) + (hv : ComputableInSpace v enc encNat S) + (hs : ComputableInSpace symbol enc (encOption encBool) S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => edgeWithSymbol ntm (B a) (n a) (u a) (v a) (symbol a)) + ComputableInSpace (fun a => edgeWithSymbol ntm (B a) (n a) (u a) (v a) (symbol a)) enc encBool S := by have hr := readRegisters_budget (k := k) hB hu have hh := and_inSpace @@ -201,12 +201,12 @@ theorem edgeWithSymbol_budget (ntm : MultiTapeNTM k Bool State) /-- The overflow test preserves any budget covering the short arguments. -/ theorem overflow_budget (ntm : MultiTapeNTM k Bool State) - (hB : ComputableTidilyInSpace B enc encNat S) - (hn : ComputableTidilyInSpace n enc encNat S) - (hu : ComputableTidilyInSpace u enc encNat S) - (hs : ComputableTidilyInSpace symbol enc (encOption encBool) S) + (hB : ComputableInSpace B enc encNat S) + (hn : ComputableInSpace n enc encNat S) + (hu : ComputableInSpace u enc encNat S) + (hs : ComputableInSpace symbol enc (encOption encBool) S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => overflow ntm (B a) (n a) (u a) (symbol a)) + ComputableInSpace (fun a => overflow ntm (B a) (n a) (u a) (symbol a)) enc encBool S := by have hr := readRegisters_budget (k := k) hB hu have hentry (t : Instruction k State) := @@ -216,17 +216,17 @@ theorem overflow_budget (ntm : MultiTapeNTM k Bool State) exact and_inSpace (valid_budget hB hn hu hin) (any_inSpace (instructions ntm) hentry hin) /-- Compute the only input query in native deterministic linear workspace. -/ -theorem queryIndex_budget (hB : ComputableTidilyInSpace B enc encNat S) - (hu : ComputableTidilyInSpace u enc encNat S) : - ComputableTidilyInSpace (fun a => queryIndex (k := k) (B a) (u a)) enc encNat S := +theorem queryIndex_budget (hB : ComputableInSpace B enc encNat S) + (hu : ComputableInSpace u enc encNat S) : + ComputableInSpace (fun a => queryIndex (k := k) (B a) (u a)) enc encNat S := budget_natPred (readRegisters_budget hB hu .inputPos) /-- Recognize the accepting halted vertices in native deterministic linear workspace. -/ -theorem bad_budget (hB : ComputableTidilyInSpace B enc encNat S) - (hn : ComputableTidilyInSpace n enc encNat S) - (hu : ComputableTidilyInSpace u enc encNat S) +theorem bad_budget (hB : ComputableInSpace B enc encNat S) + (hn : ComputableInSpace n enc encNat S) + (hu : ComputableInSpace u enc encNat S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => bad (State := State) (k := k) (B a) (n a) (u a)) + ComputableInSpace (fun a => bad (State := State) (k := k) (B a) (n a) (u a)) enc encBool S := by have hr := readRegisters_budget (k := k) hB hu exact and_inSpace (and_inSpace (valid_budget hB hn hu hin) @@ -235,9 +235,9 @@ theorem bad_budget (hB : ComputableTidilyInSpace B enc encNat S) /-- Compute the input-independent start ID from the radix. -/ theorem startID_budget (ntm : MultiTapeNTM k Bool State) - (hB : ComputableTidilyInSpace B enc encNat S) + (hB : ComputableInSpace B enc encNat S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableTidilyInSpace (fun a => startID ntm (B a)) enc encNat S := + ComputableInSpace (fun a => startID ntm (B a)) enc encNat S := pack_inSpace hB (fun _ => budget_const _ hin) hin end Turing.MultiTapeNTM.ConfigurationGraph diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean index 7fc32ba29..ac2ac44d9 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean @@ -632,9 +632,11 @@ theorem computableInLogSpace {α β : Type} {enc : α ↪ List Bool} {encOut : ComputableInLogSpace f enc encOut := by obtain ⟨d, hd⟩ := hbound exact P.toQueryMachine.computableInLogSpace (encS := Simulation.encConfig) - (Simulation.query_inSpace (P := P)) (Simulation.exec_inSpace (P := P)) - (Simulation.emitted_inSpace (P := P)) (Simulation.halted_inSpace (P := P)) - (Simulation.finish_inSpace (P := P)) time hhalt hpre hf + (Simulation.query_inSpace (P := P)).computableInSpace + (Simulation.exec_inSpace (P := P)).computableInSpace + (Simulation.emitted_inSpace (P := P)).computableInSpace + (Simulation.halted_inSpace (P := P)).computableInSpace + (Simulation.finish_inSpace (P := P)).computableInSpace time hhalt hpre hf ⟨_, fun a t ht => Simulation.length_encConfig_le P (P.run_fst_le _ t) (P.run_snd_length _ t) (hd a t ht)⟩ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean index a7632a1c1..2ccb02231 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean @@ -159,8 +159,9 @@ private theorem controllerQuery_budget {B : α → ℕ} {s : α → Cslib.Induct (fun a => controllerQuery k (B a) { s a with phase := p }) enc encNat S := by cases p <;> dsimp only [controllerQuery, Cslib.InductiveCounting.query] <;> try exact budget_const 0 hin - · exact queryIndex_budget hB (current_budget hs) - · exact (queryIndex_budget hB (candidate_budget hs)).of_enc_eq fun a => by + · exact (queryIndex_budget hB.computableInSpace (current_budget hs).computableInSpace).tidy + · exact (queryIndex_budget hB.computableInSpace + (candidate_budget hs).computableInSpace).tidy.of_enc_eq fun a => by cases (s a).finalScan <;> rfl refine (phaseCases_budget hs _ hbranches hin).of_enc_eq fun a => ?_ cases s a @@ -180,17 +181,25 @@ private theorem localAnswer_budget (ntm : MultiTapeNTM k Bool State) enc encBool S := by have hmode : ComputableTidilyInSpace (fun a => modeBad ntm (B a) (n a) (chk a) (s a).candidate (symbol a)) enc encBool S := - (budget_ite hchk (bad_budget hB hn (candidate_budget hs) hin) - (overflow_budget ntm hB hn (candidate_budget hs) hsymbol hin)).of_enc_eq fun a => by + (budget_ite hchk + (bad_budget hB.computableInSpace hn.computableInSpace + (candidate_budget hs).computableInSpace hin).tidy + (overflow_budget ntm hB.computableInSpace hn.computableInSpace + (candidate_budget hs).computableInSpace hsymbol.computableInSpace hin).tidy).of_enc_eq + fun a => by cases chk a <;> rfl have hbranches (p : Cslib.InductiveCounting.Phase) : ComputableTidilyInSpace (fun a => localAnswer ntm (B a) (n a) (chk a) { s a with phase := p } (symbol a)) enc encBool S := by cases p <;> dsimp only [localAnswer, Cslib.InductiveCounting.query] <;> try exact budget_const false hin - · exact edgeWithSymbol_budget ntm hB hn (current_budget hs) (guess_budget hs) hsymbol hin + · exact (edgeWithSymbol_budget ntm hB.computableInSpace hn.computableInSpace + (current_budget hs).computableInSpace (guess_budget hs).computableInSpace + hsymbol.computableInSpace hin).tidy · exact (budget_ite (finalScan_budget hs) hmode - (edgeWithSymbol_budget ntm hB hn (candidate_budget hs) (target_budget hs) hsymbol hin) + (edgeWithSymbol_budget ntm hB.computableInSpace hn.computableInSpace + (candidate_budget hs).computableInSpace (target_budget hs).computableInSpace + hsymbol.computableInSpace hin).tidy ).of_enc_eq fun a => by cases (s a).finalScan <;> rfl refine (phaseCases_budget hs _ hbranches hin).of_enc_eq fun a => ?_ cases s a @@ -232,7 +241,8 @@ private theorem runtimeAccept_budget {s : α → Runtime} private theorem install_budget (ntm : MultiTapeNTM k Bool State) {B : α → ℕ} (hB : ComputableTidilyInSpace B enc encNat S) (hin : (fun a => (enc a).length) ≼ S) : ComputableTidilyInSpace (fun a => install ntm (B a)) enc encState S := - initial_budget (vertexBound_budget hB hin) (startID_budget ntm hB hin) hin + initial_budget (vertexBound_budget hB.computableInSpace hin).tidy + (startID_budget ntm hB.computableInSpace hin).tidy hin /-- The complete next-state callback, including bootstrap, radix changes, graph evaluation and checked advance, uses the common budget without assuming that the runtime is reachable or well @@ -249,9 +259,9 @@ private theorem runtimeNext_budget (ntm : MultiTapeNTM k Bool State) have hB := runtimeRadix_budget hs have hchk := runtimeChecked_budget hs have hc := controller_budget hs - have hN := vertexBound_budget (k := k) hB hin + have hN := (vertexBound_budget (k := k) hB.computableInSpace hin).tidy have hw := budget_comp_linear sizeUnary_inSpace hN - have hsource := startID_budget ntm hB hin + have hsource := (startID_budget ntm hB.computableInSpace hin).tidy have ha := localAnswer_budget ntm hB hn hchk hc hsymbol hin have hadvance := runtime_budget hn hB hchk (optionSome_budget (advance_budget hN hw hsource hc ha hchoice hin)) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean index 15a1a169a..58364e5b6 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean @@ -24,7 +24,7 @@ abstract, so query machines are a convenient way to describe logarithmic-space a jump around in their input: counters, tuples of elements, indices into tables. Such a machine runs within logarithmic space when its states have logarithmic encodings and its -parts are tidily computable within space linear in the encoded state +parts are computable within space linear in the encoded state (`Turing.QueryMachine.computableInLogSpace`), and more generally within the space of its states, once that is at least logarithmic (`Turing.QueryMachine.computableInSpace`). The proof is a multi-pass fold over the input (`Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.multiPassFold`): @@ -361,18 +361,18 @@ open MultiTapeTM Simulation /-- **Query machines run in the space of their states.** Let a query machine halt on every encoded input `enc a`, first after `time a` steps, with output `encOut (f a)`. If its states along these runs have encodings of length `O(S a)`, where `S a` is at least logarithmic in the length of the -input, and its query, transition, emission, halting test and final word are tidily computable +input, and its query, transition, emission, halting test and final word are computable within space linear in the encoded state, then `f` is computable within space `O(S a)`. The input is not charged, so `S` may be much smaller than the length of the input. -/ theorem computableInSpace {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {σ : Type} {encS : σ ↪ List Bool} (M : QueryMachine σ) - (hquery : ComputableTidilyInSpace M.query encS encNat fun s => (encS s).length) - (hnext : ComputableTidilyInSpace M.next (encPair encS (encOption encBool)) encS + (hquery : ComputableInSpace M.query encS encNat fun s => (encS s).length) + (hnext : ComputableInSpace M.next (encPair encS (encOption encBool)) encS fun p => (encPair encS (encOption encBool) p).length) - (hemit : ComputableTidilyInSpace M.emit (encPair encS (encOption encBool)) encBits + (hemit : ComputableInSpace M.emit (encPair encS (encOption encBool)) encBits fun p => (encPair encS (encOption encBool) p).length) - (hhalted : ComputableTidilyInSpace M.halted encS encBool fun s => (encS s).length) - (hfinish : ComputableTidilyInSpace M.finish encS encBits fun s => (encS s).length) + (hhalted : ComputableInSpace M.halted encS encBool fun s => (encS s).length) + (hfinish : ComputableInSpace M.finish encS encBits fun s => (encS s).length) {f : α → β} (time : α → ℕ) (hhalt : ∀ a, M.halted (M.run (enc a) (time a)) = true) (hpre : ∀ a, ∀ t < time a, M.halted (M.run (enc a) t) = false) @@ -381,6 +381,11 @@ theorem computableInSpace {α β : Type} {enc : α ↪ List Bool} {encOut : β (hsize : ∃ c, ∀ a, ∀ t ≤ time a, (encS (M.run (enc a) t)).length ≤ c * S a) : ∃ t c, ComputableInTimeAndSpace f enc encOut t fun a => c * S a := by obtain ⟨cS, hS⟩ := hsize + replace hquery := hquery.tidy + replace hnext := hnext.tidy + replace hemit := hemit.tidy + replace hhalted := hhalted.tidy + replace hfinish := hfinish.tidy have hS1 (a : α) : 1 ≤ S a := (Nat.le_add_left _ _).trans (hlog a) have hS' (a : α) (t : ℕ) : (encS (M.run (enc a) t)).length ≤ cS * S a := by @@ -545,17 +550,17 @@ theorem computableInSpace {α β : Type} {enc : α ↪ List Bool} {encOut : β /-- **Query machines run in logarithmic space.** Let a query machine halt on every encoded input `enc a`, first after `time a` steps, with output `encOut (f a)`. If its states along these runs have encodings of logarithmic length in the length of the input, and its query, transition, -emission, halting test and final word are tidily computable within space linear in the encoded +emission, halting test and final word are computable within space linear in the encoded state, then `f` is computable in logarithmic space. -/ theorem computableInLogSpace {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {σ : Type} {encS : σ ↪ List Bool} (M : QueryMachine σ) - (hquery : ComputableTidilyInSpace M.query encS encNat fun s => (encS s).length) - (hnext : ComputableTidilyInSpace M.next (encPair encS (encOption encBool)) encS + (hquery : ComputableInSpace M.query encS encNat fun s => (encS s).length) + (hnext : ComputableInSpace M.next (encPair encS (encOption encBool)) encS fun p => (encPair encS (encOption encBool) p).length) - (hemit : ComputableTidilyInSpace M.emit (encPair encS (encOption encBool)) encBits + (hemit : ComputableInSpace M.emit (encPair encS (encOption encBool)) encBits fun p => (encPair encS (encOption encBool) p).length) - (hhalted : ComputableTidilyInSpace M.halted encS encBool fun s => (encS s).length) - (hfinish : ComputableTidilyInSpace M.finish encS encBits fun s => (encS s).length) + (hhalted : ComputableInSpace M.halted encS encBool fun s => (encS s).length) + (hfinish : ComputableInSpace M.finish encS encBits fun s => (encS s).length) {f : α → β} (time : α → ℕ) (hhalt : ∀ a, M.halted (M.run (enc a) (time a)) = true) (hpre : ∀ a, ∀ t < time a, M.halted (M.run (enc a) t) = false) diff --git a/ComplexityTests/ConfigurationGraph.lean b/ComplexityTests/ConfigurationGraph.lean index a204dd547..4e5610c14 100644 --- a/ComplexityTests/ConfigurationGraph.lean +++ b/ComplexityTests/ConfigurationGraph.lean @@ -62,9 +62,9 @@ example (b : Option Bool) : outputStep 2 b = 2 := by rcases b with _ | _ | _ <;> private abbrev encEdge : ℕ × ℕ × ℕ × ℕ × Option Bool ↪ List Bool := encPair encNat (encPair encNat (encPair encNat (encPair encNat (encOption encBool)))) -open ComputableTidilyInSpace in +open ComputableInSpace in /-- The edge routine on its exact encoded arguments, in linear workspace. -/ -example : ComputableTidilyInSpace +example : ComputableInSpace (fun a : ℕ × ℕ × ℕ × ℕ × Option Bool => edgeWithSymbol acceptMachine a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) encEdge encBool (fun a => (encEdge a).length) := by diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 06f1c636d..b68c38f04 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -12,15 +12,13 @@ "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 14, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean": 3, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Routines.lean": 6, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean": 11, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Routines.lean": 34, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine.lean": 5, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Routines.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 9, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 7, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean": 3, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 12, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean": 4, From 7e54c427fb2026550ad3e3a8e599602c7e12f5a6 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 22:00:28 +0000 Subject: [PATCH 2/6] =?UTF-8?q?feat(LogSpace):=20Savitch's=20theorem=20in?= =?UTF-8?q?=20space=20log=C2=B2=20n,=20NL=20and=20RL=20in=20DSPACE(log?= =?UTF-8?q?=C2=B2=20n)=20(#474)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove `NL ⊆ DSPACE(log² n)` [Savitch1970] and, through `RL ⊆ NL`, `RL ⊆ DSPACE(log² n)` (milestone M3 of #474). The machine-level result `Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_log_sq` simulates a recognizer within space `c * (log₂ n + 1)` by a deterministic query machine (`Turing.MultiTapeNTM.LogSquareSavitch.machine`) within space `O((log₂ n + 1) ^ 2)`. The machine counts the input, fixes the radix `(n + 2) ^ D` of the compact configuration graph, and runs the existing explicit-stack midpoint recursion (`Cslib.Reachability.Savitch.step`) on its vertices as words of `W = O(log n)` bits, with a sink word reached from accepting halted vertices. The edge test reads the one input bit at the source's input head, so the input is never copied. The class-level statements live in `Classes/LogSpace/Savitch.lean`. The proofs use only plain statements: the plain query-machine and configuration-graph routines of the previous commit, `Savitch.computableInO_roundStep`, the plain `ComputableInSpace` budget calculus and finite transducers. The run invariant of Savitch's machine (`Savitch.Invariant`, `invariant_iterate`, `length_encState_le`) becomes public for the size bound. Adds bibliography entries Savitch1970 and Hoza2022. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../Complexity/Classes/LogSpace/Savitch.lean | 73 ++ .../Complexity/LogSpace/Savitch.lean | 840 ++++++++++++++++++ .../Complexity/Space/Reachability.lean | 18 +- ComplexityTests/LogSpaceSavitch.lean | 89 ++ references.bib | 19 + 6 files changed, 1034 insertions(+), 7 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean create mode 100644 ComplexityTests/LogSpaceSavitch.lean diff --git a/Complexity.lean b/Complexity.lean index f59b96f22..7158b2018 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1003,6 +1003,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Tr public import Complexity.Computability.Complexity.Classes.LogSpace.PolyTime public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification +public import Complexity.Computability.Complexity.Classes.LogSpace.Savitch public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON public import Complexity.Computability.Complexity.Classes.MIP public import Complexity.Computability.Complexity.Classes.MIP.Defs @@ -1489,6 +1490,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.NondeterministicQueryMachine.Termination public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.QueryMachine public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Reachability +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Savitch public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Words public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Nondeterministic public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean new file mode 100644 index 000000000..3946b387e --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Savitch + +/-! +# Savitch's theorem for logarithmic space: `NL ⊆ DSPACE(log² n)` + +A problem in `Cslib.Complexity.NL` is decided by a deterministic machine within space +`O((log₂ n) ^ 2)` [Savitch1970]: Savitch's midpoint recursion on the compact configuration graph +of the nondeterministic machine, which never copies the input +(`Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_log_sq`). The simulation uses only the space +bound and acceptance, so it also applies to logspace recognizers, whose branches may run forever. +Since one-sided-error randomized logspace is within `NL` (`Cslib.Complexity.RL_subset_NL`), the +same bound holds for `Cslib.Complexity.RL` [Hoza, Section 4.3][Hoza2022]. + +The space classes are `Cslib.Complexity.DSPACE enc fun n => Nat.log2 n ^ 2`, the problems decided +within space `c₁ * (log₂ n) ^ 2 + c₂` on encoded instances of length `n`. + +## Main results + +* `Cslib.Complexity.mem_DSPACE_log2_sq_of_recognizesInSpace`: a logspace recognizer, whose + branches need not halt, places its problem in `DSPACE(log² n)`. +* `Cslib.Complexity.NL_subset_DSPACE_log2_sq`: `NL ⊆ DSPACE(log² n)`. +* `Cslib.Complexity.RL_subset_DSPACE_log2_sq`: `RL ⊆ DSPACE(log² n)`. + +## References + +* [W. J. Savitch, *Relationships between nondeterministic and deterministic tape + complexities*][Savitch1970] +* [W. M. Hoza, *Recent Progress on Derandomizing Space-Bounded Computation*, Section 4.3][Hoza2022] +* [M. Sipser, *Introduction to the Theory of Computation*, Theorem 8.5][Sipser2013] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} + +/-- **Savitch's theorem for logspace recognizers**: a problem recognized by a nondeterministic +machine within space `c * (log₂ n + 1)`, whose branches need not halt, is in `DSPACE(log² n)` +[Savitch1970]. -/ +theorem mem_DSPACE_log2_sq_of_recognizesInSpace {k : ℕ} {State : Type} [Finite State] + {ntm : MultiTapeNTM k Bool State} {c : ℕ} + (hA : ntm.RecognizesInSpace enc A fun a => c * (Nat.log2 (enc a).length + 1)) : + A ∈ DSPACE enc fun n => Nat.log2 n ^ 2 := by + obtain ⟨t, c', h⟩ := MultiTapeNTM.exists_decidableInTimeAndSpace_log_sq hA + refine mem_DSPACE_iff.mpr ⟨2 * c', 2 * c', t, + ComputableInTimeAndSpace.mono h (fun _ => le_rfl) fun a => ?_⟩ + have : (Nat.log2 (enc a).length + 1) ^ 2 ≤ 2 * Nat.log2 (enc a).length ^ 2 + 2 := by nlinarith + have := Nat.mul_le_mul_left c' this + nlinarith + +/-- **Savitch's theorem for logarithmic space**: `NL ⊆ DSPACE(log² n)` [Savitch1970]. -/ +theorem NL_subset_DSPACE_log2_sq : NL enc ⊆ DSPACE enc fun n => Nat.log2 n ^ 2 := by + rintro A ⟨k, State, hfinite, ntm, c, h⟩ + exact mem_DSPACE_log2_sq_of_recognizesInSpace h.recognizesInSpace + +/-- **`RL ⊆ DSPACE(log² n)`**, through `RL ⊆ NL` [Hoza, Section 4.3][Hoza2022]. -/ +theorem RL_subset_DSPACE_log2_sq : RL enc ⊆ DSPACE enc fun n => Nat.log2 n ^ 2 := + fun _ h => NL_subset_DSPACE_log2_sq (RL_subset_NL h) + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean new file mode 100644 index 000000000..5645177e6 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean @@ -0,0 +1,840 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.QueryMachine +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Space.Reachability +import Complexity.Computability.Machines.Turing.MultiTape.Internal.LinearPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryNormalization +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength +import Complexity.Foundations.Data.Nat.Log +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative +import Complexity.Foundations.Data.BitString.ShortWords +import Mathlib.Data.Nat.Size +import Mathlib.Tactic.Linarith + +/-! +# Savitch's theorem in space `log² n` + +A nondeterministic machine whose computation paths on inputs of length `n` visit at most +`c * (log₂ n + 1)` work cells is simulated by a deterministic machine within space +`O((log₂ n + 1) ^ 2)` [Savitch1970]. The simulation runs Savitch's midpoint recursion with an +explicit stack (`Cslib.Reachability.Savitch.step`) on the compact configuration graph of the +machine (`Turing.MultiTapeNTM.ConfigurationGraph`), whose vertices are numbers below +`(n + 2) ^ O(1)` that omit the input. A vertex is stored as a word of `W = O(log n)` bits, so the +stack of at most `W` frames has `O(W ^ 2)` bits. The input is never copied: the simulation is a +query machine (`Turing.QueryMachine`), which reads one input bit per step, and the edge test at +the bottom of the recursion needs exactly one input bit, at the input head of its source vertex. + +The machine first counts the input in binary, then fixes the radix `(n + 2) ^ D` of the graph +and the width `W` of its vertices. To have a single target, the graph on words gains a sink, the +word of `W` ones: every accepting halted vertex steps to it. The recursion at depth `W` then +decides whether the sink is reachable from the start vertex, that is, whether the machine accepts +(`Turing.MultiTapeNTM.LogSquareSavitch.reach_eq_true_iff`). + +## Main definitions + +* `Turing.MultiTapeNTM.LogSquareSavitch.wordEdge`: the edges of the graph on words, given the + input bit at the source. +* `Turing.MultiTapeNTM.LogSquareSavitch.machine`: the deterministic query machine. + +## Main results + +* `Turing.MultiTapeNTM.LogSquareSavitch.reach_eq_true_iff`: the recursion decides acceptance. +* `Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_log_sq`: **Savitch's theorem in space + `log² n`**: a problem recognized by a nondeterministic machine in space `c * (log₂ n + 1)` is + decided by a deterministic machine in space `O((log₂ n + 1) ^ 2)`. +* `Turing.MultiTapeNTM.LogSquareSavitch.exists_run_add`, + `Turing.MultiTapeNTM.LogSquareSavitch.length_encRuntime_run_le`: the machine runs the recursion, + and its states have `O((log₂ n + 1) ^ 2)` bits. + +## References + +* [W. J. Savitch, *Relationships between nondeterministic and deterministic tape + complexities*][Savitch1970] +* [M. Sipser, *Introduction to the Theory of Computation*, Theorem 8.5][Sipser2013] +-/ + +@[expose] public section + +namespace Turing.MultiTapeNTM.LogSquareSavitch + +open MultiTapeTM ConfigurationGraph Cslib.Reachability Cslib.Reachability.Savitch + +/-! ### Words of a fixed width -/ + +/-- The word of width `W` with value `x`, for `x < 2 ^ W`: its binary digits, least significant +first, padded to width `W`. -/ +def pad : ℕ → ℕ → List Bool + | 0, _ => [] + | W + 1, x => x.bodd :: pad W x.div2 + +/-- The word `pad W x` has width `W`. -/ +theorem length_pad (W x : ℕ) : (pad W x).length = W := by + induction W generalizing x with + | zero => rfl + | succ W ih => simp [pad, ih] + +/-- The value of a word, one digit at a time. -/ +theorem ofBits_cons (b : Bool) (u : List Bool) : ofBits (b :: u) = Nat.bit b (ofBits u) := rfl + +/-- The word `pad W x` has value `x`, for `x < 2 ^ W`. -/ +theorem ofBits_pad {W x : ℕ} (hx : x < 2 ^ W) : ofBits (pad W x) = x := by + induction W generalizing x with + | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; rfl + | succ W ih => + rw [pad, ofBits_cons, ih (by rw [Nat.div2_val]; rw [pow_succ] at hx; omega), Nat.bit_bodd_div2] + +/-- The binary digits of `x + 2 ^ W`, for `x < 2 ^ W`, are the word of width `W` with value `x`, +followed by a one. -/ +theorem bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : (x + 2 ^ W).bits = pad W x ++ [true] := by + induction W generalizing x with + | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; simp [pad] + | succ W ih => + have hx' : x.div2 < 2 ^ W := by rw [Nat.div2_val]; rw [pow_succ] at hx; omega + have hbit : x + 2 ^ (W + 1) = Nat.bit x.bodd (x.div2 + 2 ^ W) := by + conv_lhs => rw [← Nat.bit_bodd_div2 x] + rw [Nat.bit_val, Nat.bit_val, pow_succ] + ring + rw [hbit, Nat.bits_append_bit _ _ fun h => by have := Nat.one_le_two_pow (n := W); omega, + ih hx', pad, List.cons_append] + +/-- The word of width `W` with value `x < 2 ^ W` is `(x + 2 ^ W).bits` without its last +digit. -/ +theorem dropLast_bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : + (x + 2 ^ W).bits.dropLast = pad W x := by + rw [bits_add_two_pow hx, List.dropLast_concat] + +/-- The word of width `W` with value `0` is the word of zeros. -/ +theorem pad_zero (W : ℕ) : pad W 0 = List.replicate W false := by + induction W with + | zero => rfl + | succ W ih => rw [pad, Nat.bodd_zero, Nat.div2_zero, ih, List.replicate_succ] + +/-- The word of `W` ones has value `2 ^ W - 1`. -/ +theorem ofBits_replicate_true (W : ℕ) : ofBits (List.replicate W true) = 2 ^ W - 1 := by + induction W with + | zero => rfl + | succ W ih => + rw [List.replicate_succ, ofBits_cons, ih, Nat.bit_val, pow_succ] + have := Nat.one_le_two_pow (n := W) + simp only [Bool.toNat_true] + omega + +/-! ### The graph on words -/ + +variable {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) + +variable (k) in +/-- The width of the words for the vertices of the graph of radix `B`. -/ +noncomputable def width (B : ℕ) : ℕ := (vertexBound (k := k) B).size + +/-- **The edges of the graph on words**, given the input bit `symbol` at the source: the edges of +the compact configuration graph between the values of the words, and an edge from every accepting +halted vertex to the sink, the word of ones. -/ +noncomputable def wordEdge (B n : ℕ) (symbol : Option Bool) (u v : List Bool) : Bool := + edgeWithSymbol ntm B n (ofBits u) (ofBits v) symbol || + (bad (k := k) (State := State) B n (ofBits u) && v.all id) + +/-- The edges of the graph on words, with the radix, the input length and the input bit as one +parameter. -/ +noncomputable def paramEdge (p : ℕ × ℕ × Option Bool) : List Bool → List Bool → Bool := + wordEdge ntm p.1 p.2.1 p.2.2 + +/-- The edges of the graph on words on the input `w`: the input bit is read at the input head of +the source. -/ +noncomputable def inputEdge (B : ℕ) (w : List Bool) (u v : List Bool) : Bool := + wordEdge ntm B w.length w[queryIndex (k := k) B (ofBits u)]? u v + +/-! ### Reachability of the sink -/ + +section Graph + +variable {ntm} {B : ℕ} {w : List Bool} + +variable (k) in +/-- Every vertex of the graph of radix `B` has a word of width `width k B`. -/ +theorem vertexBound_lt_two_pow_width (B : ℕ) : vertexBound (k := k) B < 2 ^ width k B := + Nat.lt_size_self _ + +/-- No vertex is the sink. -/ +theorem vertexBound_le_ofBits_sink (B : ℕ) : + vertexBound (k := k) B ≤ ofBits (List.replicate (width k B) true) := by + rw [ofBits_replicate_true] + have := vertexBound_lt_two_pow_width k B + omega + +/-- **The sink is reachable exactly when an accepting halted vertex is.** Along the graph on words +of width `W = width k B`, from the start vertex to the word of `W` ones. -/ +theorem reflTransGen_sink_iff (hstart : startID ntm B < vertexBound (k := k) B) : + Relation.ReflTransGen (fun a b => a.length = width k B ∧ b.length = width k B ∧ + inputEdge ntm B w a b = true) + (pad (width k B) (startID ntm B)) (List.replicate (width k B) true) ↔ + ∃ u, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ∧ + bad (k := k) (State := State) B w.length u = true := by + have hW := vertexBound_lt_two_pow_width k B + have hsink := vertexBound_le_ofBits_sink (k := k) B + set W := width k B + have hsrc : ofBits (pad W (startID ntm B)) = startID ntm B := ofBits_pad (hstart.trans hW) + constructor + · intro h + have key : ∀ x, Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ + inputEdge ntm B w a b = true) (pad W (startID ntm B)) x → + (∃ u, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ∧ + bad (k := k) (State := State) B w.length u = true) ∨ + (Relation.ReflTransGen (Edge ntm B w) (startID ntm B) (ofBits x) ∧ + x ≠ List.replicate W true) := by + intro x hx + induction hx with + | refl => + refine .inr ⟨by rw [hsrc], fun h => ?_⟩ + have := congrArg ofBits h + omega + | @tail x y _ hxy ih => + obtain ⟨-, -, he⟩ := hxy + rcases ih with ih | ⟨hr, -⟩ + · exact .inl ih + simp only [inputEdge, wordEdge, Bool.or_eq_true, Bool.and_eq_true] at he + rcases he with he | ⟨hb, -⟩ + · refine .inr ⟨hr.tail he, fun h => ?_⟩ + have := (lt_vertexBound_of_edgeWithSymbol he).2 + rw [h] at this + omega + · exact .inl ⟨_, hr, hb⟩ + rcases key _ h with h | ⟨-, h⟩ + · exact h + · exact absurd rfl h + · rintro ⟨u, hu, hb⟩ + have key : ∀ x, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) x → + Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ + inputEdge ntm B w a b = true) (pad W (startID ntm B)) (pad W x) ∧ + x < vertexBound (k := k) B := by + intro x hx + induction hx with + | refl => exact ⟨.refl, hstart⟩ + | @tail a b _ hab ih => + have hlt := lt_vertexBound_of_edgeWithSymbol hab + refine ⟨ih.1.tail ⟨length_pad _ _, length_pad _ _, ?_⟩, hlt.2⟩ + simp only [inputEdge, wordEdge, ofBits_pad (hlt.1.trans hW), + ofBits_pad (hlt.2.trans hW)] + rw [show edgeWithSymbol ntm B w.length a b w[queryIndex (k := k) B a]? = true from hab, + Bool.true_or] + have hu' : u < vertexBound (k := k) B := by + simp only [bad, Bool.and_eq_true] at hb + exact lt_vertexBound_of_valid hb.1.1 + refine (key u hu).1.tail ⟨length_pad _ _, List.length_replicate, ?_⟩ + simp only [inputEdge, wordEdge, ofBits_pad (hu'.trans hW), hb, Bool.true_and, + Bool.or_eq_true] + exact .inr (by simp) + +/-- **The recursion decides acceptance.** For a machine whose computation paths on `w` visit at +most `c * (log₂ |w| + 1)` work cells, Savitch's midpoint recursion at depth `W` on the graph on +words of width `W`, from the start vertex to the sink, decides whether the machine accepts `w`. -/ +theorem reach_eq_true_iff {c : ℕ} (hs : ntm.RunsInSpace w (c * (Nat.log2 w.length + 1))) : + reach (inputEdge ntm (radix (radixExponent State c) w.length) w) + (width k (radix (radixExponent State c) w.length)) + (width k (radix (radixExponent State c) w.length)) + (pad (width k (radix (radixExponent State c) w.length)) + (startID ntm (radix (radixExponent State c) w.length))) + (List.replicate (width k (radix (radixExponent State c) w.length)) true) = true ↔ + ntm.Accepts w := by + set B := radix (radixExponent State c) w.length + set W := width k B + have hstart : startID ntm B < vertexBound (k := k) B := by + rw [← vertexID_init ntm B w] + exact vertexID_lt (fits_of_runsInSpace c hs .refl) + have hsrc : (pad W (startID ntm B)).length = W := length_pad _ _ + have hcard : {x | Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ + inputEdge ntm B w a b = true) (pad W (startID ntm B)) x}.encard ≤ 2 ^ W + 1 := by + refine (Set.encard_le_encard fun x hx => ?_).trans + ((Cslib.BitString.encard_setOf_length_eq _).le.trans le_self_add) + induction hx with + | refl => exact hsrc + | tail _ hstep _ => exact hstep.2.1 + rw [reach_iff hsrc List.length_replicate, + ← Relation.reflTransGen_iff_relatesWithinSteps_of_encard_le hcard, + reflTransGen_sink_iff hstart, accepts_iff_reachable_bad_of_runsInSpace c hs] + +end Graph + +/-! ### The query machine -/ + +/-- The encoding of the parameter of the edge test: the radix and the input length in binary, and +the input bit read last. -/ +abbrev encParam : ℕ × ℕ × Option Bool ↪ List Bool := + encPair encNat (encPair encNat (encOption encBool)) + +/-- The states of the machine: the input counter, which becomes the input length; whether the +recursion has started; and a round of the recursion, with its parameter and width. -/ +abbrev Runtime := ℕ × Bool × ((ℕ × ℕ × Option Bool) × ℕ) × Savitch.State + +/-- The encoding of the states of the machine. -/ +abbrev encRuntime : Runtime ↪ List Bool := encPair encNat (encPair encBool (encRound encParam)) + +/-- The first round of the recursion on inputs of length `n`, for the radix `(n + 2) ^ D`: the +call at depth `W` from the start vertex to the sink. The start vertex is written as the binary +digits of its value plus `2 ^ W`, without the last one (`bits_add_two_pow`). -/ +noncomputable def initRound (D n : ℕ) : ((ℕ × ℕ × Option Bool) × ℕ) × Savitch.State := + (((radix D n, n, none), width k (radix D n)), + ⟨[], .call (width k (radix D n)) + (startID ntm (radix D n) + 2 ^ width k (radix D n)).bits.dropLast + (List.replicate (width k (radix D n)) true)⟩) + +/-- The round held while the input is counted. -/ +def idle : ((ℕ × ℕ × Option Bool) × ℕ) × Savitch.State := (((0, 0, none), 0), ⟨[], .ret false⟩) + +/-- The source of the pending call, if any. -/ +def callSource (st : Savitch.State) : List Bool := (st.reg.toPair.1.getD (0, [], [])).2.1 + +variable (k) in +/-- The input bit to read: the next input position while counting, then the input head of the +source of the pending call. -/ +noncomputable def query (s : Runtime) : ℕ := + if s.2.1 then queryIndex (k := k) s.2.2.1.1.1 (ofBits (callSource s.2.2.2)) else s.1 + +/-- A step of the machine, given the input bit read: count the input until its end, then start +the recursion, then run its rounds with the bit read as the input bit of the edge test. -/ +noncomputable def next (D : ℕ) (p : Runtime × Option Bool) : Runtime := + if p.1.2.1 then + (p.1.1, true, roundStep (paramEdge ntm) + (((p.1.2.2.1.1.1, p.1.2.2.1.1.2.1, p.2), p.1.2.2.1.2), p.1.2.2.2)) + else if p.2.isSome then (p.1.1 + 1, false, p.1.2.2) + else (p.1.1, true, initRound ntm D p.1.1) + +/-- The machine halts once the recursion has returned. -/ +def halted (s : Runtime) : Bool := + s.2.1 && s.2.2.2.stack.isEmpty && !s.2.2.2.reg.toPair.1.isSome + +/-- The answer: the value returned by the recursion. -/ +def finish (s : Runtime) : List Bool := [s.2.2.2.reg.toPair.2] + +/-- **The deterministic simulation**, as a query machine: count the input, then run Savitch's +recursion on the graph on words of the radix `(n + 2) ^ D`, reading the input bit of each edge +test. -/ +noncomputable def machine (D : ℕ) : QueryMachine Runtime where + init := (0, false, idle) + query := query k + next := next ntm D + emit _ := [] + halted := halted + finish := finish + +/-! ### The runs of the machine -/ + +section Run + +variable {ntm} {D : ℕ} (w : List Bool) + +/-- The step of the recursion only uses the edge test at a call at level `0`. -/ +theorem step_congr {e₁ e₂ : List Bool → List Bool → Bool} {W : ℕ} {st : Savitch.State} + (h : ∀ u v, st.reg = .call 0 u v → e₁ u v = e₂ u v) : + Savitch.step e₁ W st = Savitch.step e₂ W st := by + obtain ⟨stack, (⟨_ | i, u, v⟩ | b)⟩ := st + · simp only [Savitch.step, h u v rfl] + · rfl + · cases stack <;> cases b <;> rfl + +/-- The machine emits nothing before its final answer. -/ +theorem output_eq (t : ℕ) : (machine ntm D).output w t = finish ((machine ntm D).run w t) := by + rw [QueryMachine.output] + conv_rhs => rw [← List.nil_append (finish _)] + congr 1 + simp only [List.flatten_eq_nil_iff, List.mem_map] + rintro _ ⟨i, -, rfl⟩ + split <;> rfl + +/-- While counting, the machine holds the number of input bits read. -/ +theorem run_of_le {t : ℕ} (ht : t ≤ w.length) : (machine ntm D).run w t = (t, false, idle) := by + induction t with + | zero => rfl + | succ t ih => + rw [QueryMachine.run_succ, ih (by omega)] + have hread : (machine ntm D).read w (t, false, idle) = some w[t] := by + simp [QueryMachine.read, machine, query, + List.getElem?_eq_getElem (show t < w.length by omega)] + rw [QueryMachine.step, hread] + simp [machine, halted, next] + +/-- At the end of the input, the machine starts the recursion. -/ +theorem run_length_succ : + (machine ntm D).run w (w.length + 1) = (w.length, true, initRound ntm D w.length) := by + rw [QueryMachine.run_succ, run_of_le w le_rfl] + have hread : (machine ntm D).read w (w.length, false, idle) = none := by + simp [QueryMachine.read, machine, query] + rw [QueryMachine.step, hread] + simp [machine, halted, next] + +/-- **The machine runs the recursion** on the graph on words of the input, with the input bit of +each edge test read at the source of its call. -/ +theorem exists_run_add (j : ℕ) : ∃ symbol, (machine ntm D).run w (w.length + 1 + j) = + (w.length, true, (((radix D w.length, w.length, symbol), width k (radix D w.length)), + (Savitch.step (inputEdge ntm (radix D w.length) w) (width k (radix D w.length)))^[j] + (initRound ntm D w.length).2)) := by + induction j with + | zero => exact ⟨none, run_length_succ w⟩ + | succ j ih => + obtain ⟨symbol, ih⟩ := ih + set st := (Savitch.step (inputEdge ntm (radix D w.length) w) (width k (radix D w.length)))^[j] + (initRound ntm D w.length).2 + rw [← Nat.add_assoc, QueryMachine.run_succ, ih, Function.iterate_succ_apply'] + by_cases hh : halted (w.length, true, (((radix D w.length, w.length, symbol), + width k (radix D w.length)), st)) = true + · refine ⟨symbol, ?_⟩ + have hst : ∃ b, st = ⟨[], .ret b⟩ := by + obtain ⟨stack, (⟨i, u, v⟩ | b)⟩ := st + · simp [halted, Reg.toPair] at hh + · simp only [halted, Bool.true_and, Bool.and_eq_true, List.isEmpty_iff, + Bool.not_eq_eq_eq_not, Bool.not_true] at hh + exact ⟨b, by rw [hh.1]⟩ + obtain ⟨b, hb⟩ := hst + have hfix : Savitch.step (inputEdge ntm (radix D w.length) w) (width k (radix D w.length)) + st = st := by + rw [hb]; rfl + rw [hfix, QueryMachine.step] + simp only [show (machine ntm D).halted _ = true from hh, ↓reduceIte] + · refine ⟨w[queryIndex (k := k) (radix D w.length) (ofBits (callSource st))]?, ?_⟩ + simp only [Bool.not_eq_true] at hh + simp only [QueryMachine.step, machine, hh, Bool.false_eq_true, ↓reduceIte, + QueryMachine.read, query, next, roundStep, paramEdge] + congr 3 + refine step_congr fun u v hreg => ?_ + simp [inputEdge, callSource, hreg, Reg.toPair] + +end Run + +/-! ### Halting and the size of the states -/ + +section Halting + +variable {ntm} {D : ℕ} {w : List Bool} + +/-- The first round, once the start vertex is known to have a word. -/ +theorem initRound_snd (hstart : startID ntm (radix D w.length) < 2 ^ width k (radix D w.length)) : + (initRound ntm D w.length).2 = ⟨[], .call (width k (radix D w.length)) + (pad (width k (radix D w.length)) (startID ntm (radix D w.length))) + (List.replicate (width k (radix D w.length)) true)⟩ := by + rw [initRound, dropLast_bits_add_two_pow hstart] + +/-- **The machine halts with the value of the recursion.** -/ +theorem exists_halted (hstart : startID ntm (radix D w.length) < 2 ^ width k (radix D w.length)) : + ∃ t, halted ((machine ntm D).run w t) = true ∧ + finish ((machine ntm D).run w t) = + [reach (inputEdge ntm (radix D w.length) w) (width k (radix D w.length)) + (width k (radix D w.length)) + (pad (width k (radix D w.length)) (startID ntm (radix D w.length))) + (List.replicate (width k (radix D w.length)) true)] := by + obtain ⟨T, -, hT⟩ := exists_iterate_step_call (edge := inputEdge ntm (radix D w.length) w) + (w := width k (radix D w.length)) (width k (radix D w.length)) + (pad (width k (radix D w.length)) (startID ntm (radix D w.length))) + (List.replicate (width k (radix D w.length)) true) [] + obtain ⟨symbol, h⟩ := exists_run_add (ntm := ntm) (D := D) w T + refine ⟨w.length + 1 + T, ?_⟩ + rw [h, initRound_snd hstart, hT] + exact ⟨rfl, rfl⟩ + +/-- The states of the recursion satisfy the invariant of a run at depth `W`. -/ +theorem invariant_iterate_initRound + (hstart : startID ntm (radix D w.length) < 2 ^ width k (radix D w.length)) (j : ℕ) : + Invariant (width k (radix D w.length)) (width k (radix D w.length)) + ((Savitch.step (inputEdge ntm (radix D w.length) w) (width k (radix D w.length)))^[j] + (initRound ntm D w.length).2) := by + refine invariant_iterate _ ?_ j + rw [initRound_snd hstart] + refine ⟨trivial, fun i u v h => ?_⟩ + obtain ⟨rfl, rfl, rfl⟩ := Reg.call.inj h + exact ⟨by simp, length_pad _ _, List.length_replicate⟩ + +/-- The binary length of the radix `(n + 2) ^ D`. -/ +theorem length_encNat_radix_le (D n : ℕ) : + (encNat (radix D n)).length ≤ (D + 1) * (Nat.log2 n + 2) := by + refine (length_encNat_le_of_le_pow (N := n + 1) (d := D) (le_of_eq (by simp [radix]))).trans ?_ + have : Nat.log2 (n + 1) ≤ Nat.log2 n + 1 := by + rw [Nat.log2_eq_log_two, Nat.log2_eq_log_two] + exact Nat.log_add_one_le 2 n + exact Nat.mul_le_mul_left _ (by omega) + +/-- The width of the words for the radix `(n + 2) ^ D`. -/ +theorem width_radix_le (D n : ℕ) : + width k (radix D n) ≤ (D * Fintype.card (Register k) + 1) * (Nat.log2 n + 2) := by + rw [width, ← length_encNat_eq_size, vertexBound_eq_pow] + refine (length_encNat_le_of_le_pow (N := n + 1) le_rfl).trans ?_ + have : Nat.log2 (n + 1) ≤ Nat.log2 n + 1 := by + rw [Nat.log2_eq_log_two, Nat.log2_eq_log_two] + exact Nat.log_add_one_le 2 n + exact Nat.mul_le_mul_left _ (by omega) + +variable (k) in +/-- The constant of the bound on the states of the machine. -/ +noncomputable def sizeConst (D : ℕ) : ℕ := + 40 + (encRound encParam idle).length + 16 * (D + 1) + 4 * (D * Fintype.card (Register k) + 1) + + 24 * (2 * (D * Fintype.card (Register k) + 1) + 1) * + (4 * (D * Fintype.card (Register k) + 1) + 1) + +/-- **The states of the machine have `O((log₂ n + 1) ^ 2)` bits.** -/ +theorem length_encRuntime_run_le + (hstart : startID ntm (radix D w.length) < 2 ^ width k (radix D w.length)) (t : ℕ) : + (encRuntime ((machine ntm D).run w t)).length ≤ + sizeConst k D * (Nat.log2 w.length + 1) ^ 2 := by + rw [sizeConst] + generalize hI : (encRound encParam idle).length = I + rcases le_or_gt t w.length with ht | ht + · rw [run_of_le w ht] + have h₁ := length_encNat_le_log2 ht + rw [encRuntime, length_encPair, length_encPair, encBool_apply, List.length_singleton, hI] + generalize Nat.log2 w.length = L at * + generalize D * Fintype.card (Register k) = R + have hLL : L + 1 ≤ (L + 1) ^ 2 := Nat.le_self_pow (by omega) _ + calc 2 * (encNat t).length + 1 + (2 * 1 + 1 + I) ≤ (40 + I) * (L + 1) := by nlinarith + _ ≤ (40 + I) * (L + 1) ^ 2 := Nat.mul_le_mul_left _ hLL + _ ≤ _ := Nat.mul_le_mul_right _ (by omega) + · obtain ⟨j, rfl⟩ : ∃ j, t = w.length + 1 + j := ⟨t - (w.length + 1), by omega⟩ + obtain ⟨symbol, h⟩ := exists_run_add (ntm := ntm) (D := D) w j + rw [h] + have hinv := length_encState_le (invariant_iterate_initRound hstart j) + have hn := length_encNat_le_log2 (le_refl w.length) + have hB := length_encNat_radix_le D w.length + have hW := width_radix_le (k := k) D w.length + have hsym : (encOption encBool symbol).length ≤ 2 := by cases symbol <;> simp + simp only [encRuntime, encRound, encParam, length_encPair, encBool_apply, encUnary_apply, + List.length_singleton, List.length_replicate] + generalize Nat.log2 w.length = L at * + generalize D * Fintype.card (Register k) = R at * + generalize width k (radix D w.length) = W at * + generalize (encState _).length = E at * + generalize (encNat (radix D w.length)).length = Bl at * + generalize (encNat w.length).length = nl at * + generalize (encOption encBool symbol).length = sl at * + have hLL : L + 1 ≤ (L + 1) ^ 2 := Nat.le_self_pow (by omega) _ + have hW' : W ≤ 2 * (R + 1) * (L + 1) := by nlinarith + have hB' : Bl ≤ 2 * (D + 1) * (L + 1) := by nlinarith + have hst : E ≤ 24 * (2 * (R + 1) + 1) * (4 * (R + 1) + 1) * (L + 1) ^ 2 := by + refine hinv.trans ?_ + have h₁ : W + 1 ≤ (2 * (R + 1) + 1) * (L + 1) := by nlinarith + have h₂ : W + W + 1 ≤ (4 * (R + 1) + 1) * (L + 1) := by nlinarith + have := Nat.mul_le_mul h₁ h₂ + nlinarith + have hlin : 2 * nl + 1 + (2 * 1 + 1 + (2 * (2 * (2 * Bl + 1 + (2 * nl + 1 + sl)) + 1 + W) + 1)) + ≤ (40 + 16 * (D + 1) + 4 * (R + 1)) * (L + 1) ^ 2 := by + have : (40 + 16 * (D + 1) + 4 * (R + 1)) * (L + 1) ≤ + (40 + 16 * (D + 1) + 4 * (R + 1)) * (L + 1) ^ 2 := Nat.mul_le_mul_left _ hLL + nlinarith + nlinarith + +end Halting + +/-! ### The parts of the machine in linear space -/ + +section Parts + +open ComputableInSpace + +/-- A function computed by a finite transducer is computable in linear space. -/ +theorem transducer_inSpace {Q : Type} [Finite Q] (τ : Transducer Bool Q) {α β : Type} + {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} + (h : ∀ a, encOut (f a) = τ.run τ.q₀ (encIn a)) : + ComputableInSpace f encIn encOut fun a => (encIn a).length := + of_inO (ComputableInO.of_linear (ComputableInLinearTimeAndSpace.of_transducer τ h)) + +/-- Whether its input is nonempty, as a transducer. -/ +def nonemptyT : Transducer Bool Bool where + q₀ := false + step _ _ := (true, []) + final q := [q] + length_step_le _ _ := by simp + length_final_le _ := by simp + +/-- `nonemptyT` emits whether its input is nonempty. -/ +theorem nonemptyT_run (q : Bool) (l : List Bool) : nonemptyT.run q l = [q || !l.isEmpty] := by + induction l generalizing q with + | nil => simp [nonemptyT] + | cons a l ih => rw [Transducer.run_cons, ih]; simp [nonemptyT] + +/-- Whether an option holds a value, in linear space. -/ +theorem isSome_inSpace {β : Type} (e : β ↪ List Bool) : + ComputableInSpace (fun o : Option β => o.isSome) (encOption e) encBool + fun o => (encOption e o).length := + transducer_inSpace nonemptyT fun o => by + rw [nonemptyT_run] + cases o <;> rfl + +/-- Whether every bit is one, as a transducer. -/ +def allT : Transducer Bool Bool where + q₀ := true + step q a := (q && a, []) + final q := [q] + length_step_le _ _ := by simp + length_final_le _ := by simp + +/-- `allT` emits whether every bit of its input is one. -/ +theorem allT_run (q : Bool) (l : List Bool) : allT.run q l = [q && l.all id] := by + induction l generalizing q with + | nil => simp [allT] + | cons a l ih => rw [Transducer.run_cons, ih]; simp [allT, Bool.and_assoc] + +/-- The length of a word in unary, as a transducer. -/ +def unaryT : Transducer Bool Unit where + q₀ := () + step _ _ := ((), [true]) + final _ := [] + length_step_le _ _ := by simp + length_final_le _ := by simp + +/-- `unaryT` emits the length of its input in unary. -/ +theorem unaryT_run (l : List Bool) : unaryT.run () l = List.replicate l.length true := by + induction l with + | nil => simp [unaryT] + | cons a l ih => rw [Transducer.run_cons, ih]; simp [unaryT, List.replicate_succ] + +/-- `2 ^ n` in binary from `n` in unary, as a transducer. -/ +def twoPowT : Transducer Bool Unit where + q₀ := () + step _ _ := ((), [false]) + final _ := [true] + length_step_le _ _ := by simp + length_final_le _ := by simp + +/-- `twoPowT` emits `2 ^ n` in binary on `n` in unary. -/ +theorem twoPowT_run (n : ℕ) : twoPowT.run () (List.replicate n true) = (2 ^ n).bits := by + have h := bits_add_two_pow (W := n) (x := 0) (Nat.two_pow_pos n) + rw [Nat.zero_add, pad_zero] at h + rw [h] + clear h + induction n with + | zero => simp [twoPowT] + | succ n ih => + rw [List.replicate_succ, Transducer.run_cons, ih] + simp [twoPowT, List.replicate_succ] + +/-- The value of a word, in linear space. -/ +theorem ofBits_inSpace : ComputableInSpace ofBits encBits encNat fun l => (encBits l).length := + of_inO ComputableInO.bitsToNat + +variable {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} + +/-- `Option.some`, within a budget. -/ +theorem budget_some {β : Type} {e : β ↪ List Bool} {f : α → β} + (hf : ComputableInSpace f enc e S) (hin : (fun a => (enc a).length) ≼ S) : + ComputableInSpace (fun a => some (f a)) enc (encOption e) S := + ((budget_const (encB := encBool) true hin).append hf fun _ => rfl).weaken + (.add (.refl _) (.refl _)) + +/-- The fields of a state of the recursion, as pairs. -/ +theorem stateFields_inSpace : + ComputableInSpace (fun st : Savitch.State => (st.stack, st.reg.toPair)) encState + (encPair (encList encFrame) (encPair (encOption encCall) encBool)) + fun st => (encState st).length := + of_inO (ComputableInO.of_eq fun _ => rfl) + +/-- The stack, within a budget. -/ +theorem budget_stack {st : α → Savitch.State} (h : ComputableInSpace st enc encState S) : + ComputableInSpace (fun a => (st a).stack) enc (encList encFrame) S := + (budget_comp_lin (fst _ _) (.refl _) (budget_comp_linear stateFields_inSpace h)).of_enc_eq + fun _ => rfl + +/-- The register as a pair, within a budget. -/ +theorem budget_reg {st : α → Savitch.State} (h : ComputableInSpace st enc encState S) : + ComputableInSpace (fun a => (st a).reg.toPair) enc (encPair (encOption encCall) encBool) S := + (budget_comp_lin (snd _ _) (.refl _) (budget_comp_linear stateFields_inSpace h)).of_enc_eq + fun _ => rfl + +/-- The value of the source of the pending call, within a budget. -/ +theorem budget_callSource {st : α → Savitch.State} (h : ComputableInSpace st enc encState S) : + ComputableInSpace (fun a => ofBits (callSource (st a))) enc encNat S := by + have hreg := budget_reg h + have hopt := budget_comp_lin (fst _ _) (.refl _) hreg + have hcall := budget_comp_linear + (of_inO + (ComputableInDegree.optionGetD encCall ((0, [], []) : ℕ × List Bool × List Bool)).inO_one) + hopt + have hu := budget_comp_lin (fst _ _) (.refl _) (budget_comp_lin (snd _ _) (.refl _) hcall) + exact (budget_comp_linear ofBits_inSpace hu).of_enc_eq fun _ => rfl + +/-- The projections of a state of the machine, within a budget. -/ +theorem budget_runtime {s : α → Runtime} (h : ComputableInSpace s enc encRuntime S) : + ComputableInSpace (fun a => (s a).1) enc encNat S ∧ + ComputableInSpace (fun a => (s a).2.1) enc encBool S ∧ + ComputableInSpace (fun a => (s a).2.2) enc (encRound encParam) S ∧ + ComputableInSpace (fun a => (s a).2.2.1.1.1) enc encNat S ∧ + ComputableInSpace (fun a => (s a).2.2.1.1.2.1) enc encNat S ∧ + ComputableInSpace (fun a => (s a).2.2.1.2) enc encUnary S ∧ + ComputableInSpace (fun a => (s a).2.2.2) enc encState S := by + have hrest := budget_comp_lin (snd _ _) (.refl _) h + have hround := budget_comp_lin (snd _ _) (.refl _) hrest + have hpw := budget_comp_lin (fst _ _) (.refl _) hround + have hparam := budget_comp_lin (fst _ _) (.refl _) hpw + exact ⟨budget_comp_lin (fst _ _) (.refl _) h, budget_comp_lin (fst _ _) (.refl _) hrest, hround, + budget_comp_lin (fst _ _) (.refl _) hparam, + budget_comp_lin (fst _ _) (.refl _) (budget_comp_lin (snd _ _) (.refl _) hparam), + budget_comp_lin (snd _ _) (.refl _) hpw, budget_comp_lin (snd _ _) (.refl _) hround⟩ + +/-- The input position to read, in space linear in the state. -/ +theorem query_inSpace : + ComputableInSpace (query k) encRuntime encNat fun s => (encRuntime s).length := by + obtain ⟨hk, hstarted, -, hB, -, -, hst⟩ := budget_runtime (ComputableInSpace.of_inO + (ComputableInO.of_eq (encIn := encRuntime) (encMid := encRuntime) (f := id) fun _ => rfl)) + exact (budget_ite hstarted (queryIndex_budget (k := k) hB (budget_callSource hst)) hk).of_enc_eq + fun _ => rfl + +/-- The halting test, in space linear in the state. -/ +theorem halted_inSpace : + ComputableInSpace halted encRuntime encBool fun s => (encRuntime s).length := by + obtain ⟨-, hstarted, -, -, -, -, hst⟩ := budget_runtime (ComputableInSpace.of_inO + (ComputableInO.of_eq (encIn := encRuntime) (encMid := encRuntime) (f := id) fun _ => rfl)) + have hempty := budget_isEmpty (budget_stack hst) + have hsome := budget_comp_linear (isSome_inSpace encCall) + (budget_comp_lin (fst _ _) (.refl _) (budget_reg hst)) + exact (budget_finite (fun p : Bool × Bool × Bool => p.1 && p.2.1 && !p.2.2) + (budget_prod hstarted (budget_prod hempty hsome))).of_enc_eq fun _ => rfl + +/-- The answer, in space linear in the state. -/ +theorem finish_inSpace : + ComputableInSpace finish encRuntime encBits fun s => (encRuntime s).length := by + obtain ⟨-, -, -, -, -, -, hst⟩ := budget_runtime (ComputableInSpace.of_inO + (ComputableInO.of_eq (encIn := encRuntime) (encMid := encRuntime) (f := id) fun _ => rfl)) + exact (budget_comp_lin (snd _ _) (.refl _) (budget_reg hst)).of_enc_eq fun _ => rfl + +/-- The edge test of the graph on words, in linear space. -/ +theorem paramEdge_inSpace : ComputableInSpace + (fun q : (ℕ × ℕ × Option Bool) × List Bool × List Bool => paramEdge ntm q.1 q.2.1 q.2.2) + (encPair encParam (encPair encBits encBits)) encBool + fun q => (encPair encParam (encPair encBits encBits) q).length := by + have hp := fst encParam (encPair encBits encBits) + have huv := snd encParam (encPair encBits encBits) + have hB := budget_comp_lin (fst _ _) (.refl _) hp + have hrest := budget_comp_lin (snd _ _) (.refl _) hp + have hn := budget_comp_lin (fst _ _) (.refl _) hrest + have hsym := budget_comp_lin (snd _ _) (.refl _) hrest + have hu := budget_comp_lin (fst _ _) (.refl _) huv + have hv := budget_comp_lin (snd _ _) (.refl _) huv + have hvalU := budget_comp_linear ofBits_inSpace hu + have hvalV := budget_comp_linear ofBits_inSpace hv + have hin : (fun q : (ℕ × ℕ × Option Bool) × List Bool × List Bool => + (encPair encParam (encPair encBits encBits) q).length) ≼ _ := .refl _ + have he := edgeWithSymbol_budget ntm hB hn hvalU hvalV hsym hin + have hb := bad_budget (k := k) (State := State) hB hn hvalU hin + have hall := budget_comp_linear (transducer_inSpace (encIn := encBits) (encOut := encBool) + (f := fun l : List Bool => l.all id) allT fun l => by rw [allT_run]; rfl) hv + exact (budget_finite (fun p : Bool × Bool × Bool => p.1 || (p.2.1 && p.2.2)) + (budget_prod he (budget_prod hb hall))).of_enc_eq fun _ => rfl + +/-- A round of the recursion on the graph on words, in space linear in the round. -/ +theorem roundStep_inSpace : ComputableInSpace (roundStep (paramEdge ntm)) (encRound encParam) + (encRound encParam) fun q => (encRound encParam q).length := by + obtain ⟨Te, hedge⟩ := (paramEdge_inSpace ntm).exists_inO + refine (of_inO (computableInO_roundStep hedge)).weaken (.of_le_linear 3 0 fun q => ?_) + rcases h : q.2.reg with ⟨i, u, v⟩ | b + · have hreg := length_encReg_call i u v + have hst := length_encState q.2 + rw [h, hreg] at hst + simp only [Reg.edgeCost, encRound, length_encPair, encBits_apply] at hst ⊢ + omega + · simp only [Reg.edgeCost] + omega + +/-- The first round, from the input length, in linear space. -/ +theorem initRound_inSpace (D : ℕ) : ComputableInSpace (initRound ntm D) encNat (encRound encParam) + fun n => (encNat n).length := by + have hn : ComputableInSpace (fun n : ℕ => n) encNat encNat fun n => (encNat n).length := + of_inO (ComputableInO.of_eq fun _ => rfl) + have hin : (fun n : ℕ => (encNat n).length) ≼ fun n => (encNat n).length := .refl _ + have hB : ComputableInSpace (fun n => radix D n) encNat encNat fun n => (encNat n).length := + (budget_natPow (budget_natAdd hn (budget_const 2 hin)) hin D).of_enc_eq fun _ => rfl + have hN := vertexBound_budget (k := k) hB hin + have hW₀ := budget_comp_linear (transducer_inSpace (encIn := encNat) (encOut := encUnary) + (f := Nat.size) unaryT fun x => by + rw [unaryT_run, encUnary_apply, encNat_apply, Nat.size_eq_bits_len]) hN + have hW : ComputableInSpace (fun n => width k (radix D n)) encNat encUnary + fun n => (encNat n).length := hW₀.of_enc_eq fun _ => rfl + have hstart := startID_budget ntm hB hin + have hpow := budget_comp_linear (transducer_inSpace (encIn := encUnary) (encOut := encNat) + (f := fun W => 2 ^ W) twoPowT fun W => (twoPowT_run W).symm) hW + have hbits : ComputableInSpace + (fun n => (startID ntm (radix D n) + 2 ^ width k (radix D n)).bits) encNat encBits + fun n => (encNat n).length := + (budget_natAdd hstart hpow).of_enc_eq fun _ => rfl + have hsrc := budget_comp_linear (of_inO ComputableInDegree.bitsDropLast.inO_one) hbits + have hsink : ComputableInSpace (fun n => List.replicate (width k (radix D n)) true) encNat + encBits fun n => (encNat n).length := hW.of_enc_eq fun _ => rfl + have hcall := budget_some (e := encCall) (budget_prod hW (budget_prod hsrc hsink)) hin + have hstate : ComputableInSpace (fun n => (initRound ntm D n).2) encNat encState + fun n => (encNat n).length := + (budget_prod (budget_const (encB := encList encFrame) [] hin) + (budget_prod hcall (budget_const (encB := encBool) false hin))).of_enc_eq fun _ => rfl + exact (budget_prod (budget_prod (budget_prod hB (budget_prod hn + (budget_const (encB := encOption encBool) none hin))) hW) hstate).of_enc_eq fun _ => rfl + +/-- A step of the machine, in space linear in the state and the bit read. -/ +theorem next_inSpace (D : ℕ) : ComputableInSpace (next ntm D) + (encPair encRuntime (encOption encBool)) encRuntime + fun p => (encPair encRuntime (encOption encBool) p).length := by + have hin : (fun p : Runtime × Option Bool => (encPair encRuntime (encOption encBool) p).length) + ≼ _ := .refl _ + have hs := fst encRuntime (encOption encBool) + have hsym := snd encRuntime (encOption encBool) + obtain ⟨hk, hstarted, hround, hB, hn, hW, hst⟩ := budget_runtime hs + have hq := budget_prod (budget_prod (budget_prod hB (budget_prod hn hsym)) hW) hst + have hA := budget_prod hk (budget_prod (budget_const (encB := encBool) true hin) + (budget_comp_linear (roundStep_inSpace ntm) hq)) + have hC := budget_prod (budget_natSucc hk) (budget_prod + (budget_const (encB := encBool) false hin) hround) + have hI := budget_prod hk (budget_prod (budget_const (encB := encBool) true hin) + (budget_comp_linear (initRound_inSpace ntm D) hk)) + have hsome := budget_comp_linear (isSome_inSpace encBool) hsym + exact (budget_ite hstarted hA (budget_ite hsome hC hI)).of_enc_eq fun _ => rfl + +end Parts + +end Turing.MultiTapeNTM.LogSquareSavitch + +namespace Turing.MultiTapeNTM + +open MultiTapeTM ConfigurationGraph LogSquareSavitch + +/-- **Savitch's theorem in space `log² n`** [Savitch1970]. A problem recognized by a +nondeterministic machine whose computation paths on `enc a` visit at most +`c * (log₂ |enc a| + 1)` work cells, and whose branches need not halt, is decided by a +deterministic machine within space `O((log₂ |enc a| + 1) ^ 2)`: Savitch's midpoint recursion on +the compact configuration graph of the machine +(`Turing.MultiTapeNTM.LogSquareSavitch.machine`). -/ +theorem exists_decidableInTimeAndSpace_log_sq {α : Type} {enc : α ↪ List Bool} {A : Set α} + {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} {c : ℕ} + (hA : ntm.RecognizesInSpace enc A fun a => c * (Nat.log2 (enc a).length + 1)) : + ∃ t c', DecidableInTimeAndSpace A enc t fun a => c' * (Nat.log2 (enc a).length + 1) ^ 2 := by + classical + let : Fintype State := Fintype.ofFinite State + set D := radixExponent State c + have hstart (a : α) : + startID ntm (radix D (enc a).length) < 2 ^ width k (radix D (enc a).length) := by + rw [← vertexID_init ntm _ (enc a)] + exact (vertexID_lt (fits_of_runsInSpace c (hA a).1 .refl)).trans + (vertexBound_lt_two_pow_width k _) + have hex (a : α) : ∃ t, (machine ntm D).halted ((machine ntm D).run (enc a) t) = true := + let ⟨t, h, _⟩ := exists_halted (hstart a) + ⟨t, h⟩ + have hhalt (a : α) := Nat.find_spec (hex a) + have hpre (a : α) : ∀ t < Nat.find (hex a), + (machine ntm D).halted ((machine ntm D).run (enc a) t) = false := fun t ht => by + simpa using Nat.find_min (hex a) ht + have hf (a : α) : + encBool (decide (a ∈ A)) = (machine ntm D).output (enc a) (Nat.find (hex a)) := by + obtain ⟨t, ht, hfin⟩ := exists_halted (hstart a) + rw [output_eq, ← (machine ntm D).run_eq_of_le (enc a) (hhalt a) (Nat.find_min' (hex a) ht), + hfin, encBool_apply] + congr 1 + rw [Bool.eq_iff_iff, reach_eq_true_iff (hA a).1, decide_eq_true_iff] + exact (hA a).2 + obtain ⟨t, c', h⟩ := (machine ntm D).computableInSpace query_inSpace (next_inSpace ntm D) + (ComputableInSpace.const []) halted_inSpace finish_inSpace (fun a => Nat.find (hex a)) + hhalt hpre hf (fun a => (Nat.log2 (enc a).length + 1) ^ 2) + (fun a => Nat.le_self_pow two_ne_zero _) + ⟨sizeConst k D, fun a t _ => length_encRuntime_run_le (hstart a) t⟩ + exact ⟨t, c', decidableInTimeAndSpace_iff.mpr ⟨_, h, fun a => by simp⟩⟩ + +end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean index e6d6cf33b..0418d771b 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean @@ -47,10 +47,14 @@ polynomial time, the space is polynomial (`Cslib.Reachability.exists_polyBounded `Cslib.Reachability.Savitch.encState`: the encoded states of the machine. * `Cslib.Reachability.Savitch.roundStep`, `Cslib.Reachability.Savitch.encRound`: a step carrying the parameter of the edge test and the width, and its encoding. +* `Cslib.Reachability.Savitch.Invariant`: the states of a run from a call at a given level. ## Main results * `Cslib.Reachability.Savitch.computableInO_roundStep`: the time and space of a round. +* `Cslib.Reachability.Savitch.invariant_iterate`, `Cslib.Reachability.Savitch.length_encState_le`: + the states of a run hold at most `d` frames, so their encodings have length + `O((d + 1) * (d + w + 1))`. * `Cslib.Reachability.computableInO_savitch`: the time and space of Savitch's algorithm. * `Cslib.Reachability.exists_polyBounded_space_savitch`: Savitch's algorithm in polynomial space. @@ -484,13 +488,13 @@ theorem roundStep_iterate (edge : π → List Bool → List Bool → Bool) (p : /-- The frames of a run from a call at level `d` with words of width `w`: a frame with `n` frames below it is at a level below `d - n`, and its words have width `w`. -/ -private def StackOk (w d : ℕ) : List Frame → Prop +def StackOk (w d : ℕ) : List Frame → Prop | [] => True | f :: stack => f.level + 1 + stack.length ≤ d ∧ f.src.length = w ∧ f.dst.length = w ∧ f.mid.length = w ∧ StackOk w d stack /-- The states of a run from a call at level `d` with words of width `w`. -/ -private def Invariant (w d : ℕ) (s : State) : Prop := +def Invariant (w d : ℕ) (s : State) : Prop := StackOk w d s.stack ∧ ∀ i u v, s.reg = .call i u v → i + s.stack.length ≤ d ∧ u.length = w ∧ v.length = w @@ -502,7 +506,7 @@ private theorem length_of_next {u m : List Bool} (h : next u = some m) : m.lengt exact length_increment u /-- The step keeps the invariant of a run. -/ -private theorem invariant_step (edge : List Bool → List Bool → Bool) {w d : ℕ} {s : State} +theorem invariant_step (edge : List Bool → List Bool → Bool) {w d : ℕ} {s : State} (h : Invariant w d s) : Invariant w d (step edge w s) := by obtain ⟨hst, hreg⟩ := h obtain ⟨stack, (⟨_ | i, u, v⟩ | b)⟩ := s @@ -535,21 +539,21 @@ private theorem invariant_step (edge : List Bool → List Bool → Bool) {w d : exact ⟨hst, fun _ _ _ h => by cases h⟩ /-- Every state of a run keeps the invariant. -/ -private theorem invariant_iterate (edge : List Bool → List Bool → Bool) {w d : ℕ} {s : State} +theorem invariant_iterate (edge : List Bool → List Bool → Bool) {w d : ℕ} {s : State} (h : Invariant w d s) (k : ℕ) : Invariant w d ((step edge w)^[k] s) := by induction k with | zero => exact h | succ k ih => rw [Function.iterate_succ_apply']; exact invariant_step edge ih /-- A run from a call at level `d` holds at most `d` frames. -/ -private theorem StackOk.length_le {w d : ℕ} : +theorem StackOk.length_le {w d : ℕ} : ∀ {stack : List Frame}, StackOk w d stack → stack.length ≤ d | [], _ => Nat.zero_le _ | _ :: _, h => by have := h.1; simp only [List.length_cons]; omega /-- The frames of a run from a call at level `d` are below level `d`, with words of width `w`. -/ -private theorem StackOk.mem {w d : ℕ} : +theorem StackOk.mem {w d : ℕ} : ∀ {stack : List Frame}, StackOk w d stack → ∀ f ∈ stack, f.level < d ∧ f.src.length = w ∧ f.dst.length = w ∧ f.mid.length = w | [], _, _, hf => by simp at hf @@ -561,7 +565,7 @@ private theorem StackOk.mem {w d : ℕ} : /-- The states of a run from a call at level `d`, with words of width `w`, are of size `O((d + 1) * (d + w + 1))`: at most `d` frames of size `O(d + w)`, and a call of size `O(d + w)`. -/ -private theorem length_encState_le {w d : ℕ} {s : State} (h : Invariant w d s) : +theorem length_encState_le {w d : ℕ} {s : State} (h : Invariant w d s) : (encState s).length ≤ 24 * (d + 1) * (d + w + 1) := by obtain ⟨hst, hreg⟩ := h have hlist : (encList encFrame s.stack).length ≤ d * (2 * (2 * d + 6 * w + 5) + 1) := by diff --git a/ComplexityTests/LogSpaceSavitch.lean b/ComplexityTests/LogSpaceSavitch.lean new file mode 100644 index 000000000..0e4bee2d0 --- /dev/null +++ b/ComplexityTests/LogSpaceSavitch.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Computability.Complexity.Classes.LogSpace.Savitch +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Savitch + +/-! +# Tests: Savitch's theorem in space `log² n` + +Words of a fixed width and the start word written as `(x + 2 ^ W).bits.dropLast`; the counting +phase of the query machine; the recursion deciding acceptance for a machine without work tapes +that accepts every input, so that the hypotheses of the machine-level theorem are satisfiable; and +the class inclusions `NL ⊆ DSPACE(log² n)` and `RL ⊆ DSPACE(log² n)` on concrete problems. +-/ + +namespace ComplexityTests.LogSpaceSavitch + +open Cslib.Turing Turing Turing.MultiTapeTM Cslib.Complexity +open Turing.MultiTapeNTM.ConfigurationGraph Turing.MultiTapeNTM.LogSquareSavitch + +/-! ### Words of a fixed width -/ + +example : pad 4 5 = [true, false, true, false] := by decide +example : (5 + 2 ^ 4).bits.dropLast = pad 4 5 := by decide +example : ofBits (pad 6 37) = 37 := by decide +example : ofBits (List.replicate 5 true) = 31 := by decide +example : (pad 3 0, pad 0 0) = ([false, false, false], []) := by decide + +/-! ### A machine accepting every input -/ + +private def acceptAction : Action 0 Bool Unit := + { inputTape := 0, workTapes := Fin.elim0, output := some true, state := none } + +private def acceptMachine : MultiTapeNTM 0 Bool Unit where + q₀ := () + Tr _ _ _ a := a = acceptAction + +private theorem accepts_acceptMachine (w : List Bool) : acceptMachine.Accepts w := by + have hstep : acceptMachine.Step (acceptMachine.initCfg w) + (acceptAction.apply (acceptMachine.initCfg w)) := ⟨acceptAction, rfl, rfl⟩ + refine ⟨⟨(RelSeries.singleton _ _).cons (acceptMachine.initCfg w) hstep, rfl⟩, ?_, ?_⟩ <;> + simp [acceptAction] + +-- While counting, the query machine holds the number of input bits read, and at the end of the +-- input it starts the recursion. +example (D : ℕ) : (machine acceptMachine D).run [true, false, true] 2 = (2, false, idle) := + run_of_le _ (by decide) + +example (D : ℕ) : + (machine acceptMachine D).run [true, false] 3 = (2, true, initRound acceptMachine D 2) := + run_length_succ [true, false] + +/-- The recursion on the graph on words decides acceptance, here of every input. -/ +example (w : List Bool) : + Cslib.Reachability.reach (inputEdge acceptMachine (radix (radixExponent Unit 0) w.length) w) + (width 0 (radix (radixExponent Unit 0) w.length)) + (width 0 (radix (radixExponent Unit 0) w.length)) + (pad (width 0 (radix (radixExponent Unit 0) w.length)) + (startID acceptMachine (radix (radixExponent Unit 0) w.length))) + (List.replicate (width 0 (radix (radixExponent Unit 0) w.length)) true) = true := + (reach_eq_true_iff (MultiTapeNTM.runsInSpace_zero_tapes _ _ _)).mpr (accepts_acceptMachine w) + +/-- The machine-level theorem applies to a concrete recognizer. -/ +example : ∃ t c', DecidableInTimeAndSpace (Set.univ : Set (List Bool)) encBits t + fun w => c' * (Nat.log2 (encBits w).length + 1) ^ 2 := + MultiTapeNTM.exists_decidableInTimeAndSpace_log_sq (ntm := acceptMachine) (c := 0) + fun w => ⟨MultiTapeNTM.runsInSpace_zero_tapes _ _ _, by simpa using accepts_acceptMachine w⟩ + +example : (Set.univ : Set (List Bool)) ∈ DSPACE encBits fun n => Nat.log2 n ^ 2 := + mem_DSPACE_log2_sq_of_recognizesInSpace (ntm := acceptMachine) (c := 0) + fun w => ⟨MultiTapeNTM.runsInSpace_zero_tapes _ _ _, by simpa using accepts_acceptMachine w⟩ + +/-! ### The class inclusions -/ + +example {α : Type} (enc : α ↪ List Bool) : NL enc ⊆ DSPACE enc fun n => Nat.log2 n ^ 2 := + NL_subset_DSPACE_log2_sq + +example {α : Type} (enc : α ↪ List Bool) : RL enc ⊆ DSPACE enc fun n => Nat.log2 n ^ 2 := + RL_subset_DSPACE_log2_sq + +/-- Every problem in `L` is in `DSPACE(log² n)` through `RL`. -/ +example {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ L enc) : + A ∈ DSPACE enc fun n => Nat.log2 n ^ 2 := + RL_subset_DSPACE_log2_sq (L_subset_RL h) + +end ComplexityTests.LogSpaceSavitch diff --git a/references.bib b/references.bib index ffd09ecfe..70acf8376 100644 --- a/references.bib +++ b/references.bib @@ -2234,6 +2234,14 @@ @book{ Hopcroft2006 address = {USA} } +@misc{Hoza2022, + author = {Hoza, William M.}, + title = {Recent Progress on Derandomizing Space-Bounded Computation}, + year = {2022}, + note = {Electronic Colloquium on Computational Complexity (ECCC), TR22-121}, + url = {https://eccc.weizmann.ac.il/report/2022/121/} +} + @article{Huang2019, author = {Huang, Hao}, title = {Induced Subgraphs of Hypercubes and a Proof of the Sensitivity Conjecture}, @@ -3817,6 +3825,17 @@ @Book{ Sangiorgi2011 doi = {10.1017/CBO9780511777110} } +@article{Savitch1970, + author = {Savitch, Walter J.}, + title = {Relationships between Nondeterministic and Deterministic Tape Complexities}, + journal = {Journal of Computer and System Sciences}, + volume = {4}, + number = {2}, + pages = {177--192}, + year = {1970}, + doi = {10.1016/S0022-0000(70)80006-X} +} + @article{Schaefer1978, author = {Schaefer, Thomas J.}, title = {On the Complexity of Some Two-Person Perfect-Information Games}, From 7b3d3a4900ee3fbb3f4a3333b572d3d885d09e10 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 22:18:52 +0000 Subject: [PATCH 3/6] refactor(LogSpace): reuse existing transducers in the log-squared Savitch simulation (#474) Address the review of #1671: - the power of two from unary uses `ComputableInDegree.two_pow_length encUnary` instead of a copy of `Turing.MultiTapeTM.twoPowT`; - `isSome_inSpace` is `ComputableInDegree.isSome` instead of a new transducer; - the all-ones test reuses `Cslib.Reachability.Savitch.allT`, now public, instead of a copy. The fixed-width words move to `Encodings/Nat/Words.lean` as `Turing.MultiTapeTM.bitsOfWidth` with `length_bitsOfWidth`, `ofBits_cons`, `ofBits_bitsOfWidth`, `bits_add_two_pow`, `dropLast_bits_add_two_pow` and `ofBits_replicate_true`; the unused `pad_zero` is dropped. `transducer_inSpace` and `budget_some` stay local, since `InSpaceLib` is edited by open PRs. Co-Authored-By: Claude Opus 5.5 --- .../Complexity/LogSpace/Savitch.lean | 158 +++--------------- .../Complexity/Space/Reachability.lean | 4 +- .../Turing/MultiTape/Encodings/Nat/Words.lean | 57 +++++++ ComplexityTests/LogSpaceSavitch.lean | 10 +- 4 files changed, 91 insertions(+), 138 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean index 5645177e6..5a051e943 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean @@ -14,6 +14,8 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.LinearPrimiti import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryNormalization import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength import Complexity.Foundations.Data.Nat.Log +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower +import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeOptionPrimitives import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative import Complexity.Foundations.Data.BitString.ShortWords @@ -68,66 +70,6 @@ namespace Turing.MultiTapeNTM.LogSquareSavitch open MultiTapeTM ConfigurationGraph Cslib.Reachability Cslib.Reachability.Savitch -/-! ### Words of a fixed width -/ - -/-- The word of width `W` with value `x`, for `x < 2 ^ W`: its binary digits, least significant -first, padded to width `W`. -/ -def pad : ℕ → ℕ → List Bool - | 0, _ => [] - | W + 1, x => x.bodd :: pad W x.div2 - -/-- The word `pad W x` has width `W`. -/ -theorem length_pad (W x : ℕ) : (pad W x).length = W := by - induction W generalizing x with - | zero => rfl - | succ W ih => simp [pad, ih] - -/-- The value of a word, one digit at a time. -/ -theorem ofBits_cons (b : Bool) (u : List Bool) : ofBits (b :: u) = Nat.bit b (ofBits u) := rfl - -/-- The word `pad W x` has value `x`, for `x < 2 ^ W`. -/ -theorem ofBits_pad {W x : ℕ} (hx : x < 2 ^ W) : ofBits (pad W x) = x := by - induction W generalizing x with - | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; rfl - | succ W ih => - rw [pad, ofBits_cons, ih (by rw [Nat.div2_val]; rw [pow_succ] at hx; omega), Nat.bit_bodd_div2] - -/-- The binary digits of `x + 2 ^ W`, for `x < 2 ^ W`, are the word of width `W` with value `x`, -followed by a one. -/ -theorem bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : (x + 2 ^ W).bits = pad W x ++ [true] := by - induction W generalizing x with - | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; simp [pad] - | succ W ih => - have hx' : x.div2 < 2 ^ W := by rw [Nat.div2_val]; rw [pow_succ] at hx; omega - have hbit : x + 2 ^ (W + 1) = Nat.bit x.bodd (x.div2 + 2 ^ W) := by - conv_lhs => rw [← Nat.bit_bodd_div2 x] - rw [Nat.bit_val, Nat.bit_val, pow_succ] - ring - rw [hbit, Nat.bits_append_bit _ _ fun h => by have := Nat.one_le_two_pow (n := W); omega, - ih hx', pad, List.cons_append] - -/-- The word of width `W` with value `x < 2 ^ W` is `(x + 2 ^ W).bits` without its last -digit. -/ -theorem dropLast_bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : - (x + 2 ^ W).bits.dropLast = pad W x := by - rw [bits_add_two_pow hx, List.dropLast_concat] - -/-- The word of width `W` with value `0` is the word of zeros. -/ -theorem pad_zero (W : ℕ) : pad W 0 = List.replicate W false := by - induction W with - | zero => rfl - | succ W ih => rw [pad, Nat.bodd_zero, Nat.div2_zero, ih, List.replicate_succ] - -/-- The word of `W` ones has value `2 ^ W - 1`. -/ -theorem ofBits_replicate_true (W : ℕ) : ofBits (List.replicate W true) = 2 ^ W - 1 := by - induction W with - | zero => rfl - | succ W ih => - rw [List.replicate_succ, ofBits_cons, ih, Nat.bit_val, pow_succ] - have := Nat.one_le_two_pow (n := W) - simp only [Bool.toNat_true] - omega - /-! ### The graph on words -/ variable {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) @@ -176,17 +118,18 @@ of width `W = width k B`, from the start vertex to the word of `W` ones. -/ theorem reflTransGen_sink_iff (hstart : startID ntm B < vertexBound (k := k) B) : Relation.ReflTransGen (fun a b => a.length = width k B ∧ b.length = width k B ∧ inputEdge ntm B w a b = true) - (pad (width k B) (startID ntm B)) (List.replicate (width k B) true) ↔ + (bitsOfWidth (width k B) (startID ntm B)) (List.replicate (width k B) true) ↔ ∃ u, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ∧ bad (k := k) (State := State) B w.length u = true := by have hW := vertexBound_lt_two_pow_width k B have hsink := vertexBound_le_ofBits_sink (k := k) B set W := width k B - have hsrc : ofBits (pad W (startID ntm B)) = startID ntm B := ofBits_pad (hstart.trans hW) + have hsrc : ofBits (bitsOfWidth W (startID ntm B)) = startID ntm B := + ofBits_bitsOfWidth (hstart.trans hW) constructor · intro h have key : ∀ x, Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ - inputEdge ntm B w a b = true) (pad W (startID ntm B)) x → + inputEdge ntm B w a b = true) (bitsOfWidth W (startID ntm B)) x → (∃ u, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ∧ bad (k := k) (State := State) B w.length u = true) ∨ (Relation.ReflTransGen (Edge ntm B w) (startID ntm B) (ofBits x) ∧ @@ -214,23 +157,23 @@ theorem reflTransGen_sink_iff (hstart : startID ntm B < vertexBound (k := k) B) · rintro ⟨u, hu, hb⟩ have key : ∀ x, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) x → Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ - inputEdge ntm B w a b = true) (pad W (startID ntm B)) (pad W x) ∧ + inputEdge ntm B w a b = true) (bitsOfWidth W (startID ntm B)) (bitsOfWidth W x) ∧ x < vertexBound (k := k) B := by intro x hx induction hx with | refl => exact ⟨.refl, hstart⟩ | @tail a b _ hab ih => have hlt := lt_vertexBound_of_edgeWithSymbol hab - refine ⟨ih.1.tail ⟨length_pad _ _, length_pad _ _, ?_⟩, hlt.2⟩ - simp only [inputEdge, wordEdge, ofBits_pad (hlt.1.trans hW), - ofBits_pad (hlt.2.trans hW)] + refine ⟨ih.1.tail ⟨length_bitsOfWidth _ _, length_bitsOfWidth _ _, ?_⟩, hlt.2⟩ + simp only [inputEdge, wordEdge, ofBits_bitsOfWidth (hlt.1.trans hW), + ofBits_bitsOfWidth (hlt.2.trans hW)] rw [show edgeWithSymbol ntm B w.length a b w[queryIndex (k := k) B a]? = true from hab, Bool.true_or] have hu' : u < vertexBound (k := k) B := by simp only [bad, Bool.and_eq_true] at hb exact lt_vertexBound_of_valid hb.1.1 - refine (key u hu).1.tail ⟨length_pad _ _, List.length_replicate, ?_⟩ - simp only [inputEdge, wordEdge, ofBits_pad (hu'.trans hW), hb, Bool.true_and, + refine (key u hu).1.tail ⟨length_bitsOfWidth _ _, List.length_replicate, ?_⟩ + simp only [inputEdge, wordEdge, ofBits_bitsOfWidth (hu'.trans hW), hb, Bool.true_and, Bool.or_eq_true] exact .inr (by simp) @@ -241,7 +184,7 @@ theorem reach_eq_true_iff {c : ℕ} (hs : ntm.RunsInSpace w (c * (Nat.log2 w.len reach (inputEdge ntm (radix (radixExponent State c) w.length) w) (width k (radix (radixExponent State c) w.length)) (width k (radix (radixExponent State c) w.length)) - (pad (width k (radix (radixExponent State c) w.length)) + (bitsOfWidth (width k (radix (radixExponent State c) w.length)) (startID ntm (radix (radixExponent State c) w.length))) (List.replicate (width k (radix (radixExponent State c) w.length)) true) = true ↔ ntm.Accepts w := by @@ -250,9 +193,9 @@ theorem reach_eq_true_iff {c : ℕ} (hs : ntm.RunsInSpace w (c * (Nat.log2 w.len have hstart : startID ntm B < vertexBound (k := k) B := by rw [← vertexID_init ntm B w] exact vertexID_lt (fits_of_runsInSpace c hs .refl) - have hsrc : (pad W (startID ntm B)).length = W := length_pad _ _ + have hsrc : (bitsOfWidth W (startID ntm B)).length = W := length_bitsOfWidth _ _ have hcard : {x | Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ - inputEdge ntm B w a b = true) (pad W (startID ntm B)) x}.encard ≤ 2 ^ W + 1 := by + inputEdge ntm B w a b = true) (bitsOfWidth W (startID ntm B)) x}.encard ≤ 2 ^ W + 1 := by refine (Set.encard_le_encard fun x hx => ?_).trans ((Cslib.BitString.encard_setOf_length_eq _).le.trans le_self_add) induction hx with @@ -280,7 +223,7 @@ abbrev encRuntime : Runtime ↪ List Bool := encPair encNat (encPair encBool (en /-- The first round of the recursion on inputs of length `n`, for the radix `(n + 2) ^ D`: the call at depth `W` from the start vertex to the sink. The start vertex is written as the binary -digits of its value plus `2 ^ W`, without the last one (`bits_add_two_pow`). -/ +digits of its value plus `2 ^ W`, without the last one (`Turing.MultiTapeTM.bits_add_two_pow`). -/ noncomputable def initRound (D n : ℕ) : ((ℕ × ℕ × Option Bool) × ℕ) × Savitch.State := (((radix D n, n, none), width k (radix D n)), ⟨[], .call (width k (radix D n)) @@ -418,7 +361,7 @@ variable {ntm} {D : ℕ} {w : List Bool} /-- The first round, once the start vertex is known to have a word. -/ theorem initRound_snd (hstart : startID ntm (radix D w.length) < 2 ^ width k (radix D w.length)) : (initRound ntm D w.length).2 = ⟨[], .call (width k (radix D w.length)) - (pad (width k (radix D w.length)) (startID ntm (radix D w.length))) + (bitsOfWidth (width k (radix D w.length)) (startID ntm (radix D w.length))) (List.replicate (width k (radix D w.length)) true)⟩ := by rw [initRound, dropLast_bits_add_two_pow hstart] @@ -428,11 +371,11 @@ theorem exists_halted (hstart : startID ntm (radix D w.length) < 2 ^ width k (ra finish ((machine ntm D).run w t) = [reach (inputEdge ntm (radix D w.length) w) (width k (radix D w.length)) (width k (radix D w.length)) - (pad (width k (radix D w.length)) (startID ntm (radix D w.length))) + (bitsOfWidth (width k (radix D w.length)) (startID ntm (radix D w.length))) (List.replicate (width k (radix D w.length)) true)] := by obtain ⟨T, -, hT⟩ := exists_iterate_step_call (edge := inputEdge ntm (radix D w.length) w) (w := width k (radix D w.length)) (width k (radix D w.length)) - (pad (width k (radix D w.length)) (startID ntm (radix D w.length))) + (bitsOfWidth (width k (radix D w.length)) (startID ntm (radix D w.length))) (List.replicate (width k (radix D w.length)) true) [] obtain ⟨symbol, h⟩ := exists_run_add (ntm := ntm) (D := D) w T refine ⟨w.length + 1 + T, ?_⟩ @@ -449,7 +392,7 @@ theorem invariant_iterate_initRound rw [initRound_snd hstart] refine ⟨trivial, fun i u v h => ?_⟩ obtain ⟨rfl, rfl, rfl⟩ := Reg.call.inj h - exact ⟨by simp, length_pad _ _, List.length_replicate⟩ + exact ⟨by simp, length_bitsOfWidth _ _, List.length_replicate⟩ /-- The binary length of the radix `(n + 2) ^ D`. -/ theorem length_encNat_radix_le (D n : ℕ) : @@ -542,41 +485,11 @@ theorem transducer_inSpace {Q : Type} [Finite Q] (τ : Transducer Bool Q) {α β ComputableInSpace f encIn encOut fun a => (encIn a).length := of_inO (ComputableInO.of_linear (ComputableInLinearTimeAndSpace.of_transducer τ h)) -/-- Whether its input is nonempty, as a transducer. -/ -def nonemptyT : Transducer Bool Bool where - q₀ := false - step _ _ := (true, []) - final q := [q] - length_step_le _ _ := by simp - length_final_le _ := by simp - -/-- `nonemptyT` emits whether its input is nonempty. -/ -theorem nonemptyT_run (q : Bool) (l : List Bool) : nonemptyT.run q l = [q || !l.isEmpty] := by - induction l generalizing q with - | nil => simp [nonemptyT] - | cons a l ih => rw [Transducer.run_cons, ih]; simp [nonemptyT] - /-- Whether an option holds a value, in linear space. -/ theorem isSome_inSpace {β : Type} (e : β ↪ List Bool) : ComputableInSpace (fun o : Option β => o.isSome) (encOption e) encBool fun o => (encOption e o).length := - transducer_inSpace nonemptyT fun o => by - rw [nonemptyT_run] - cases o <;> rfl - -/-- Whether every bit is one, as a transducer. -/ -def allT : Transducer Bool Bool where - q₀ := true - step q a := (q && a, []) - final q := [q] - length_step_le _ _ := by simp - length_final_le _ := by simp - -/-- `allT` emits whether every bit of its input is one. -/ -theorem allT_run (q : Bool) (l : List Bool) : allT.run q l = [q && l.all id] := by - induction l generalizing q with - | nil => simp [allT] - | cons a l ih => rw [Transducer.run_cons, ih]; simp [allT, Bool.and_assoc] + of_inO (ComputableInDegree.isSome e).inO_one /-- The length of a word in unary, as a transducer. -/ def unaryT : Transducer Bool Unit where @@ -592,26 +505,6 @@ theorem unaryT_run (l : List Bool) : unaryT.run () l = List.replicate l.length t | nil => simp [unaryT] | cons a l ih => rw [Transducer.run_cons, ih]; simp [unaryT, List.replicate_succ] -/-- `2 ^ n` in binary from `n` in unary, as a transducer. -/ -def twoPowT : Transducer Bool Unit where - q₀ := () - step _ _ := ((), [false]) - final _ := [true] - length_step_le _ _ := by simp - length_final_le _ := by simp - -/-- `twoPowT` emits `2 ^ n` in binary on `n` in unary. -/ -theorem twoPowT_run (n : ℕ) : twoPowT.run () (List.replicate n true) = (2 ^ n).bits := by - have h := bits_add_two_pow (W := n) (x := 0) (Nat.two_pow_pos n) - rw [Nat.zero_add, pad_zero] at h - rw [h] - clear h - induction n with - | zero => simp [twoPowT] - | succ n ih => - rw [List.replicate_succ, Transducer.run_cons, ih] - simp [twoPowT, List.replicate_succ] - /-- The value of a word, in linear space. -/ theorem ofBits_inSpace : ComputableInSpace ofBits encBits encNat fun l => (encBits l).length := of_inO ComputableInO.bitsToNat @@ -720,7 +613,7 @@ theorem paramEdge_inSpace : ComputableInSpace have he := edgeWithSymbol_budget ntm hB hn hvalU hvalV hsym hin have hb := bad_budget (k := k) (State := State) hB hn hvalU hin have hall := budget_comp_linear (transducer_inSpace (encIn := encBits) (encOut := encBool) - (f := fun l : List Bool => l.all id) allT fun l => by rw [allT_run]; rfl) hv + (f := fun l : List Bool => l.all id) Savitch.allT fun l => by rw [Savitch.allT_run]; rfl) hv exact (budget_finite (fun p : Bool × Bool × Bool => p.1 || (p.2.1 && p.2.2)) (budget_prod he (budget_prod hb hall))).of_enc_eq fun _ => rfl @@ -753,8 +646,11 @@ theorem initRound_inSpace (D : ℕ) : ComputableInSpace (initRound ntm D) encNat have hW : ComputableInSpace (fun n => width k (radix D n)) encNat encUnary fun n => (encNat n).length := hW₀.of_enc_eq fun _ => rfl have hstart := startID_budget ntm hB hin - have hpow := budget_comp_linear (transducer_inSpace (encIn := encUnary) (encOut := encNat) - (f := fun W => 2 ^ W) twoPowT fun W => (twoPowT_run W).symm) hW + have hpow₀ : ComputableInSpace (fun W : ℕ => 2 ^ W) encUnary encNat + fun W => (encUnary W).length := by + simpa only [encUnary_apply, List.length_replicate] using + of_inO (ComputableInDegree.two_pow_length encUnary).inO_one + have hpow := budget_comp_linear hpow₀ hW have hbits : ComputableInSpace (fun n => (startID ntm (radix D n) + 2 ^ width k (radix D n)).bits) encNat encBits fun n => (encNat n).length := diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean index 0418d771b..446b9db5f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean @@ -149,7 +149,7 @@ private theorem next_eq (u : List Bool) : /-- The transducer testing whether all bits are ones. -/ @[simps q₀ step final] -private def allT : Transducer Bool Bool where +def allT : Transducer Bool Bool where q₀ := true step a b := (a && b, []) final a := [a] @@ -157,7 +157,7 @@ private def allT : Transducer Bool Bool where length_final_le _ := by simp /-- The transducer `allT` tests whether all bits are ones. -/ -private theorem allT_run (a : Bool) (u : List Bool) : allT.run a u = [a && u.all id] := by +theorem allT_run (a : Bool) (u : List Bool) : allT.run a u = [a && u.all id] := by induction u generalizing a with | nil => simp [allT_final] | cons b u ih => simp [allT_step, ih, Bool.and_assoc] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean index 25e5fe08c..a6da6f30d 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean @@ -22,10 +22,13 @@ complexity certificates. Trailing false symbols are ignored, and the empty word ## Main definitions * `Turing.MultiTapeTM.ofBits`: read little-endian digits as a natural number. +* `Turing.MultiTapeTM.bitsOfWidth`: the word of a fixed width with a given value. ## Main results * `Turing.MultiTapeTM.bits_ofBits`: normalize a word by removing its trailing false symbols. +* `Turing.MultiTapeTM.ofBits_bitsOfWidth`, `Turing.MultiTapeTM.bits_add_two_pow`: the word of + width `W` with value `x < 2 ^ W`, and the binary digits of `x + 2 ^ W`. -/ @[expose] public section @@ -50,4 +53,58 @@ theorem bits_ofBits (w : List Bool) : (ofBits w).bits = w.rdropWhile (!·) := by · simp only [Nat.bits_eq_nil_iff, h₀, ↓reduceIte] rfl +/-- The word of width `W` with value `x`, for `x < 2 ^ W`: its binary digits, least significant +first, padded to width `W`. -/ +def bitsOfWidth : ℕ → ℕ → List Bool + | 0, _ => [] + | W + 1, x => x.bodd :: bitsOfWidth W x.div2 + +/-- The word `bitsOfWidth W x` has width `W`. -/ +theorem length_bitsOfWidth (W x : ℕ) : (bitsOfWidth W x).length = W := by + induction W generalizing x with + | zero => rfl + | succ W ih => simp [bitsOfWidth, ih] + +/-- The value of a word, one digit at a time. -/ +theorem ofBits_cons (b : Bool) (u : List Bool) : ofBits (b :: u) = Nat.bit b (ofBits u) := rfl + +/-- The word `bitsOfWidth W x` has value `x`, for `x < 2 ^ W`. -/ +theorem ofBits_bitsOfWidth {W x : ℕ} (hx : x < 2 ^ W) : ofBits (bitsOfWidth W x) = x := by + induction W generalizing x with + | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; rfl + | succ W ih => + rw [bitsOfWidth, ofBits_cons, ih (by rw [Nat.div2_val]; rw [pow_succ] at hx; omega), + Nat.bit_bodd_div2] + +/-- The binary digits of `x + 2 ^ W`, for `x < 2 ^ W`, are the word of width `W` with value `x`, +followed by a one. -/ +theorem bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : + (x + 2 ^ W).bits = bitsOfWidth W x ++ [true] := by + induction W generalizing x with + | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; simp [bitsOfWidth] + | succ W ih => + have hx' : x.div2 < 2 ^ W := by rw [Nat.div2_val]; rw [pow_succ] at hx; omega + have hbit : x + 2 ^ (W + 1) = Nat.bit x.bodd (x.div2 + 2 ^ W) := by + conv_lhs => rw [← Nat.bit_bodd_div2 x] + rw [Nat.bit_val, Nat.bit_val, pow_succ] + omega + rw [hbit, Nat.bits_append_bit _ _ fun h => by have := Nat.one_le_two_pow (n := W); omega, + ih hx', bitsOfWidth, List.cons_append] + +/-- The word of width `W` with value `x < 2 ^ W` is `(x + 2 ^ W).bits` without its last +digit. -/ +theorem dropLast_bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : + (x + 2 ^ W).bits.dropLast = bitsOfWidth W x := by + rw [bits_add_two_pow hx, List.dropLast_concat] + +/-- The word of `W` ones has value `2 ^ W - 1`. -/ +theorem ofBits_replicate_true (W : ℕ) : ofBits (List.replicate W true) = 2 ^ W - 1 := by + induction W with + | zero => rfl + | succ W ih => + rw [List.replicate_succ, ofBits_cons, ih, Nat.bit_val, pow_succ] + have := Nat.one_le_two_pow (n := W) + simp only [Bool.toNat_true] + omega + end Turing.MultiTapeTM diff --git a/ComplexityTests/LogSpaceSavitch.lean b/ComplexityTests/LogSpaceSavitch.lean index 0e4bee2d0..e573eb049 100644 --- a/ComplexityTests/LogSpaceSavitch.lean +++ b/ComplexityTests/LogSpaceSavitch.lean @@ -23,11 +23,11 @@ open Turing.MultiTapeNTM.ConfigurationGraph Turing.MultiTapeNTM.LogSquareSavitch /-! ### Words of a fixed width -/ -example : pad 4 5 = [true, false, true, false] := by decide -example : (5 + 2 ^ 4).bits.dropLast = pad 4 5 := by decide -example : ofBits (pad 6 37) = 37 := by decide +example : bitsOfWidth 4 5 = [true, false, true, false] := by decide +example : (5 + 2 ^ 4).bits.dropLast = bitsOfWidth 4 5 := by decide +example : ofBits (bitsOfWidth 6 37) = 37 := by decide example : ofBits (List.replicate 5 true) = 31 := by decide -example : (pad 3 0, pad 0 0) = ([false, false, false], []) := by decide +example : (bitsOfWidth 3 0, bitsOfWidth 0 0) = ([false, false, false], []) := by decide /-! ### A machine accepting every input -/ @@ -58,7 +58,7 @@ example (w : List Bool) : Cslib.Reachability.reach (inputEdge acceptMachine (radix (radixExponent Unit 0) w.length) w) (width 0 (radix (radixExponent Unit 0) w.length)) (width 0 (radix (radixExponent Unit 0) w.length)) - (pad (width 0 (radix (radixExponent Unit 0) w.length)) + (bitsOfWidth (width 0 (radix (radixExponent Unit 0) w.length)) (startID acceptMachine (radix (radixExponent Unit 0) w.length))) (List.replicate (width 0 (radix (radixExponent Unit 0) w.length)) true) = true := (reach_eq_true_iff (MultiTapeNTM.runsInSpace_zero_tapes _ _ _)).mpr (accepts_acceptMachine w) From 474c4183f6a9395e5866522fef5841efd4f53345 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 22:35:59 +0000 Subject: [PATCH 4/6] refactor(LogSpace): reuse lowBits and existing word certificates in log-squared Savitch (#474) Address the delta review of #1671: - the fixed-width words are `Cslib.BitString.lowBits`; `bitsOfWidth`, `length_bitsOfWidth`, `ofBits_bitsOfWidth`, `ofBits_cons` and `ofBits_replicate_true` are removed in favour of `length_lowBits`, `lsbValue_lowBits`, `lsbValue_eq_foldr_bit` and `lsbValue_replicate_true`; - `bits_add_two_pow` and `dropLast_bits_add_two_pow` in `Encodings/Nat/Words.lean` are stated with `lowBits`, proved from `Nat.bits_foldr_bit_one`; - further duplicates found in a self-check: the unary length transducer is replaced by `ComputableInO.lengthUnary`, and the local `budget_some` by `ComputableInDegree.optionSome`. Co-Authored-By: Claude Opus 5.5 --- .../Complexity/LogSpace/Savitch.lean | 79 +++++++++---------- .../Turing/MultiTape/Encodings/Nat/Words.lean | 71 +++++------------ ComplexityTests/LogSpaceSavitch.lean | 12 +-- 3 files changed, 64 insertions(+), 98 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean index 5a051e943..07a313a40 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean @@ -19,6 +19,8 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeOptionP import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative import Complexity.Foundations.Data.BitString.ShortWords +import Complexity.Foundations.Data.BitString.Binary +import Complexity.Foundations.Data.BitString.Counter import Mathlib.Data.Nat.Size import Mathlib.Tactic.Linarith @@ -69,9 +71,16 @@ decides whether the sink is reachable from the start vertex, that is, whether th namespace Turing.MultiTapeNTM.LogSquareSavitch open MultiTapeTM ConfigurationGraph Cslib.Reachability Cslib.Reachability.Savitch +open Cslib.BitString (lowBits length_lowBits lsbValue_lowBits lsbValue_eq_foldr_bit + lsbValue_replicate_true) /-! ### The graph on words -/ +/-- The value of the `W` low-order digits of `x < 2 ^ W` is `x`. -/ +private theorem ofBits_lowBits {W x : ℕ} (hx : x < 2 ^ W) : + ofBits (lowBits W x) = x := + (lsbValue_eq_foldr_bit _).symm.trans (lsbValue_lowBits hx) + variable {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State) variable (k) in @@ -109,8 +118,10 @@ theorem vertexBound_lt_two_pow_width (B : ℕ) : vertexBound (k := k) B < 2 ^ wi /-- No vertex is the sink. -/ theorem vertexBound_le_ofBits_sink (B : ℕ) : vertexBound (k := k) B ≤ ofBits (List.replicate (width k B) true) := by - rw [ofBits_replicate_true] + have h := lsbValue_replicate_true (width k B) + rw [lsbValue_eq_foldr_bit] at h have := vertexBound_lt_two_pow_width k B + change _ ≤ (List.replicate _ true).foldr Nat.bit 0 omega /-- **The sink is reachable exactly when an accepting halted vertex is.** Along the graph on words @@ -118,18 +129,18 @@ of width `W = width k B`, from the start vertex to the word of `W` ones. -/ theorem reflTransGen_sink_iff (hstart : startID ntm B < vertexBound (k := k) B) : Relation.ReflTransGen (fun a b => a.length = width k B ∧ b.length = width k B ∧ inputEdge ntm B w a b = true) - (bitsOfWidth (width k B) (startID ntm B)) (List.replicate (width k B) true) ↔ + (lowBits (width k B) (startID ntm B)) (List.replicate (width k B) true) ↔ ∃ u, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ∧ bad (k := k) (State := State) B w.length u = true := by have hW := vertexBound_lt_two_pow_width k B have hsink := vertexBound_le_ofBits_sink (k := k) B set W := width k B - have hsrc : ofBits (bitsOfWidth W (startID ntm B)) = startID ntm B := - ofBits_bitsOfWidth (hstart.trans hW) + have hsrc : ofBits (lowBits W (startID ntm B)) = startID ntm B := + ofBits_lowBits (hstart.trans hW) constructor · intro h have key : ∀ x, Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ - inputEdge ntm B w a b = true) (bitsOfWidth W (startID ntm B)) x → + inputEdge ntm B w a b = true) (lowBits W (startID ntm B)) x → (∃ u, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) u ∧ bad (k := k) (State := State) B w.length u = true) ∨ (Relation.ReflTransGen (Edge ntm B w) (startID ntm B) (ofBits x) ∧ @@ -157,23 +168,23 @@ theorem reflTransGen_sink_iff (hstart : startID ntm B < vertexBound (k := k) B) · rintro ⟨u, hu, hb⟩ have key : ∀ x, Relation.ReflTransGen (Edge ntm B w) (startID ntm B) x → Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ - inputEdge ntm B w a b = true) (bitsOfWidth W (startID ntm B)) (bitsOfWidth W x) ∧ + inputEdge ntm B w a b = true) (lowBits W (startID ntm B)) (lowBits W x) ∧ x < vertexBound (k := k) B := by intro x hx induction hx with | refl => exact ⟨.refl, hstart⟩ | @tail a b _ hab ih => have hlt := lt_vertexBound_of_edgeWithSymbol hab - refine ⟨ih.1.tail ⟨length_bitsOfWidth _ _, length_bitsOfWidth _ _, ?_⟩, hlt.2⟩ - simp only [inputEdge, wordEdge, ofBits_bitsOfWidth (hlt.1.trans hW), - ofBits_bitsOfWidth (hlt.2.trans hW)] + refine ⟨ih.1.tail ⟨length_lowBits _ _, length_lowBits _ _, ?_⟩, hlt.2⟩ + simp only [inputEdge, wordEdge, ofBits_lowBits (hlt.1.trans hW), + ofBits_lowBits (hlt.2.trans hW)] rw [show edgeWithSymbol ntm B w.length a b w[queryIndex (k := k) B a]? = true from hab, Bool.true_or] have hu' : u < vertexBound (k := k) B := by simp only [bad, Bool.and_eq_true] at hb exact lt_vertexBound_of_valid hb.1.1 - refine (key u hu).1.tail ⟨length_bitsOfWidth _ _, List.length_replicate, ?_⟩ - simp only [inputEdge, wordEdge, ofBits_bitsOfWidth (hu'.trans hW), hb, Bool.true_and, + refine (key u hu).1.tail ⟨length_lowBits _ _, List.length_replicate, ?_⟩ + simp only [inputEdge, wordEdge, ofBits_lowBits (hu'.trans hW), hb, Bool.true_and, Bool.or_eq_true] exact .inr (by simp) @@ -184,7 +195,7 @@ theorem reach_eq_true_iff {c : ℕ} (hs : ntm.RunsInSpace w (c * (Nat.log2 w.len reach (inputEdge ntm (radix (radixExponent State c) w.length) w) (width k (radix (radixExponent State c) w.length)) (width k (radix (radixExponent State c) w.length)) - (bitsOfWidth (width k (radix (radixExponent State c) w.length)) + (lowBits (width k (radix (radixExponent State c) w.length)) (startID ntm (radix (radixExponent State c) w.length))) (List.replicate (width k (radix (radixExponent State c) w.length)) true) = true ↔ ntm.Accepts w := by @@ -193,9 +204,9 @@ theorem reach_eq_true_iff {c : ℕ} (hs : ntm.RunsInSpace w (c * (Nat.log2 w.len have hstart : startID ntm B < vertexBound (k := k) B := by rw [← vertexID_init ntm B w] exact vertexID_lt (fits_of_runsInSpace c hs .refl) - have hsrc : (bitsOfWidth W (startID ntm B)).length = W := length_bitsOfWidth _ _ + have hsrc : (lowBits W (startID ntm B)).length = W := length_lowBits _ _ have hcard : {x | Relation.ReflTransGen (fun a b => a.length = W ∧ b.length = W ∧ - inputEdge ntm B w a b = true) (bitsOfWidth W (startID ntm B)) x}.encard ≤ 2 ^ W + 1 := by + inputEdge ntm B w a b = true) (lowBits W (startID ntm B)) x}.encard ≤ 2 ^ W + 1 := by refine (Set.encard_le_encard fun x hx => ?_).trans ((Cslib.BitString.encard_setOf_length_eq _).le.trans le_self_add) induction hx with @@ -361,7 +372,7 @@ variable {ntm} {D : ℕ} {w : List Bool} /-- The first round, once the start vertex is known to have a word. -/ theorem initRound_snd (hstart : startID ntm (radix D w.length) < 2 ^ width k (radix D w.length)) : (initRound ntm D w.length).2 = ⟨[], .call (width k (radix D w.length)) - (bitsOfWidth (width k (radix D w.length)) (startID ntm (radix D w.length))) + (lowBits (width k (radix D w.length)) (startID ntm (radix D w.length))) (List.replicate (width k (radix D w.length)) true)⟩ := by rw [initRound, dropLast_bits_add_two_pow hstart] @@ -371,11 +382,11 @@ theorem exists_halted (hstart : startID ntm (radix D w.length) < 2 ^ width k (ra finish ((machine ntm D).run w t) = [reach (inputEdge ntm (radix D w.length) w) (width k (radix D w.length)) (width k (radix D w.length)) - (bitsOfWidth (width k (radix D w.length)) (startID ntm (radix D w.length))) + (lowBits (width k (radix D w.length)) (startID ntm (radix D w.length))) (List.replicate (width k (radix D w.length)) true)] := by obtain ⟨T, -, hT⟩ := exists_iterate_step_call (edge := inputEdge ntm (radix D w.length) w) (w := width k (radix D w.length)) (width k (radix D w.length)) - (bitsOfWidth (width k (radix D w.length)) (startID ntm (radix D w.length))) + (lowBits (width k (radix D w.length)) (startID ntm (radix D w.length))) (List.replicate (width k (radix D w.length)) true) [] obtain ⟨symbol, h⟩ := exists_run_add (ntm := ntm) (D := D) w T refine ⟨w.length + 1 + T, ?_⟩ @@ -392,7 +403,7 @@ theorem invariant_iterate_initRound rw [initRound_snd hstart] refine ⟨trivial, fun i u v h => ?_⟩ obtain ⟨rfl, rfl, rfl⟩ := Reg.call.inj h - exact ⟨by simp, length_bitsOfWidth _ _, List.length_replicate⟩ + exact ⟨by simp, length_lowBits _ _, List.length_replicate⟩ /-- The binary length of the radix `(n + 2) ^ D`. -/ theorem length_encNat_radix_le (D n : ℕ) : @@ -491,19 +502,10 @@ theorem isSome_inSpace {β : Type} (e : β ↪ List Bool) : fun o => (encOption e o).length := of_inO (ComputableInDegree.isSome e).inO_one -/-- The length of a word in unary, as a transducer. -/ -def unaryT : Transducer Bool Unit where - q₀ := () - step _ _ := ((), [true]) - final _ := [] - length_step_le _ _ := by simp - length_final_le _ := by simp - -/-- `unaryT` emits the length of its input in unary. -/ -theorem unaryT_run (l : List Bool) : unaryT.run () l = List.replicate l.length true := by - induction l with - | nil => simp [unaryT] - | cons a l ih => rw [Transducer.run_cons, ih]; simp [unaryT, List.replicate_succ] +/-- The binary length of a number, in unary, in linear space. -/ +theorem size_inSpace : ComputableInSpace Nat.size encNat encUnary fun x => (encNat x).length := + ((of_inO ComputableInO.lengthUnary).of_encIn_eq Nat.bits fun _ => rfl).of_enc_eq fun x => by + rw [Nat.size_eq_bits_len] /-- The value of a word, in linear space. -/ theorem ofBits_inSpace : ComputableInSpace ofBits encBits encNat fun l => (encBits l).length := @@ -511,13 +513,6 @@ theorem ofBits_inSpace : ComputableInSpace ofBits encBits encNat fun l => (encBi variable {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} -/-- `Option.some`, within a budget. -/ -theorem budget_some {β : Type} {e : β ↪ List Bool} {f : α → β} - (hf : ComputableInSpace f enc e S) (hin : (fun a => (enc a).length) ≼ S) : - ComputableInSpace (fun a => some (f a)) enc (encOption e) S := - ((budget_const (encB := encBool) true hin).append hf fun _ => rfl).weaken - (.add (.refl _) (.refl _)) - /-- The fields of a state of the recursion, as pairs. -/ theorem stateFields_inSpace : ComputableInSpace (fun st : Savitch.State => (st.stack, st.reg.toPair)) encState @@ -640,9 +635,7 @@ theorem initRound_inSpace (D : ℕ) : ComputableInSpace (initRound ntm D) encNat have hB : ComputableInSpace (fun n => radix D n) encNat encNat fun n => (encNat n).length := (budget_natPow (budget_natAdd hn (budget_const 2 hin)) hin D).of_enc_eq fun _ => rfl have hN := vertexBound_budget (k := k) hB hin - have hW₀ := budget_comp_linear (transducer_inSpace (encIn := encNat) (encOut := encUnary) - (f := Nat.size) unaryT fun x => by - rw [unaryT_run, encUnary_apply, encNat_apply, Nat.size_eq_bits_len]) hN + have hW₀ := budget_comp_linear size_inSpace hN have hW : ComputableInSpace (fun n => width k (radix D n)) encNat encUnary fun n => (encNat n).length := hW₀.of_enc_eq fun _ => rfl have hstart := startID_budget ntm hB hin @@ -658,7 +651,9 @@ theorem initRound_inSpace (D : ℕ) : ComputableInSpace (initRound ntm D) encNat have hsrc := budget_comp_linear (of_inO ComputableInDegree.bitsDropLast.inO_one) hbits have hsink : ComputableInSpace (fun n => List.replicate (width k (radix D n)) true) encNat encBits fun n => (encNat n).length := hW.of_enc_eq fun _ => rfl - have hcall := budget_some (e := encCall) (budget_prod hW (budget_prod hsrc hsink)) hin + have hcall := budget_comp_linear + (of_inO (ComputableInDegree.optionSome (enc₁ := encCall) (enc := encOption encCall)).inO_one) + (budget_prod hW (budget_prod hsrc hsink)) have hstate : ComputableInSpace (fun n => (initRound ntm D n).2) encNat encState fun n => (encNat n).length := (budget_prod (budget_const (encB := encList encFrame) [] hin) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean index a6da6f30d..ce5f5d95f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Words.lean @@ -9,6 +9,9 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits public import Mathlib.Data.List.DropRight +public import Complexity.Foundations.Data.BitString.List.Binary +import Complexity.Foundations.Data.BitString.Binary +import Complexity.Foundations.Data.BitString.Counter import Complexity.Foundations.Data.List.Append import Complexity.Foundations.Data.Nat.Bits import Mathlib.Data.Nat.Size @@ -22,13 +25,12 @@ complexity certificates. Trailing false symbols are ignored, and the empty word ## Main definitions * `Turing.MultiTapeTM.ofBits`: read little-endian digits as a natural number. -* `Turing.MultiTapeTM.bitsOfWidth`: the word of a fixed width with a given value. ## Main results * `Turing.MultiTapeTM.bits_ofBits`: normalize a word by removing its trailing false symbols. -* `Turing.MultiTapeTM.ofBits_bitsOfWidth`, `Turing.MultiTapeTM.bits_add_two_pow`: the word of - width `W` with value `x < 2 ^ W`, and the binary digits of `x + 2 ^ W`. +* `Turing.MultiTapeTM.bits_add_two_pow`: the binary digits of `x + 2 ^ W`, for `x < 2 ^ W`, are + the `W` low-order digits of `x` (`Cslib.BitString.lowBits`) followed by a one. -/ @[expose] public section @@ -53,58 +55,27 @@ theorem bits_ofBits (w : List Bool) : (ofBits w).bits = w.rdropWhile (!·) := by · simp only [Nat.bits_eq_nil_iff, h₀, ↓reduceIte] rfl -/-- The word of width `W` with value `x`, for `x < 2 ^ W`: its binary digits, least significant -first, padded to width `W`. -/ -def bitsOfWidth : ℕ → ℕ → List Bool - | 0, _ => [] - | W + 1, x => x.bodd :: bitsOfWidth W x.div2 - -/-- The word `bitsOfWidth W x` has width `W`. -/ -theorem length_bitsOfWidth (W x : ℕ) : (bitsOfWidth W x).length = W := by - induction W generalizing x with - | zero => rfl - | succ W ih => simp [bitsOfWidth, ih] - -/-- The value of a word, one digit at a time. -/ -theorem ofBits_cons (b : Bool) (u : List Bool) : ofBits (b :: u) = Nat.bit b (ofBits u) := rfl - -/-- The word `bitsOfWidth W x` has value `x`, for `x < 2 ^ W`. -/ -theorem ofBits_bitsOfWidth {W x : ℕ} (hx : x < 2 ^ W) : ofBits (bitsOfWidth W x) = x := by - induction W generalizing x with - | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; rfl - | succ W ih => - rw [bitsOfWidth, ofBits_cons, ih (by rw [Nat.div2_val]; rw [pow_succ] at hx; omega), - Nat.bit_bodd_div2] +/-- A trailing one adds `2 ^ |w|` to the value of a word. -/ +private theorem foldr_bit_one_eq (w : List Bool) : + w.foldr Nat.bit 1 = w.foldr Nat.bit 0 + 2 ^ w.length := by + induction w with + | nil => rfl + | cons b w ih => + rw [List.foldr_cons, List.foldr_cons, ih, Nat.bit_val, Nat.bit_val, List.length_cons, pow_succ] + omega -/-- The binary digits of `x + 2 ^ W`, for `x < 2 ^ W`, are the word of width `W` with value `x`, +/-- The binary digits of `x + 2 ^ W`, for `x < 2 ^ W`, are the `W` low-order digits of `x`, followed by a one. -/ theorem bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : - (x + 2 ^ W).bits = bitsOfWidth W x ++ [true] := by - induction W generalizing x with - | zero => simp only [pow_zero, Nat.lt_one_iff] at hx; subst hx; simp [bitsOfWidth] - | succ W ih => - have hx' : x.div2 < 2 ^ W := by rw [Nat.div2_val]; rw [pow_succ] at hx; omega - have hbit : x + 2 ^ (W + 1) = Nat.bit x.bodd (x.div2 + 2 ^ W) := by - conv_lhs => rw [← Nat.bit_bodd_div2 x] - rw [Nat.bit_val, Nat.bit_val, pow_succ] - omega - rw [hbit, Nat.bits_append_bit _ _ fun h => by have := Nat.one_le_two_pow (n := W); omega, - ih hx', bitsOfWidth, List.cons_append] + (x + 2 ^ W).bits = Cslib.BitString.lowBits W x ++ [true] := by + have h := foldr_bit_one_eq (Cslib.BitString.lowBits W x) + rw [← Cslib.BitString.lsbValue_eq_foldr_bit, Cslib.BitString.lsbValue_lowBits hx, + Cslib.BitString.length_lowBits] at h + rw [← h, Nat.bits_foldr_bit_one] -/-- The word of width `W` with value `x < 2 ^ W` is `(x + 2 ^ W).bits` without its last -digit. -/ +/-- The `W` low-order digits of `x < 2 ^ W` are `(x + 2 ^ W).bits` without its last digit. -/ theorem dropLast_bits_add_two_pow {W x : ℕ} (hx : x < 2 ^ W) : - (x + 2 ^ W).bits.dropLast = bitsOfWidth W x := by + (x + 2 ^ W).bits.dropLast = Cslib.BitString.lowBits W x := by rw [bits_add_two_pow hx, List.dropLast_concat] -/-- The word of `W` ones has value `2 ^ W - 1`. -/ -theorem ofBits_replicate_true (W : ℕ) : ofBits (List.replicate W true) = 2 ^ W - 1 := by - induction W with - | zero => rfl - | succ W ih => - rw [List.replicate_succ, ofBits_cons, ih, Nat.bit_val, pow_succ] - have := Nat.one_le_two_pow (n := W) - simp only [Bool.toNat_true] - omega - end Turing.MultiTapeTM diff --git a/ComplexityTests/LogSpaceSavitch.lean b/ComplexityTests/LogSpaceSavitch.lean index e573eb049..d3a96237b 100644 --- a/ComplexityTests/LogSpaceSavitch.lean +++ b/ComplexityTests/LogSpaceSavitch.lean @@ -20,14 +20,14 @@ namespace ComplexityTests.LogSpaceSavitch open Cslib.Turing Turing Turing.MultiTapeTM Cslib.Complexity open Turing.MultiTapeNTM.ConfigurationGraph Turing.MultiTapeNTM.LogSquareSavitch +open Cslib.BitString (lowBits) /-! ### Words of a fixed width -/ -example : bitsOfWidth 4 5 = [true, false, true, false] := by decide -example : (5 + 2 ^ 4).bits.dropLast = bitsOfWidth 4 5 := by decide -example : ofBits (bitsOfWidth 6 37) = 37 := by decide -example : ofBits (List.replicate 5 true) = 31 := by decide -example : (bitsOfWidth 3 0, bitsOfWidth 0 0) = ([false, false, false], []) := by decide +example : lowBits 4 5 = [true, false, true, false] := by decide +example : (5 + 2 ^ 4).bits.dropLast = lowBits 4 5 := by decide +example : ofBits (lowBits 6 37) = 37 := by decide +example : (lowBits 3 0, lowBits 0 0) = ([false, false, false], []) := by decide /-! ### A machine accepting every input -/ @@ -58,7 +58,7 @@ example (w : List Bool) : Cslib.Reachability.reach (inputEdge acceptMachine (radix (radixExponent Unit 0) w.length) w) (width 0 (radix (radixExponent Unit 0) w.length)) (width 0 (radix (radixExponent Unit 0) w.length)) - (bitsOfWidth (width 0 (radix (radixExponent Unit 0) w.length)) + (lowBits (width 0 (radix (radixExponent Unit 0) w.length)) (startID acceptMachine (radix (radixExponent Unit 0) w.length))) (List.replicate (width 0 (radix (radixExponent Unit 0) w.length)) true) = true := (reach_eq_true_iff (MultiTapeNTM.runsInSpace_zero_tapes _ _ _)).mpr (accepts_acceptMachine w) From 3e0c03adda136d87d886fcbb72f93e37d9d80113 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:46:58 +0000 Subject: [PATCH 5/6] docs(LogSpace): cite Sipser's sublinear extension of Savitch's theorem (#474) Theorem 8.5 assumes f(n) >= n. The sublinear statement is the final paragraph of Section 8.4 (3rd ed., p. 351). Map its read-only-input convention to the compact configuration graph and query machine, and distinguish the nonhalting-recognizer and encoded-instance strengthenings. Co-Authored-By: Claude Opus 5.5 --- .../Complexity/Classes/LogSpace/Savitch.lean | 9 ++++++++- .../MultiTape/Complexity/LogSpace/Savitch.lean | 15 ++++++++++++++- 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean index 3946b387e..9fda4f180 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean @@ -24,6 +24,12 @@ same bound holds for `Cslib.Complexity.RL` [Hoza, Section 4.3][Hoza2022]. The space classes are `Cslib.Complexity.DSPACE enc fun n => Nat.log2 n ^ 2`, the problems decided within space `c₁ * (log₂ n) ^ 2 + c₂` on encoded instances of length `n`. +The source statement for sublinear space is the extension in the final paragraph of Sipser's +Section 8.4 (3rd edition, p. 351), "We can extend Savitch's theorem to hold for sublinear space +bounds down to f(n) ≥ log n"; Sipser's Theorem 8.5 assumes `f(n) ≥ n`. The source is about +deciders on strings; the statements here also cover nonhalting recognizers and arbitrary encoded +instances. + ## Main results * `Cslib.Complexity.mem_DSPACE_log2_sq_of_recognizesInSpace`: a logspace recognizer, whose @@ -36,7 +42,8 @@ within space `c₁ * (log₂ n) ^ 2 + c₂` on encoded instances of length `n`. * [W. J. Savitch, *Relationships between nondeterministic and deterministic tape complexities*][Savitch1970] * [W. M. Hoza, *Recent Progress on Derandomizing Space-Bounded Computation*, Section 4.3][Hoza2022] -* [M. Sipser, *Introduction to the Theory of Computation*, Theorem 8.5][Sipser2013] +* [M. Sipser, *Introduction to the Theory of Computation*, 3rd edition, Section 8.4, final + paragraph (p. 351)][Sipser2013] -/ @[expose] public section diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean index 07a313a40..b3e8c5233 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Savitch.lean @@ -43,6 +43,18 @@ word of `W` ones: every accepting halted vertex steps to it. The recursion at de decides whether the sink is reachable from the start vertex, that is, whether the machine accepts (`Turing.MultiTapeNTM.LogSquareSavitch.reach_eq_true_iff`). +The sublinear form of Savitch's theorem is the extension stated in the final paragraph of +Section 8.4 of Sipser's third edition, just before Section 8.5 (p. 351): "We can extend Savitch's +theorem to hold for sublinear space bounds down to f(n) ≥ log n." Sipser's Theorem 8.5 itself +assumes `f(n) ≥ n`. In the extension, the machine has a read-only input tape, and the +configurations of the machine on the input `w` record the state, the work tapes and the head +positions but not `w`. Here these are the vertices of the compact configuration graph, which omit +the input, and the query machine reads the one input bit an edge test needs. The source states +the theorem for every `f(n) ≥ log n` and for languages decided by nondeterministic machines whose +branches all halt; this file proves only the case `f(n) = c * (log₂ n + 1)`, but for machines that +only recognize the problem (branches may run forever), on arbitrary instances under an encoding +into `List Bool`. + ## Main definitions * `Turing.MultiTapeNTM.LogSquareSavitch.wordEdge`: the edges of the graph on words, given the @@ -63,7 +75,8 @@ decides whether the sink is reachable from the start vertex, that is, whether th * [W. J. Savitch, *Relationships between nondeterministic and deterministic tape complexities*][Savitch1970] -* [M. Sipser, *Introduction to the Theory of Computation*, Theorem 8.5][Sipser2013] +* [M. Sipser, *Introduction to the Theory of Computation*, 3rd edition, Section 8.4, final + paragraph (p. 351)][Sipser2013] -/ @[expose] public section From d81ad0308e9ecc8ec873030579ab5a82c0dd4fee Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 12:10:19 -0400 Subject: [PATCH 6/6] chore: regenerate Savitch aggregate import order Apply the actual mk_all output after integration. Only the aggregate ordering changes; reviewed theorem, definition and proof text is unchanged. AI assistance: Codex coordinator /root. --- Complexity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Complexity.lean b/Complexity.lean index 40f5f0fc4..71d79531d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1066,9 +1066,9 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Tr public import Complexity.Computability.Complexity.Classes.LogSpace.PolyTime public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification -public import Complexity.Computability.Complexity.Classes.LogSpace.Savitch public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.BPP public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix +public import Complexity.Computability.Complexity.Classes.LogSpace.Savitch public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON public import Complexity.Computability.Complexity.Classes.MIP public import Complexity.Computability.Complexity.Classes.MIP.Defs