feat(LogSpace): Savitch's theorem in space log² n, NL and RL in DSPACE(log² n) (#474)

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

Complexity/Computability/Complexity/Classes/LogSpace/Savitch.lean

@@ -0,0 +1,80 @@
+/-
+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`.
+
+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
+  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*, 3rd edition, Section 8.4, final
+  paragraph (p. 351)][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

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

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

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