Deterministic Linearly Bounded Automata

A deterministic linearly bounded automaton (DLBA) is a deterministic Turing machine whose read/write head is restricted to the portion of the tape containing the input. This makes the configuration space finite, yielding powerful decidability results that do not hold for unrestricted Turing machines.

We adapt Mathlib's Turing machine framework (Turing.TM0, Turing.TM1) by replacing the infinite Turing.Tape with a fixed-length BoundedTape.

Main Definitions

• DLBA.BoundedTape Γ n — A tape of n cells over alphabet Γ with a head position
• DLBA.Machine Γ Λ — A deterministic linearly bounded automaton
• DLBA.Cfg Γ Λ n — Configuration (state + bounded tape contents)
• DLBA.step — Single computation step (none = halted)
• DLBA.iterateStep — Multi-step computation
• DLBA.Halts — Whether the machine eventually halts
• DLBA.HaltsAt — The specific step at which the machine first halts
• DLBA.Accepts — Whether the machine halts in an accepting state
• DLBA.complementMachine — Complement machine (same transitions, negated acceptance)

Main Results

• DLBA.Cfg.instFintype — The configuration space is finite (for finite alphabets/states)
• DLBA.iterateStep_none_mono — Once halted, the machine remains halted
• DLBA.complement_step_eq — The complement machine takes identical transitions
• DLBA.complement_halts_iff — The complement machine halts iff the original does
• DLBA.complement_accepts_iff — On halting inputs, complement accepts iff original rejects
• DLBA.halts_iff_haltsWithin — A DLBA halts iff it halts within Fintype.card Cfg steps
• DLBA.decidableHalts — The halting problem for DLBAs is decidable
• DLBA.decidableAccepts — Acceptance for DLBAs is decidable

References

• Kuroda, S.Y. (1964), "Classes of languages and linear-bounded automata"
• Myhill, J. (1960), "Linear bounded automata"

Implementation Notes

We use Fin (n + 1) to index tape cells, guaranteeing at least one cell exists. Head movement is clamped at boundaries: moving left at position 0 or right at the last position leaves the head in place. This is the standard convention for DLBAs, where boundary markers prevent the head from leaving the input region.

Direction

inductive DLBA.Dir : Type

Direction for head movement. We include stay since the head is clamped at tape boundaries and this simplifies the definition of moveHead.

• left : Dir
• right : Dir
• stay : Dir

instance DLBA.instDecidableEqDir : DecidableEq Dir

Equations

• DLBA.instDecidableEqDir x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DLBA.instReprDir : Repr Dir

Equations

• DLBA.instReprDir = { reprPrec := DLBA.instReprDir.repr }

def DLBA.instReprDir.repr : Dir → ℕ → Std.Format

Equations

• DLBA.instReprDir.repr DLBA.Dir.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DLBA.Dir.left")).group prec✝
• DLBA.instReprDir.repr DLBA.Dir.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DLBA.Dir.right")).group prec✝
• DLBA.instReprDir.repr DLBA.Dir.stay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DLBA.Dir.stay")).group prec✝

instance DLBA.instFintypeDir : Fintype Dir

Equations

• DLBA.instFintypeDir = { elems := { val := ↑DLBA.Dir.enumList, nodup := DLBA.Dir.enumList_nodup }, complete := DLBA.instFintypeDir._proof_1 }

def DLBA.instInhabitedDir.default : Dir

Equations

• DLBA.instInhabitedDir.default = DLBA.Dir.left

instance DLBA.instInhabitedDir : Inhabited Dir

Equations

• DLBA.instInhabitedDir = { default := DLBA.instInhabitedDir.default }

Bounded Tape

structure DLBA.BoundedTape (Γ : Type u_1) (n : ℕ) : Type u_1

A bounded tape of n + 1 cells over alphabet Γ, with a read/write head. This replaces the infinite Turing.Tape used in unrestricted Turing machines. The tape always has at least one cell (indexed by Fin (n + 1)).

• contents : Fin (n + 1) → Γ

  Contents of each tape cell

• head : Fin (n + 1)

  Current head position

def DLBA.instDecidableEqBoundedTape.decEq {Γ✝ : Type u_1} {n✝ : ℕ} [DecidableEq Γ✝] (x✝ x✝¹ : BoundedTape Γ✝ n✝) : Decidable (x✝ = x✝¹)

Equations

• DLBA.instDecidableEqBoundedTape.decEq { contents := a, head := a_1 } { contents := b, head := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance DLBA.instDecidableEqBoundedTape {Γ✝ : Type u_1} {n✝ : ℕ} [DecidableEq Γ✝] : DecidableEq (BoundedTape Γ✝ n✝)

Equations

• DLBA.instDecidableEqBoundedTape = DLBA.instDecidableEqBoundedTape.decEq

def DLBA.BoundedTape.read {Γ : Type u_1} {n : ℕ} (t : BoundedTape Γ n) : Γ

Read the symbol under the head.

Equations

• t.read = t.contents t.head

def DLBA.BoundedTape.write {Γ : Type u_1} {n : ℕ} (t : BoundedTape Γ n) (a : Γ) : BoundedTape Γ n

Write a symbol at the current head position.

Equations

• t.write a = { contents := Function.update t.contents t.head a, head := t.head }

def DLBA.BoundedTape.moveHead {Γ : Type u_1} {n : ℕ} (t : BoundedTape Γ n) (d : Dir) : BoundedTape Γ n

Move the head, clamping at boundaries (left end = 0, right end = n).

Equations

• t.moveHead DLBA.Dir.stay = { contents := t.contents, head := t.head }
• t.moveHead DLBA.Dir.left = { contents := t.contents, head := if h : 0 < ↑t.head then ⟨↑t.head - 1, ⋯⟩ else t.head }
• t.moveHead DLBA.Dir.right = { contents := t.contents, head := if h : ↑t.head < n then ⟨↑t.head + 1, ⋯⟩ else t.head }

noncomputable instance DLBA.BoundedTape.instFintype {Γ : Type u_1} {n : ℕ} [Fintype Γ] : Fintype (BoundedTape Γ n)

Equations

• DLBA.BoundedTape.instFintype = Fintype.ofInjective (fun (t : DLBA.BoundedTape Γ n) => (t.contents, t.head)) ⋯

Machine Definition

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

A deterministic linearly bounded automaton.

• Γ is the tape alphabet (must include a blank symbol, but we keep it general)
• Λ is the finite set of states
• transition maps (state, symbol) to (new_state, symbol_to_write, direction), or none to signal halting.
• accept determines which states are accepting (used to define the recognized language).
• initial is the start state.

• transition : Λ → Γ → Option (Λ × Γ × Dir)

  Transition function. Returns none to halt.

• accept : Λ → Bool

  Which states are accepting (decidable predicate).

• initial : Λ

  The initial state.

Configuration

structure DLBA.Cfg (Γ : Type u_1) (Λ : Type u_2) (n : ℕ) : Type (max u_1 u_2)

A configuration of a DLBA running on a tape of n + 1 cells.

• state : Λ

  Current state of the machine.

• tape : BoundedTape Γ n

  Current tape contents and head position.

def DLBA.instDecidableEqCfg.decEq {Γ✝ : Type u_1} {Λ✝ : Type u_2} {n✝ : ℕ} [DecidableEq Γ✝] [DecidableEq Λ✝] (x✝ x✝¹ : Cfg Γ✝ Λ✝ n✝) : Decidable (x✝ = x✝¹)

Equations

• DLBA.instDecidableEqCfg.decEq { state := a, tape := a_1 } { state := b, tape := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance DLBA.instDecidableEqCfg {Γ✝ : Type u_1} {Λ✝ : Type u_2} {n✝ : ℕ} [DecidableEq Γ✝] [DecidableEq Λ✝] : DecidableEq (Cfg Γ✝ Λ✝ n✝)

Equations

• DLBA.instDecidableEqCfg = DLBA.instDecidableEqCfg.decEq

noncomputable instance DLBA.Cfg.instFintype {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] : Fintype (Cfg Γ Λ n)

Equations

• DLBA.Cfg.instFintype = Fintype.ofInjective (fun (c : DLBA.Cfg Γ Λ n) => (c.state, c.tape)) ⋯

Step Function

def DLBA.step {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Option (Cfg Γ Λ n)

Execute one step of the DLBA. Returns none if the machine halts (i.e., the transition function returns none for the current state and symbol). The configuration just before halting can be inspected for acceptance.

Equations

• DLBA.step M cfg = match M.transition cfg.state cfg.tape.read with | none => none | some (q', a, d) => some { state := q', tape := (cfg.tape.write a).moveHead d }

def DLBA.iterateStep {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : ℕ → Option (Cfg Γ Λ n)

Iterate the step function k times. Returns some cfg' if the machine is still running after k steps, or none if it halted at or before step k.

Equations

• DLBA.iterateStep M cfg 0 = some cfg
• DLBA.iterateStep M cfg k.succ = (DLBA.iterateStep M cfg k).bind (DLBA.step M)

@[simp]

theorem DLBA.iterateStep_zero {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : iterateStep M cfg 0 = some cfg

theorem DLBA.iterateStep_succ {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (k : ℕ) : iterateStep M cfg (k + 1) = (iterateStep M cfg k).bind (step M)

theorem DLBA.iterateStep_none_mono {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) {k : ℕ} (hk : iterateStep M cfg k = none) (j : ℕ) : iterateStep M cfg (k + j) = none

theorem DLBA.iterateStep_some_of_succ_some {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) {k : ℕ} {cfg' : Cfg Γ Λ n} (hk : iterateStep M cfg (k + 1) = some cfg') : ∃ (cfg'' : Cfg Γ Λ n), iterateStep M cfg k = some cfg''

theorem DLBA.iterateStep_add {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (i j : ℕ) : iterateStep M cfg (i + j) = (iterateStep M cfg i).bind fun (c : Cfg Γ Λ n) => iterateStep M c j

Halting and Acceptance

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

The machine halts from configuration cfg if there exists a step at which iterateStep returns none.

Equations

• DLBA.Halts M cfg = ∃ (k : ℕ), DLBA.iterateStep M cfg k = none

noncomputable def DLBA.haltingCfg {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (h : Halts M cfg) : Cfg Γ Λ n

The halting configuration: the configuration of the machine at the last step before it halts. This is where we check acceptance.

Equations

• DLBA.haltingCfg M cfg h = match _hk : DLBA.iterateStep M cfg (Nat.find h - 1) with | some c => c | none => cfg

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

The machine accepts from configuration cfg if it halts and the last configuration before halting has an accepting state.

Equations

• DLBA.Accepts M cfg = ∃ (k : ℕ), DLBA.iterateStep M cfg (k + 1) = none ∧ ∃ (cfg' : DLBA.Cfg Γ Λ n), DLBA.iterateStep M cfg k = some cfg' ∧ M.accept cfg'.state = true

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

The machine rejects from configuration cfg if it halts and the last configuration before halting has a non-accepting state.

Equations

• DLBA.Rejects M cfg = ∃ (k : ℕ), DLBA.iterateStep M cfg (k + 1) = none ∧ ∃ (cfg' : DLBA.Cfg Γ Λ n), DLBA.iterateStep M cfg k = some cfg' ∧ M.accept cfg'.state = false

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

The initial configuration for input w on a tape of n + 1 cells.

Equations

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

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

Load a non-empty list onto a bounded tape.

Equations

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

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

Initial configuration for a non-empty list input.

Equations

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

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

The language recognized by a DLBA: the set of inputs (of each length) that the machine accepts.

Equations

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

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

The language recognized by a DLBA, defined on non-empty lists.

Equations

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

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

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

Equations

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

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

Recognition with an explicit decision for the empty word (see LBA.LanguageRecognized).

Equations

• DLBA.LanguageRecognized M embed acceptEmpty w = (acceptEmpty = true ∧ w = [] ∨ DLBA.LanguageViaEmbed M embed w)

Complement Machine

def DLBA.complementMachine {Γ : Type u_1} {Λ : Type u_2} (M : Machine Γ Λ) : Machine Γ Λ

The complement of a deterministic DLBA: same transitions, negated acceptance. This is the key construction for showing closure under complement.

Equations

• DLBA.complementMachine M = { transition := M.transition, accept := fun (q : Λ) => !M.accept q, initial := M.initial }

@[simp]

theorem DLBA.complement_step_eq {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : step (complementMachine M) cfg = step M cfg

@[simp]

theorem DLBA.complement_iterateStep_eq {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (k : ℕ) : iterateStep (complementMachine M) cfg k = iterateStep M cfg k

theorem DLBA.complement_halts_iff {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Halts (complementMachine M) cfg ↔ Halts M cfg

theorem DLBA.complement_accepts_iff_rejects {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Accepts (complementMachine M) cfg ↔ Rejects M cfg

theorem DLBA.complement_rejects_iff_accepts {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Rejects (complementMachine M) cfg ↔ Accepts M cfg

theorem DLBA.accepts_or_rejects_of_halts {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (h : Halts M cfg) : Accepts M cfg ∨ Rejects M cfg

theorem DLBA.not_accepts_and_rejects {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : ¬(Accepts M cfg ∧ Rejects M cfg)

theorem DLBA.complement_language {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (w : Fin (n + 1) → Γ) (hh : Halts M (initCfg M w)) : w ∈ Language (complementMachine M) n ↔ w ∉ Language M n

Decidability of Halting

theorem DLBA.not_halts_of_iterate_eq {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) {i j : ℕ} (hij : i < j) (hi : iterateStep M cfg i = iterateStep M cfg j) (hi_some : (iterateStep M cfg i).isSome = true) : ¬Halts M cfg

theorem DLBA.exists_iterate_eq_of_long_run {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (hrun : ∀ k ≤ Fintype.card (Cfg Γ Λ n), (iterateStep M cfg k).isSome = true) : ∃ (i : ℕ) (j : ℕ), i < j ∧ j ≤ Fintype.card (Cfg Γ Λ n) ∧ iterateStep M cfg i = iterateStep M cfg j ∧ (iterateStep M cfg i).isSome = true

theorem DLBA.halts_iff_haltsWithin {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Halts M cfg ↔ ∃ k ≤ Fintype.card (Cfg Γ Λ n), iterateStep M cfg k = none

noncomputable instance DLBA.decidableHalts {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Decidable (Halts M cfg)

Equations

• DLBA.decidableHalts M cfg = decidable_of_iff (∃ k ≤ Fintype.card (DLBA.Cfg Γ Λ n), DLBA.iterateStep M cfg k = none) ⋯

theorem DLBA.accepts_iff_bounded {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Accepts M cfg ↔ ∃ k ≤ Fintype.card (Cfg Γ Λ n), iterateStep M cfg (k + 1) = none ∧ ∃ (cfg' : Cfg Γ Λ n), iterateStep M cfg k = some cfg' ∧ M.accept cfg'.state = true

noncomputable instance DLBA.decidableAccepts {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Decidable (Accepts M cfg)

Equations

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

theorem DLBA.rejects_iff_bounded {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Rejects M cfg ↔ ∃ k ≤ Fintype.card (Cfg Γ Λ n), iterateStep M cfg (k + 1) = none ∧ ∃ (cfg' : Cfg Γ Λ n), iterateStep M cfg k = some cfg' ∧ M.accept cfg'.state = false

noncomputable instance DLBA.decidableRejects {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) : Decidable (Rejects M cfg)

Equations

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

noncomputable instance DLBA.decidableLanguage {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (w : Fin (n + 1) → Γ) : Decidable (w ∈ Language M n)

Equations

• DLBA.decidableLanguage M w = DLBA.decidableAccepts M (DLBA.initCfg M w)

Closure Under Intersection and Union

def DLBA.productMachine {Γ : Type u_1} {Λ₁ : Type u_2} {Λ₂ : Type u_3} (M₁ : Machine Γ Λ₁) (M₂ : Machine Γ Λ₂) : Machine Γ (Λ₁ × Λ₂ × Bool)

Product machine for showing closure under intersection. Runs two LBAs in parallel by taking their product state space. Both machines share the same tape (for the intersection construction, we need them to operate on the same input).

Equations

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

Configuration Space Cardinality

theorem DLBA.card_cfg {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [Fintype Γ] [Fintype Λ] : Fintype.card (Cfg Γ Λ n) = Fintype.card Λ * Fintype.card Γ ^ (n + 1) * (n + 1)

theorem DLBA.card_boundedTape {Γ : Type u_1} {n : ℕ} [Fintype Γ] : Fintype.card (BoundedTape Γ n) = Fintype.card Γ ^ (n + 1) * (n + 1)

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

A language over a finite alphabet T is DLBA-recognizable if it is accepted by some finite deterministic linearly bounded automaton over the tape alphabet Option (T ⊕ Γ) (arbitrary finite work alphabet Γ), with the input written canonically via some ∘ Sum.inl and an explicit decision acceptEmpty for the empty word — the same convention as the Turing-machine/recursive definitions.

Equations

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

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

The class of deterministic LBA languages.

Equations

• DLBA = setOf is_DLBA