NLBA Languages ⊆ Turing Machine Languages

We show that every language recognized by a nondeterministic linearly bounded automaton (NLBA) is also recognized by a Turing machine, adapting the LBA ⊆ TM proof for the nondeterministic case.

Strategy

The key challenge is that NLBAs are nondeterministic: there may be multiple possible successor configurations at each step. We handle this by BFS determinization: the simulating Turing machine tracks the entire set of currently reachable NLBA configurations, expanding it by one nondeterministic step at a time.

Part 1: BFS Determinization

We define stepFinset M S, which expands a Finset of configurations by one NLBA step, and iterStepFinset M S k, which applies k expansion steps. We prove:

• Monotonicity: the configuration sets grow over time
• Correctness: if Reaches M cfg cfg' and cfg ∈ S, then cfg' ∈ iterStepFinset M S k for some k

Part 2: Concrete TM0 Simulation

We construct a Turing.TM0.Machine that simulates a given NLBA via BFS:

1. Reading phase: Same as the LBA simulation — read input symbols into the state.
2. Simulation phase: Track a Finset (DLBA.Cfg Γ Λ n) of reachable configurations. At each step, expand the set via stepFinset. If any configuration is accepting, halt. If the set reaches a fixpoint (no new configurations), loop forever.

The TM0 halts if and only if the NLBA accepts the input.

Main Results

• LBA.reaches_mem_iterStepFinset — multi-step reachability is captured by BFS
• LBA.reading_phase_complete — reading phase reaches the initial simulation state
• LBA.lba_language_subset_tm0_language — every word accepted by the NLBA is accepted by the simulating TM0 machine

Initialization

def LBA.initCfg {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (w : Fin (n + 1) → Γ) : DLBA.Cfg Γ Λ n

Initial configuration for a Fin-indexed input word.

Equations

• LBA.initCfg M w = { state := M.initial, tape := { contents := w, head := ⟨0, ⋯⟩ } }

def LBA.LanguageN {Γ : Type u_1} {Λ : Type u_2} (M : Machine Γ Λ) (n : ℕ) : Set (Fin (n + 1) → Γ)

The language recognized by an NLBA at a fixed input length.

Equations

• LBA.LanguageN M n = {w : Fin (n + 1) → Γ | LBA.Accepts M (LBA.initCfg M w)}

Part 1: BFS Determinization

def LBA.hasAccepting {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) : Prop

Whether a Finset of configurations contains an accepting one.

Equations

• LBA.hasAccepting M S = ∃ cfg ∈ S, M.accept cfg.state = true

noncomputable instance LBA.hasAcceptingDec {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) : Decidable (hasAccepting M S)

Equations

• LBA.hasAcceptingDec M S = inferInstance

noncomputable def LBA.stepFinset {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) : Finset (DLBA.Cfg Γ Λ n)

One-step BFS expansion: union of S with all configurations reachable in one NLBA step from any configuration in S.

Equations

• LBA.stepFinset M S = S ∪ {cfg' : DLBA.Cfg Γ Λ n | ∃ cfg ∈ S, LBA.Step M cfg cfg'}

noncomputable def LBA.iterStepFinset {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) : ℕ → Finset (DLBA.Cfg Γ Λ n)

Iterated BFS expansion.

Equations

• LBA.iterStepFinset M S 0 = S
• LBA.iterStepFinset M S k.succ = LBA.stepFinset M (LBA.iterStepFinset M S k)

theorem LBA.subset_stepFinset {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) : S ⊆ stepFinset M S

theorem LBA.step_mem_stepFinset {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) {cfg cfg' : DLBA.Cfg Γ Λ n} (hcfg : cfg ∈ S) (hstep : Step M cfg cfg') : cfg' ∈ stepFinset M S

theorem LBA.iterStepFinset_subset_succ {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) (k : ℕ) : iterStepFinset M S k ⊆ iterStepFinset M S (k + 1)

theorem LBA.iterStepFinset_mono {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) {i j : ℕ} (hij : i ≤ j) : iterStepFinset M S i ⊆ iterStepFinset M S j

theorem LBA.reaches_mem_iterStepFinset {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) {cfg cfg' : DLBA.Cfg Γ Λ n} (hcfg : cfg ∈ S) (hreach : Reaches M cfg cfg') : ∃ (k : ℕ), cfg' ∈ iterStepFinset M S k

Part 2: Concrete TM0 Simulation

inductive LBA.NSimState (Γ : Type u_1) (Λ : Type u_2) (n : ℕ) : Type (max u_1 u_2)

States of the TM0 machine simulating an NLBA via BFS.

• reading {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} : List Γ → NSimState Γ Λ n
• simulating {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} : Finset (DLBA.Cfg Γ Λ n) → NSimState Γ Λ n
• loop {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} : NSimState Γ Λ n

instance LBA.NSimState.instInhabited {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} : Inhabited (NSimState Γ Λ n)

Equations

• LBA.NSimState.instInhabited = { default := LBA.NSimState.reading [] }

noncomputable def LBA.nToTM0 {Γ : Type u_1} {Λ : Type u_2} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (n : ℕ) : Turing.TM0.Machine (Option Γ) (NSimState Γ Λ n)

The TM0 machine that simulates a given NLBA via breadth-first search.

Equations

• One or more equations did not get rendered due to their size.
• LBA.nToTM0 M n (LBA.NSimState.reading acc) (some a) = some (LBA.NSimState.reading (acc ++ [a]), Turing.TM0.Stmt.move Turing.Dir.right)
• LBA.nToTM0 M n LBA.NSimState.loop sym = some (LBA.NSimState.loop, Turing.TM0.Stmt.write sym)

def LBA.encodeInput {Γ : Type u_1} {n : ℕ} (w : Fin (n + 1) → Γ) : List (Option Γ)

Encode an NLBA input as a TM0 input (list over Option Γ).

Equations

• LBA.encodeInput w = List.map some (List.ofFn w)

@[reducible, inline]

noncomputable abbrev LBA.ntm0Step {Γ : Type u_1} {Λ : Type u_2} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (n : ℕ) : Turing.TM0.Cfg (Option Γ) (NSimState Γ Λ n) → Option (Turing.TM0.Cfg (Option Γ) (NSimState Γ Λ n))

The TM0 step function for the NLBA simulation machine.

Equations

• LBA.ntm0Step M n = Turing.TM0.step (LBA.nToTM0 M n)

@[reducible, inline]

abbrev LBA.NSimCfg (Γ : Type u_1) (Λ : Type u_2) (n : ℕ) : Type (max u_1 u_2 u_1)

Abbreviation for TM0 configurations in the NLBA simulation.

Equations

• LBA.NSimCfg Γ Λ n = Turing.TM0.Cfg (Option Γ) (LBA.NSimState Γ Λ n)

noncomputable def LBA.ntm0Init {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (_M : Machine Γ Λ) (w : Fin (n + 1) → Γ) : NSimCfg Γ Λ n

The initial TM0 configuration for a given encoded input.

Equations

• LBA.ntm0Init _M w = Turing.TM0.init (LBA.encodeInput w)

Tape Helper Lemmas

theorem LBA.tape_iter_move_right_nth {α : Type u_1} [Inhabited α] (T : Turing.Tape α) (k : ℕ) (i : ℤ) : ((Turing.Tape.move Turing.Dir.right)^[k] T).nth i = T.nth (i + ↑k)

theorem LBA.tape_mk1_move_right_head {α : Type u_1} [Inhabited α] (l : List α) (k : ℕ) : ((Turing.Tape.move Turing.Dir.right)^[k] (Turing.Tape.mk₁ l)).head = l.getI k

theorem LBA.encodeInput_length {Γ : Type u_1} {n : ℕ} (w : Fin (n + 1) → Γ) : (encodeInput w).length = n + 1

theorem LBA.encodeInput_getI {Γ : Type u_1} {n : ℕ} (w : Fin (n + 1) → Γ) (k : ℕ) (hk : k < n + 1) : (encodeInput w).getI k = some (w ⟨k, hk⟩)

theorem LBA.encodeInput_getI_end {Γ : Type u_1} {n : ℕ} (w : Fin (n + 1) → Γ) : (encodeInput w).getI (n + 1) = none

Reading Phase

theorem LBA.reading_single_step {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (acc : List Γ) (a : Γ) (T : Turing.Tape (Option Γ)) (hhead : T.head = some a) : ntm0Step M n { q := NSimState.reading acc, Tape := T } = some { q := NSimState.reading (acc ++ [a]), Tape := Turing.Tape.move Turing.Dir.right T }

theorem LBA.reading_to_simulating {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (acc : List Γ) (hacc : acc.length = n + 1) (T : Turing.Tape (Option Γ)) (hhead : T.head = none) : ∃ (T' : Turing.Tape (Option Γ)), ntm0Step M n { q := NSimState.reading acc, Tape := T } = some { q := NSimState.simulating {initCfg M fun (i : Fin (n + 1)) => acc.get (Fin.cast ⋯ i)}, Tape := T' }

theorem LBA.reading_phase_k_steps {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (w : Fin (n + 1) → Γ) (k : ℕ) (hk : k ≤ n + 1) : Turing.Reaches (ntm0Step M n) (ntm0Init M w) { q := NSimState.reading (List.take k (List.ofFn w)), Tape := (Turing.Tape.move Turing.Dir.right)^[k] (Turing.Tape.mk₁ (encodeInput w)) }

theorem LBA.reading_phase_complete {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (w : Fin (n + 1) → Γ) : ∃ (T : Turing.Tape (Option Γ)), Turing.Reaches (ntm0Step M n) (ntm0Init M w) { q := NSimState.simulating {initCfg M w}, Tape := T }

Simulation Phase

theorem LBA.simulation_step_bfs {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) (T : Turing.Tape (Option Γ)) (hnacc : ¬hasAccepting M S) (hne : stepFinset M S ≠ S) : ∃ (T' : Turing.Tape (Option Γ)), ntm0Step M n { q := NSimState.simulating S, Tape := T } = some { q := NSimState.simulating (stepFinset M S), Tape := T' }

theorem LBA.simulation_halts_on_accept {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) (T : Turing.Tape (Option Γ)) (hacc : hasAccepting M S) : ntm0Step M n { q := NSimState.simulating S, Tape := T } = none

theorem LBA.iterStepFinset_fixpoint {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S : Finset (DLBA.Cfg Γ Λ n)) {i : ℕ} (hfix : stepFinset M (iterStepFinset M S i) = iterStepFinset M S i) {m : ℕ} (hm : i ≤ m) : iterStepFinset M S m = iterStepFinset M S i

theorem LBA.simulation_reaches_iterStepFinset {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S₀ : Finset (DLBA.Cfg Γ Λ n)) (T₀ : Turing.Tape (Option Γ)) (k : ℕ) (hnacc : ∀ j < k, ¬hasAccepting M (iterStepFinset M S₀ j)) (hgrow : ∀ j < k, stepFinset M (iterStepFinset M S₀ j) ≠ iterStepFinset M S₀ j) : ∃ (T : Turing.Tape (Option Γ)), Turing.Reaches (ntm0Step M n) { q := NSimState.simulating S₀, Tape := T₀ } { q := NSimState.simulating (iterStepFinset M S₀ k), Tape := T }

theorem LBA.tm0_halts_of_nlba_accepts {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (S₀ : Finset (DLBA.Cfg Γ Λ n)) (T : Turing.Tape (Option Γ)) (hacc : ∃ cfg ∈ S₀, Accepts M cfg) : (Turing.eval (ntm0Step M n) { q := NSimState.simulating S₀, Tape := T }).Dom

theorem LBA.eval_dom_of_reaches {σ : Type u_1} (f : σ → Option σ) (a b : σ) (hr : Turing.Reaches f a b) (hb : (Turing.eval f b).Dom) : (Turing.eval f a).Dom

Main Theorem

theorem LBA.lba_language_subset_tm0_language {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (w : Fin (n + 1) → Γ) (hw : w ∈ LanguageN M n) : (Turing.eval (ntm0Step M n) (ntm0Init M w)).Dom

Main theorem: Every word accepted by the NLBA is also accepted by the simulating TM0 machine. This establishes that NLBA languages are a subset of TM0-recognizable languages.