Skip to content

refactor(Machines): plain polynomial-time tape, configuration and breadth-first search rules #1670

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 3 commits into from
Oct 30, 2026
Merged

refactor(Machines): plain polynomial-time tape, configuration and breadth-first search rules #1670

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
975c93f
refactor(Machines): plain polynomial-time tape, configuration and NL …
chris-ai1 Oct 29, 2026
a2e6884
chore(Machines): compose reviewed plain-space tidy baselines
Oct 30, 2026
b7c7835
style(Machines): use canonical tidy-baseline serialization
Oct 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
79 changes: 39 additions & 40 deletions Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ configuration graph, which has polynomially many vertices [Sipser, Section 8.4][

* `Turing.MultiTapeNTM.reflTransGen_viewSucc_iff`: the successor lists give the reachable views.
* `Turing.MultiTapeNTM.searchAccepts_iff`: enough rounds decide acceptance.
* `Turing.MultiTapeNTM.computableTidilyInPolyTime_viewSucc`: the successors in polynomial time.
* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.expand`: a round in polynomial time.
* `Turing.MultiTapeNTM.computableInPolyTime_viewSucc`: the successors in polynomial time.
* `Turing.MultiTapeTM.ComputableInPolyTime.expand`: a round in polynomial time.
* `Turing.MultiTapeNTM.exists_computableInPolyTime_searchAccepts`: under a logarithmic space
bound, enough rounds of breadth-first search run in polynomial time.

Expand Down Expand Up @@ -133,12 +133,12 @@ end Turing.MultiTapeNTM

/-! ### Breadth-first search in polynomial time -/

namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime
namespace Turing.MultiTapeTM.ComputableInPolyTime

variable {α : Type} [DecidableEq α] {enc : α ↪ List Bool}

/-- Appending an element unless it is already in the list is polynomial-time. -/
theorem insertNew : ComputableTidilyInPolyTime
theorem insertNew : ComputableInPolyTime
(fun p : List α × α => Cslib.Reachability.insertNew p.1 p.2) (encPair (encList enc) enc)
(encList enc) := by
have hmem (l : List α) (a : α) : decide (a ∈ l) = l.any fun b => decide (b = a) := by
Expand All @@ -153,12 +153,12 @@ theorem insertNew : ComputableTidilyInPolyTime

/-- **A round of breadth-first search is polynomial-time** when the successors are: the found
elements and their successors are at most polynomially many and long. -/
theorem expand {succ : α → List α} (hsucc : ComputableTidilyInPolyTime succ enc (encList enc)) :
ComputableTidilyInPolyTime (Cslib.Reachability.expand succ) (encList enc) (encList enc) := by
have hlist : ComputableTidilyInPolyTime (fun found : List α => found.flatMap succ)
theorem expand {succ : α → List α} (hsucc : ComputableInPolyTime succ enc (encList enc)) :
ComputableInPolyTime (Cslib.Reachability.expand succ) (encList enc) (encList enc) := by
have hlist : ComputableInPolyTime (fun found : List α => found.flatMap succ)
(encList enc) (encList enc) :=
flatMapWithInput id' (hsucc.comp (snd _ _))
have hstep : ComputableTidilyInPolyTime
have hstep : ComputableInPolyTime
(fun p : (List α × List α) × α => Cslib.Reachability.insertNew p.1.2 p.2)
(encPair (encPair (encList enc) (encList enc)) enc) (encList enc) :=
insertNew.comp (((snd _ _).comp (fst _ _)).prod (snd _ _))
Expand All @@ -176,7 +176,7 @@ theorem expand {succ : α → List α} (hsucc : ComputableTidilyInPolyTime succ
length_frame]
omega

end Turing.MultiTapeTM.ComputableTidilyInPolyTime
end Turing.MultiTapeTM.ComputableInPolyTime

namespace Turing.MultiTapeNTM

Expand All @@ -185,8 +185,8 @@ open MultiTapeTM
variable {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State}

/-- **The successors of a view are polynomial-time.** -/
theorem computableTidilyInPolyTime_viewSucc :
ComputableTidilyInPolyTime ntm.viewSucc encFiniteCfg (encList encFiniteCfg) := by
theorem computableInPolyTime_viewSucc :
ComputableInPolyTime ntm.viewSucc encFiniteCfg (encList encFiniteCfg) := by
classical
let key (finite : FiniteCfg k Bool State) : Option State × Option Bool × (Fin k → Option Bool) :=
(finite.state, finite.inputSymbol, finite.workTapeSymbols)
Expand All @@ -200,16 +200,16 @@ theorem computableTidilyInPolyTime_viewSucc :
funext finite
rfl
rw [heq]
refine ComputableTidilyInPolyTime.finite_cases
refine ComputableInPolyTime.finite_cases
(tagEncoding := encPair (encFinite _) (encPair (encFinEnum _) (encFinEnum _))) ?_ fun tag => ?_
· exact ComputableTidilyInPolyTime.finiteCfg_state.prod
(ComputableTidilyInPolyTime.finiteCfg_inputSymbol.prod
ComputableTidilyInPolyTime.finiteCfg_workTapeSymbols)
· exact ComputableInPolyTime.finiteCfg_state.prod
(ComputableInPolyTime.finiteCfg_inputSymbol.prod
ComputableInPolyTime.finiteCfg_workTapeSymbols)
· rcases tag with ⟨_ | state, symbol, work⟩
· exact ComputableTidilyInPolyTime.const []
· exact ComputableTidilyInPolyTime.mapConst _ fun action _ =>
ComputableInPolyTime.finiteCfg_summarizeOutput.tidy.comp
(ComputableTidilyInPolyTime.finiteCfg_step action)
· exact ComputableInPolyTime.const []
· exact ComputableInPolyTime.mapConst _ fun action _ =>
ComputableInPolyTime.finiteCfg_summarizeOutput.comp
(ComputableInPolyTime.finiteCfg_step action)

/-- Under a logarithmic space bound, the number of rounds that decides acceptance is at most a
polynomial in the input length. -/
Expand Down Expand Up @@ -244,20 +244,19 @@ theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List
ComputableInPolyTime (fun a => ntm.searchAccepts (rounds a) (enc a)) enc encBool := by
set D := 2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)
set rounds : α → ℕ := fun a => 2 * 2 ^ D * ((enc a).length + 1) ^ D
refine ⟨rounds, fun a => rounds_le k State c _,
ComputableTidilyInPolyTime.computableInPolyTime ?_⟩
refine ⟨rounds, fun a => rounds_le k State c _, ?_⟩
-- the number of rounds in unary
have hcount : ComputableTidilyInPolyTime rounds enc encUnary :=
ComputableTidilyInPolyTime.unary_mul.comp ((ComputableTidilyInPolyTime.const _).prod
((ComputableTidilyInPolyTime.unary_pow D).comp (ComputableTidilyInPolyTime.unary_add.comp
((ComputableTidilyInPolyTime.encoding_length enc).prod
(ComputableTidilyInPolyTime.const 1)))))
have hinit : ComputableTidilyInPolyTime (fun a => [ntm.initView (enc a)]) enc
have hcount : ComputableInPolyTime rounds enc encUnary :=
ComputableInPolyTime.unary_mul.comp ((ComputableInPolyTime.const _).prod
((ComputableInPolyTime.unary_pow D).comp (ComputableInPolyTime.unary_add.comp
((ComputableInPolyTime.encoding_length enc).prod
(ComputableInPolyTime.const 1)))))
have hinit : ComputableInPolyTime (fun a => [ntm.initView (enc a)]) enc
(encList encFiniteCfg) :=
ComputableTidilyInPolyTime.cons' (ComputableTidilyInPolyTime.finiteCfg_init
(ComputableTidilyInPolyTime.of_eq (encIn := enc) (encMid := encBits) (f := fun a => enc a)
ComputableInPolyTime.cons' (ComputableInPolyTime.finiteCfg_init
(ComputableInPolyTime.of_eq (encIn := enc) (encOut := encBits) (f := fun a => enc a)
fun _ => rfl) ntm.q₀)
(ComputableTidilyInPolyTime.const [])
(ComputableInPolyTime.const [])
-- the found views are polynomially many, each of linear length
set bound : α → ℕ := fun a => rounds a *
(2 * viewLengthBound k State (enc a).length (c * (Nat.log2 (enc a).length + 1)) + 1)
Expand All @@ -282,17 +281,17 @@ theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List
refine (length_encList_le encFiniteCfg _ fun finite hf =>
length_encFiniteCfg_le (hs a) (hreach finite hf)).trans ?_
exact Nat.mul_le_mul_right _ hlen
have hsearch := ComputableTidilyInPolyTime.iterate hcount hinit
(ComputableTidilyInPolyTime.expand computableTidilyInPolyTime_viewSucc) hbound hstates
have htest : ComputableTidilyInPolyTime
have hsearch := ComputableInPolyTime.iterate hcount hinit
(ComputableInPolyTime.expand computableInPolyTime_viewSucc) hbound hstates
have htest : ComputableInPolyTime
(fun finite : FiniteCfg k Bool State =>
decide (finite.state = none) && decide (finite.output = [true])) encFiniteCfg encBool :=
ComputableTidilyInPolyTime.bool_and.comp
(((ComputableTidilyInPolyTime.of_finite fun state : Option State =>
decide (state = none)).comp ComputableTidilyInPolyTime.finiteCfg_state).prod
(ComputableTidilyInPolyTime.decide_eq' ComputableTidilyInPolyTime.finiteCfg_output
(ComputableTidilyInPolyTime.const [true])))
exact ComputableTidilyInPolyTime.anyWithInput hsearch
(htest.comp (ComputableTidilyInPolyTime.snd _ _))
ComputableInPolyTime.bool_and.comp
(((ComputableInPolyTime.of_finite fun state : Option State =>
decide (state = none)).comp ComputableInPolyTime.finiteCfg_state).prod
(ComputableInPolyTime.decide_eq' ComputableInPolyTime.finiteCfg_output
(ComputableInPolyTime.const [true])))
exact ComputableInPolyTime.anyWithInput hsearch
(htest.comp (ComputableInPolyTime.snd _ _))

end Turing.MultiTapeNTM
Loading
Loading