DLBA Languages ⊆ Turing Machine Languages

We show that every language recognized by a linearly bounded automaton (DLBA) is also recognized by a Turing machine, connecting the DLBA framework to Mathlib's Turing machine definitions.

Strategy

Part 1: Turing.eval characterization

We show that DLBA.Accepts is equivalent to Mathlib's Turing.eval halting in an accepting state. Since Turing.eval is the common foundation underlying all Mathlib TM models (TM0, TM1, TM2), this connects the DLBA framework directly to Mathlib's notion of Turing computation.

Part 2: Concrete TM0 simulation

We construct a Turing.TM0.Machine that simulates a given DLBA. The construction has two phases:

1. Reading phase: The TM0 reads the input from the tape symbol by symbol, accumulating the symbols in its state space.
2. Simulation phase: Once the input is fully read, the TM0 simulates the DLBA step-by-step entirely within its state space (no further tape access needed).

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

Main Results

• DLBA.iterateStep_reaches — iterateStep implies Turing.Reaches
• DLBA.reaches_iterateStep — Turing.Reaches implies iterateStep
• DLBA.accepts_iff_eval — DLBA acceptance ↔ Turing.eval halts with accepting state
• DLBA.lba_language_subset_tm0_language — Every word accepted by the DLBA is accepted by the simulating TM0 machine

Part 1: Connecting DLBA to Turing.eval

theorem DLBA.iterateStep_reaches {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg cfg' : Cfg Γ Λ n) {k : ℕ} (hk : iterateStep M cfg k = some cfg') : Turing.Reaches (step M) cfg cfg'

If iterateStep M cfg k = some cfg', then Turing.Reaches (step M) cfg cfg'.

theorem DLBA.reaches_iterateStep {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg cfg' : Cfg Γ Λ n) (hr : Turing.Reaches (step M) cfg cfg') : ∃ (k : ℕ), iterateStep M cfg k = some cfg'

If Turing.Reaches (step M) cfg cfg', then there exists k such that iterateStep M cfg k = some cfg'.

theorem DLBA.accepts_iff_eval {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Accepts M cfg ↔ ∃ c ∈ Turing.eval (step M) cfg, M.accept c.state = true

DLBA acceptance is equivalent to Turing.eval halting in an accepting state. This connects the DLBA directly to Mathlib's Turing.eval framework, which underlies all TM models (TM0, TM1, TM2).

Part 2: Concrete TM0 Simulation

inductive DLBA.SimState (Γ : Type u_1) (Λ : Type u_2) (n : ℕ) : Type (max u_1 u_2)

States of the TM0 machine simulating an DLBA.

• reading {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} : List Γ → SimState Γ Λ n
• simulating {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} : Cfg Γ Λ n → SimState Γ Λ n
• loop {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} : SimState Γ Λ n

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

Equations

• DLBA.SimState.instInhabited = { default := DLBA.SimState.reading [] }

noncomputable def DLBA.toTM0 {Γ : Type u_1} {Λ : Type u_2} [DecidableEq Γ] (M : Machine Γ Λ) (n : ℕ) : Turing.TM0.Machine (Option Γ) (SimState Γ Λ n)

The TM0 machine that simulates a given DLBA.

Equations

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

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

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

Equations

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

@[reducible, inline]

noncomputable abbrev DLBA.tm0Step {Γ : Type u_1} {Λ : Type u_2} [DecidableEq Γ] (M : Machine Γ Λ) (n : ℕ) : Turing.TM0.Cfg (Option Γ) (SimState Γ Λ n) → Option (Turing.TM0.Cfg (Option Γ) (SimState Γ Λ n))

The TM0 step function for the DLBA simulation machine.

Equations

• DLBA.tm0Step M n = Turing.TM0.step (DLBA.toTM0 M n)

@[reducible, inline]

abbrev DLBA.SimCfg (Γ : Type u_1) (Λ : Type u_2) (n : ℕ) : Type (max u_1 u_2 u_1)

Abbreviation for TM0 configurations in the simulation.

Equations

• DLBA.SimCfg Γ Λ n = Turing.TM0.Cfg (Option Γ) (DLBA.SimState Γ Λ n)

noncomputable def DLBA.tm0Init {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (_M : Machine Γ Λ) (w : Fin (n + 1) → Γ) : SimCfg Γ Λ n

The initial TM0 configuration for a given encoded input.

Equations

• DLBA.tm0Init _M w = Turing.TM0.init (DLBA.encodeInput w)

Tape Helper Lemmas

theorem DLBA.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 DLBA.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 DLBA.tape_mk1_head {Γ : Type u_1} [Inhabited Γ] (l : List Γ) : (Turing.Tape.mk₁ l).head = l.headI

theorem DLBA.list_getI_eq_get {α : Type u_1} [Inhabited α] (l : List α) (k : ℕ) (hk : k < l.length) : l.getI k = l.get ⟨k, hk⟩

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

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

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

Reading Phase

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

A single reading step: if the head symbol is some a, the machine appends a to the accumulator and moves right.

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

When the head is none and the accumulator has length n + 1, the reading phase transitions to the simulation phase.

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

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

Simulation Phase Correctness

theorem DLBA.simulation_preserves_step {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg cfg' : Cfg Γ Λ n) (T : Turing.Tape (Option Γ)) (hstep : step M cfg = some cfg') : ∃ (T' : Turing.Tape (Option Γ)), tm0Step M n { q := SimState.simulating cfg, Tape := T } = some { q := SimState.simulating cfg', Tape := T' }

In the simulation phase, if the DLBA takes a step, the TM0 also takes a step maintaining the simulation invariant.

theorem DLBA.simulation_halts_on_accept {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (T : Turing.Tape (Option Γ)) (hhalt : step M cfg = none) (hacc : M.accept cfg.state = true) : tm0Step M n { q := SimState.simulating cfg, Tape := T } = none

In the simulation phase, if the DLBA halts in an accepting state, the TM0 halts.

theorem DLBA.tm0_halts_of_lba_accepts {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (T : Turing.Tape (Option Γ)) (hacc : Accepts M cfg) : (Turing.eval (tm0Step M n) { q := SimState.simulating cfg, Tape := T }).Dom

theorem DLBA.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 DLBA.lba_language_subset_tm0_language {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] [Fintype Γ] [DecidableEq Λ] [Fintype Λ] (M : Machine Γ Λ) (w : Fin (n + 1) → Γ) (hw : w ∈ Language M n) : (Turing.eval (tm0Step M n) (tm0Init M w)).Dom

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