Linearly Bounded Automata

A linearly bounded automaton (LBA) is a nondeterministic Turing machine whose read/write head is confined to a region of the tape whose length is bounded by a linear function of the input length.

The canonical model used here is the endmarker presentation is_LBA/LBA (below): the input w is written bracketed between a left endmarker ⊢ and a right endmarker ⊣, so the tape is ⊢ w ⊣ (with |w| + 2 cells). The empty word gets the genuine two-cell tape ⊢⊣, on which the machine runs like any other input — so the machine itself decides ε, with no external flag. The head is confined to the bracketed region by the usual boundary clamping.

The tape alphabet is EndAlpha T Γ = Option (T ⊕ Γ) ⊕ Bool: the Sum.inl part is the marker-free interior alphabet (none = blank, some (Sum.inl t) = input symbol, some (Sum.inr γ) = a work symbol over an arbitrary finite work alphabet Γ), and Sum.inr false/Sum.inr true are the endmarkers ⊢/⊣. The input is written canonically, so the recognizer cannot do hidden preprocessing. Because Γ is an arbitrary finite type, the interior provides Θ(|w|) bits of read/write working space — genuine linear space, the standard Kuroda/Hopcroft–Ullman LBA, for which the recognised languages are exactly the context-sensitive ones (CS = LBA, see Equivalence/EndmarkerToFlag.lean).

The shared machine/configuration vocabulary (Machine, Step, Reaches, Accepts) and the plain list-loading helpers (loadList, initCfgList, LanguageViaEmbed) live here too; they are reused by the internal marker-free bounded-tape model (Automata/LinearBounded/Positive.lean, is_LBA_pos), which the CS = LBA development uses as the genuinely space-bounded core (it recognizes exactly the ε-free context-sensitive languages); the empty word is supplied here by the endmarker model running on ⊢⊣.

This is a separate automaton class from deterministic DLBAs. It reuses the bounded tape and configuration types from Langlib.Automata.DeterministicLinearBounded.Definition.

structure LBA.Machine (Γ : Type u_1) (Λ : Type u_2) : Type (max u_1 u_2)

A nondeterministic linearly bounded automaton.

• transition : Λ → Γ → Set (Λ × Γ × DLBA.Dir)
• accept : Λ → Bool
• initial : Λ

def LBA.Step {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg cfg' : DLBA.Cfg Γ Λ n) : Prop

One step of nondeterministic computation.

Equations

• LBA.Step M cfg cfg' = ∃ (q' : Λ) (a : Γ) (d : DLBA.Dir), (q', a, d) ∈ M.transition cfg.state cfg.tape.read ∧ cfg' = { state := q', tape := (cfg.tape.write a).moveHead d }

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

Multi-step reachability: the reflexive-transitive closure of Step.

Equations

• LBA.Reaches M = Relation.ReflTransGen (LBA.Step M)

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

The LBA accepts from configuration cfg if some computation path reaches an accepting state.

Equations

• LBA.Accepts M cfg = ∃ (cfg' : DLBA.Cfg Γ Λ n), LBA.Reaches M cfg cfg' ∧ M.accept cfg'.state = true

noncomputable def LBA.loadList {Γ : Type u_1} (w : List Γ) (hw : w ≠ []) : DLBA.BoundedTape Γ (w.length - 1)

Load a non-empty list onto a bounded tape.

Equations

• LBA.loadList w hw = { contents := fun (i : Fin (w.length - 1 + 1)) => w.get ⟨↑i, ⋯⟩, head := ⟨0, ⋯⟩ }

noncomputable def LBA.initCfgList {Γ : Type u_1} {Λ : Type u_2} (M : Machine Γ Λ) (w : List Γ) (hw : w ≠ []) : DLBA.Cfg Γ Λ (w.length - 1)

Initial configuration for a non-empty list input.

Equations

• LBA.initCfgList M w hw = { state := M.initial, tape := LBA.loadList w hw }

noncomputable def LBA.LanguageOfMachine {Γ : Type u_1} {Λ : Type u_2} (M : Machine Γ Λ) : Language Γ

The language recognized by an LBA, defined on non-empty lists.

Equations

• LBA.LanguageOfMachine M w = ∃ (hw : w ≠ []), LBA.Accepts M (LBA.initCfgList M w hw)

noncomputable def LBA.LanguageViaEmbed {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) (embed : T → Γ) : Language T

Recognition via an embedding from the input alphabet into the tape alphabet.

Equations

• LBA.LanguageViaEmbed M embed w = ∃ (hw : List.map embed w ≠ []), LBA.Accepts M (LBA.initCfgList M (List.map embed w) hw)

noncomputable def LBA.LanguageRecognized {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) (embed : T → Γ) (b : Bool) : Language T

An internal helper: the language LanguageViaEmbed M embed together with an explicit decision b for the empty word. The |w|-cell tape cannot run on ε, so this combinator is used only to state the recognized languages of the endmarker simulators (Equivalence/EndmarkerTape.lean, Equivalence/EndmarkerToFlag.lean), where b is always the derived value decide (ε ∈ L) — it is never a free parameter of any automaton model.

Equations

• LBA.LanguageRecognized M embed b w = (b = true ∧ w = [] ∨ LBA.LanguageViaEmbed M embed w)

The canonical endmarker model

The input is bracketed ⊢ w ⊣ (|w| + 2 cells); the empty word gets the two-cell tape ⊢⊣, so the machine decides ε itself.

@[reducible, inline]

abbrev LBA.EndAlpha (T : Type u_3) (Γ : Type u_4) : Type (max u_4 u_3)

Canonical tape alphabet of an endmarker LBA over input alphabet T and work alphabet Γ. The Sum.inl part is the marker-free interior alphabet Option (T ⊕ Γ) (blank / input / work); Sum.inr false is the left endmarker ⊢ and Sum.inr true the right endmarker ⊣.

Equations

• LBA.EndAlpha T Γ = (Option (T ⊕ Γ) ⊕ Bool)

@[reducible, inline]

abbrev LBA.leftMark {T : Type u_1} {Γ : Type u_2} : EndAlpha T Γ

The left endmarker ⊢.

Equations

• LBA.leftMark = Sum.inr false

@[reducible, inline]

abbrev LBA.rightMark {T : Type u_1} {Γ : Type u_2} : EndAlpha T Γ

The right endmarker ⊣.

Equations

• LBA.rightMark = Sum.inr true

noncomputable def LBA.loadEnd {T : Type u_1} {Γ : Type u_2} (w : List T) : DLBA.BoundedTape (EndAlpha T Γ) (w.length + 1)

The bracketed input tape ⊢ w ⊣: |w| + 2 cells, with the head at the left endmarker. Even the empty word gets the genuine two-cell tape ⊢⊣, so no separate empty-word flag is needed.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LBA.initCfgEnd {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (EndAlpha T Γ) Λ) (w : List T) : DLBA.Cfg (EndAlpha T Γ) Λ (w.length + 1)

The initial configuration of an endmarker LBA on input w: start state, head on ⊢.

Equations

• LBA.initCfgEnd M w = { state := M.initial, tape := LBA.loadEnd w }

noncomputable def LBA.LanguageEnd {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (EndAlpha T Γ) Λ) : Language T

The language recognized by an endmarker LBA: the input is bracketed ⊢ w ⊣ and the machine accepts by an ordinary accepting run (it can accept ε by inspecting the adjacent ⊢⊣).

Equations

• LBA.LanguageEnd M w = LBA.Accepts M (LBA.initCfgEnd M w)

def is_LBA {T : Type} [Fintype T] [DecidableEq T] (L : Language T) : Prop

A language over a finite alphabet T is LBA-recognizable if some finite nondeterministic linearly bounded automaton over the canonical endmarker alphabet Option (T ⊕ Γ) ⊕ Bool recognizes it with its input bracketed by endmarkers (⊢ w ⊣). The empty word is handled by the machine itself (it runs on the two-cell tape ⊢⊣), with no external accept-empty flag.

Equations

• is_LBA L = ∃ (Γ : Type) (Λ : Type) (x : Fintype Γ) (x : Fintype Λ) (x : DecidableEq Γ) (x : DecidableEq Λ) (M : LBA.Machine (LBA.EndAlpha T Γ) Λ), LBA.LanguageEnd M = L

def LBA {T : Type} [Fintype T] [DecidableEq T] : Set (Language T)

Equations

• LBA = setOf is_LBA