Paper
The Immerman–Szelepcsényi Theorem
3 pages · 25 marked passages · pdflatex · download PDF · lax-362205
-
Bounded reachability
A directed graph on vertices is given by its Boolean adjacency matrix. A walk may repeat vertices. The recursive reachability test divides the length bound in two and enumerates possible middle vertices.
1 import Mathlib.Data.List.FinRange 2 import Mathlib.Logic.Relation 3 4 set_option backward.isDefEq.respectTransparency false 5 6 /-! 7 --- 8 title: Bounded reachability 9 type: definition 10 --- 11 A directed graph on vertices is given by its Boolean adjacency matrix. 12 A walk may repeat vertices. The recursive reachability test divides the 13 length bound in two and enumerates possible middle vertices. 14 -/ 15 16 namespace Lax362205.Reachability 17 18 abbrev Graph (N : ℕ) := Fin N → Fin N → Bool 19 20 inductive Walk {α : Type} (R : α → α → Prop) : ℕ → α → α → Prop 21 | nil (a : α) : Walk R 0 a a 22 | tail {n : ℕ} {a b c : α} : Walk R n a b → R b c → Walk R (n + 1) a c 23 24 def Within {α : Type} (R : α → α → Prop) (n : ℕ) (a b : α) : Prop := 25 ∃ k ≤ n, Walk R k a b 26 27 def Reachable {N : ℕ} (G : Graph N) (a b : Fin N) : Prop := 28 Relation.ReflTransGen (fun u v => G u v = true) a b 29 30 def search {N : ℕ} (G : Graph N) : ℕ → Fin N → Fin N → Bool 31 | 0, a, b => decide (a = b) || G a b 32 | k + 1, a, b => (List.finRange N).any fun m => search G k a m && search G k m b 33 34 end Lax362205.Reachability 35 -
Bounded machine configurations
A configuration using at most work cells consists of a control state, an input-head position, a work-head position, and work symbols. Cells beyond this prefix are blank.
1 import Lax434930.SpaceMachines 2 import Mathlib.Data.Fintype.Pi 3 4 set_option backward.isDefEq.respectTransparency false 5 6 /-! 7 --- 8 title: Bounded machine configurations 9 type: definition 10 --- 11 A configuration using at most work cells consists of a control state, 12 an input-head position, a work-head position, and work symbols. 13 Cells beyond this prefix are blank. 14 -/ 15 16 namespace Lax362205.BoundedConfigurations 17 18 open Lax434930.SpaceMachines 19 20 structure Config (M : Machine) (n s : ℕ) where 21 state : M.Q 22 inputHead : Fin (n + 2) 23 workHead : Fin s 24 tape : Fin s → M.Γ 25 deriving Fintype 26 27 def expand {M : Machine} {n s : ℕ} (c : Config M n s) : M.Config := 28 ⟨c.state, c.inputHead.val, c.workHead.val, 29 fun i => if h : i < s then c.tape ⟨i, h⟩ else M.blank⟩ 30 31 end Lax362205.BoundedConfigurations 32 -
The bounded configuration graph
Vertices are configurations whose work tape has a fixed finite bound. Edges are machine transitions. Acceptance is reachability from the initial configuration to a terminal accepting configuration. The search predicate replaces reachability by the recursive finite graph test.
1 import Lax362205.BoundedConfigurations 2 import Lax362205.Reachability 3 import Mathlib.Data.Fintype.EquivFin 4 import Mathlib.Data.Nat.Log 5 6 set_option backward.isDefEq.respectTransparency false 7 8 /-! 9 --- 10 title: The bounded configuration graph 11 type: definition 12 --- 13 Vertices are configurations whose work tape has a fixed finite bound. 14 Edges are machine transitions. Acceptance is reachability from the initial 15 configuration to a terminal accepting configuration. The search predicate 16 replaces reachability by the recursive finite graph test. 17 -/ 18 19 namespace Lax362205.ConfigurationGraph 20 21 open scoped Classical 22 23 open Lax434930.PolynomialTime Lax434930.SpaceMachines BoundedConfigurations Reachability 24 25 /-- Label all bounded configurations consecutively from zero. -/ 26 noncomputable def numbering (M : Machine) (n s : ℕ) : 27 Config M n s ≃ Fin (Fintype.card (Config M n s)) := Fintype.equivFin _ 28 29 /-- Connect two numbered configurations exactly when the machine can move from the first to the second. -/ 30 noncomputable def graph (M : Machine) (w : Word) (s : ℕ) : 31 Graph (Fintype.card (Config M w.length s)) := 32 fun a b => decide (M.Step w (expand ((numbering M w.length s).symm a)) 33 (expand ((numbering M w.length s).symm b))) 34 35 /-- Some accepting terminal configuration is reachable from the initial configuration within the tape bound. -/ 36 def AcceptsBounded (M : Machine) (w : Word) (s : ℕ) : Prop := 37 ∃ a b : Config M w.length s, 38 expand a = M.initial ∧ M.Terminal w (expand b) ∧ M.accept b.state = true ∧ 39 Reachable (graph M w s) (numbering M w.length s a) (numbering M w.length s b) 40 41 /-- The finite reachability search finds a path from the initial configuration to an accepting terminal one. -/ 42 def SearchAccepts (M : Machine) (w : Word) (s : ℕ) : Prop := 43 ∃ a b : Config M w.length s, 44 expand a = M.initial ∧ M.Terminal w (expand b) ∧ M.accept b.state = true ∧ 45 search (graph M w s) (Nat.clog 2 (Fintype.card (Config M w.length s))) 46 (numbering M w.length s a) (numbering M w.length s b) = true 47 48 end Lax362205.ConfigurationGraph 49 -
Inductive counting certificates
The th reachable layer contains vertices at distance at most from the source. A census lists distinct reachable vertices and their path witnesses. Given the correct census size, a negative classification checks that no listed vertex has an edge to the target. A counting step classifies every vertex and counts the positive answers.
1 import Lax362205.Reachability 2 import Mathlib.Data.Fintype.Powerset 3 … module docstring, 11 lines 15 16 namespace Lax362205.Counting 17 18 open scoped Classical 19 20 open Lax362205.Reachability 21 22 /-- The vertices reachable from `a` using at most `k` directed edges. -/ 23 noncomputable def layer {N : ℕ} (G : Graph N) (a : Fin N) (k : ℕ) : Finset (Fin N) := 24 Finset.univ.filter (fun v => Within (fun u v => G u v = true) k a v) 25 26 /-- A set of `c` distinct vertices, each reachable within `k` steps. -/ 27 def Census {N : ℕ} (G : Graph N) (a : Fin N) (k c : ℕ) (S : Finset (Fin N)) : Prop := 28 S.card = c ∧ ∀ v ∈ S, Within (fun u v => G u v = true) k a v 29 30 /-- A positive answer supplies a path; a negative answer supplies a census that has no edge to `v`. -/ 31 def Classify {N : ℕ} (G : Graph N) (a : Fin N) (k c : ℕ) (v : Fin N) : Bool → Prop 32 | true => Within (fun u v => G u v = true) (k + 1) a v 33 | false => ∃ S, Census G a k c S ∧ v ≠ a ∧ ∀ u ∈ S, G u v = false 34 35 /-- Classify every vertex for the next layer and count exactly `d` positive answers. -/ 36 def CountStep {N : ℕ} (G : Graph N) (a : Fin N) (k c d : ℕ) : Prop := 37 ∃ answers : Fin N → Bool, (∀ v, Classify G a k c v (answers v)) ∧ 38 (Finset.univ.filter (fun v => answers v = true)).card = d 39 40 /-- Start with the source alone and certify the size of each successive reachable layer. -/ 41 def CountTrace {N : ℕ} (G : Graph N) (a : Fin N) (counts : ℕ → ℕ) : Prop := 42 counts 0 = 1 ∧ ∀ k < N, CountStep G a k (counts k) (counts (k + 1)) 43 44 /-- A certified sequence of layer counts whose final census omits the target `b`. -/ 45 def NonreachCertificate {N : ℕ} (G : Graph N) (a b : Fin N) : Prop := 46 ∃ counts, CountTrace G a counts ∧ 47 ∃ S, Census G a N (counts N) S ∧ b ∉ S 48 49 end Lax362205.Counting 50 -
Exact censuses enumerate the whole layer
A census of reachable vertices with the correct cardinality contains every vertex of the layer. Distinctness is enforced by the finite-set representation.
1 import Lax362205.Counting 2 … module docstring, 8 lines 11 12 namespace Lax362205.ExactCensus 13 14 open Lax362205.Reachability Counting 15 16 axiom complete {N : ℕ} (G : Graph N) (a : Fin N) (k : ℕ) (S : Finset (Fin N)) : 17 Census G a k (layer G a k).card S → S = layer G a k 18 19 end Lax362205.ExactCensus 20 -
no assumptions
A finite subset with the same cardinality is the entire layer.
-
The next reachable layer
A vertex belongs to the next layer precisely when it is the source or has an incoming edge from the current layer.
1 import Lax362205.Counting 2 … module docstring, 8 lines 11 12 namespace Lax362205.SuccessorLayer 13 14 open Lax362205.Reachability Counting 15 16 axiom successor {N : ℕ} (G : Graph N) (a v : Fin N) (k : ℕ) : 17 v ∈ layer G a (k + 1) ↔ v = a ∨ ∃ u ∈ layer G a k, G u v = true 18 19 end Lax362205.SuccessorLayer 20 -
no assumptions
Remove the last edge of a nonempty walk; the empty walk ends at the source.
-
Correctness of vertex classification
With the correct current count, a vertex has a valid positive or negative classification exactly according to its membership in the next layer.
1 import Lax362205.Counting 2 … module docstring, 8 lines 11 12 namespace Lax362205.Classification 13 14 open Lax362205.Reachability Counting 15 16 axiom correct {N : ℕ} (G : Graph N) (a v : Fin N) (k : ℕ) (b : Bool) : 17 Classify G a k (layer G a k).card v b ↔ 18 (b = true ↔ v ∈ layer G a (k + 1)) 19 20 end Lax362205.Classification 21 -
An exact census makes the negative test exhaustive.
-
Correctness of one counting step
Starting from the correct layer size, valid classifications produce exactly the size of the next layer. Such classifications exist.
1 import Lax362205.Counting 2 … module docstring, 8 lines 11 12 namespace Lax362205.CountingStep 13 14 open Lax362205.Reachability Counting 15 16 axiom correct {N : ℕ} (G : Graph N) (a : Fin N) (k d : ℕ) : 17 CountStep G a k (layer G a k).card d ↔ d = (layer G a (k + 1)).card 18 19 end Lax362205.CountingStep 20 -
The vertices classified positively are exactly the next layer.
-
Correctness of the count sequence
The initial layer consists of the source. Inductive counting certifies exactly the successive layer sizes, including the final size after steps.
1 import Lax362205.Counting 2 … module docstring, 8 lines 11 12 namespace Lax362205.CountingTrace 13 14 open Lax362205.Reachability Counting 15 16 axiom correct {N : ℕ} (G : Graph N) (a : Fin N) (counts : ℕ → ℕ) : 17 CountTrace G a counts ↔ ∀ k ≤ N, counts k = (layer G a k).card 18 19 end Lax362205.CountingTrace 20 -
Induct from the singleton initial layer through the certified counting steps.
-
Correctness of nonreachability certificates
A valid sequence of counts and a final census omitting the target exist exactly when the target is unreachable from the source.
1 import Lax362205.Counting 2 … module docstring, 8 lines 11 12 namespace Lax362205.Nonreachability 13 14 open Lax362205.Reachability Counting 15 16 axiom correct {N : ℕ} (G : Graph N) (a b : Fin N) : 17 NonreachCertificate G a b ↔ ¬ Reachable G a b 18 19 end Lax362205.Nonreachability 20 -
The final exact census contains every reachable vertex, so omitting the target certifies nonreachability.
-
Counting on the configuration graph
For every terminal accepting configuration, certify that it cannot be reached from the initial configuration. The implementation must generate the witnesses sequentially; this predicate alone makes no space claim.
1 import Lax362205.ConfigurationGraph 2 import Lax362205.Counting 3 … module docstring, 9 lines 13 14 namespace Lax362205.ConfigurationCounting 15 16 open Lax434930.PolynomialTime Lax434930.SpaceMachines 17 open Lax362205.BoundedConfigurations Lax362205.ConfigurationGraph Counting 18 19 def RejectsByCounting (M : Machine) (w : Word) (s : ℕ) : Prop := 20 ∀ a b : Config M w.length s, expand a = M.initial → 21 M.Terminal w (expand b) → M.accept b.state = true → 22 NonreachCertificate (graph M w s) (numbering M w.length s a) (numbering M w.length s b) 23 24 end Lax362205.ConfigurationCounting 25 -
Correctness of rejection by counting
On a space-bounded computation, counting certifies rejection precisely when there is no accepting computation.
1 import Lax362205.ConfigurationCounting 2 … module docstring, 8 lines 11 12 namespace Lax362205.Rejection 13 14 open Lax434930.PolynomialTime Lax434930.SpaceMachines ConfigurationCounting 15 16 axiom correct (M : Machine) (w : Word) (s : ℕ) (hs : M.UsesSpace w s) : 17 RejectsByCounting M w s ↔ ¬ M.Accepts w 18 19 end Lax362205.Rejection 20 -
Apply the nonreachability certificate to each possible accepting configuration.
-
Logarithmic space for inductive counting
For a machine using logarithmic space, a nondeterministic machine implements its configuration counting predicate in logarithmic space. Vertices and bounded paths are generated sequentially. Every branch halts.
1 import Lax362205.ConfigurationCounting 2 import Lax434930.SpaceBounds 3 … module docstring, 9 lines 13 14 namespace Lax362205.CountMachine 15 16 open Lax434930.PolynomialTime Lax434930.SpaceMachines Lax434930.SpaceBounds 17 open ConfigurationCounting 18 19 axiom implement (M : Machine) (c : ℕ) (hc : 0 < c) 20 (hM : ∀ w, M.UsesSpace w (c * logSpace w.length)) : 21 ∃ (d : ℕ) (D : Machine), 0 < d ∧ 22 (∀ w, D.HaltsOn w ∧ (D.Accepts w ↔ RejectsByCounting M w (c * logSpace w.length))) ∧ 23 ∀ w, D.UsesSpace w (d * logSpace w.length) 24 25 end Lax362205.CountMachine 26 -
Compile the sequential path and census loops to a finite Turing machine. Every branch halts and every register has logarithmic length.
-
Complementing a logarithmic space language
The complement of a language in also belongs to .
1 import Lax434930.NondeterministicLogarithmicSpace 2 … module docstring, 7 lines 10 11 namespace Lax362205.ComplementClosure 12 13 open Lax434930.PolynomialTime Lax434930.NondeterministicLogarithmicSpace 14 15 axiom closed (A : Language) : A ∈ NL → Aᶜ ∈ NL 16 17 end Lax362205.ComplementClosure 18 -
The counting machine accepts the complement and preserves a logarithmic space bound.
-
thm✓
Lax362205.NLcoNLThe Immerman–Szelepcsényi theorem
Nondeterministic logarithmic space is closed under complement: .
1 import Lax434930.ComplementClasses 2 … module docstring, 8 lines 11 12 namespace Lax362205.NLcoNL 13 14 open Lax434930.NondeterministicLogarithmicSpace Lax434930.ComplementClasses 15 16 axiom nl_eq_conl : NL = coNL 17 18 end Lax362205.NLcoNL 19 -
Apply complement closure in both directions and use double complementation.