Deterministic LBA Languages ⊆ LBA Languages

We show that every language recognized by a deterministic linearly bounded automaton (DLBA) is also recognized by a nondeterministic linearly bounded automaton (LBA).

Strategy

The conversion uses Option Λ as the LBA state space:

• some q simulates LBA state q (always non-accepting in the NLBA)
• none is a special accepting halt state

When the DLBA halts (transition returns none) in an accepting state, the LBA transitions to none. This ensures the LBA accepts (reaches an accepting state) if and only if the DLBA accepts (halts in an accepting state).

Main Results

• is_DLBA_subset_is_LBA — Every DLBA language is an (endmarker) LBA language

Conversion from DLBA to LBA

def DLBA.toLBA' {Γ : Type u_1} {Λ : Type u_2} [DecidableEq Γ] (M : Machine Γ Λ) : LBA.Machine Γ (Option Λ)

Convert a deterministic DLBA to an LBA using Option Λ states.

• some q simulates DLBA state q (non-accepting)
• none is the accepting halt state When the DLBA halts in an accepting state, we transition to none.

Equations

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

Step Correspondence

theorem DLBA.dlba_step_implies_lba_step {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg cfg' : Cfg Γ Λ n) (h : step M cfg = some cfg') : LBA.Step (toLBA' M) { state := some cfg.state, tape := cfg.tape } { state := some cfg'.state, tape := cfg'.tape }

theorem DLBA.dlba_halt_accept_implies_lba_step {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (h_halt : step M cfg = none) (h_acc : M.accept cfg.state = true) : LBA.Step (toLBA' M) { state := some cfg.state, tape := cfg.tape } { state := none, tape := cfg.tape }

Multi-step Correspondence

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

Lift a single DLBA configuration to the LBA state space.

Equations

• DLBA.liftCfg cfg = { state := some cfg.state, tape := cfg.tape }

theorem DLBA.iterateStep_implies_lba_reaches {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg cfg' : Cfg Γ Λ n) {k : ℕ} (hk : iterateStep M cfg k = some cfg') : LBA.Reaches (toLBA' M) (liftCfg cfg) (liftCfg cfg')

Acceptance Correspondence

theorem DLBA.dlba_accepts_implies_lba_accepts' {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (h : Accepts M cfg) : LBA.Accepts (toLBA' M) (liftCfg cfg)

theorem DLBA.toLBA'_step_cases {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (q : Λ) (tape : BoundedTape Γ n) (cfg' : Cfg Γ (Option Λ) n) (h : LBA.Step (toLBA' M) { state := some q, tape := tape } cfg') : (∃ (q' : Λ) (tape' : BoundedTape Γ n), cfg' = { state := some q', tape := tape' } ∧ step M { state := q, tape := tape } = some { state := q', tape := tape' }) ∨ cfg' = { state := none, tape := tape } ∧ step M { state := q, tape := tape } = none ∧ M.accept q = true

theorem DLBA.toLBA'_reaches_inv {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (cfg' : Cfg Γ (Option Λ) n) (h : LBA.Reaches (toLBA' M) (liftCfg cfg) cfg') : (∃ (cfg_lba : Cfg Γ Λ n), cfg'.state = some cfg_lba.state ∧ cfg'.tape = cfg_lba.tape ∧ ∃ (k : ℕ), iterateStep M cfg k = some cfg_lba) ∨ cfg'.state = none ∧ Accepts M cfg

theorem DLBA.lba_accepts_implies_dlba_accepts' {Γ : Type u_1} {Λ : Type u_2} {n : ℕ} [DecidableEq Γ] (M : Machine Γ Λ) (cfg : Cfg Γ Λ n) (h : LBA.Accepts (toLBA' M) (liftCfg cfg)) : Accepts M cfg

Language Definitions For DLBAs

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

Load a non-empty list onto a bounded tape for a deterministic DLBA.

Equations

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

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

Initial configuration for a non-empty list input on a deterministic DLBA.

Equations

• DLBA.initCfgListDLBA M w hw = { state := M.initial, tape := DLBA.loadListDLBA w hw }

noncomputable def DLBA.LanguageViaEmbedDLBA {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, for a deterministic DLBA.

Equations

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

Initial Configuration Correspondence

theorem DLBA.initCfg_lift_eq {Γ : Type u_1} {Λ : Type u_2} [DecidableEq Γ] (M : Machine Γ Λ) (w : List Γ) (hw : w ≠ []) : liftCfg (initCfgListDLBA M w hw) = LBA.initCfgList (toLBA' M) w hw

Main Theorem

theorem dlba_language_eq_lba_language {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq Γ] (M : DLBA.Machine Γ Λ) (embed : T → Γ) : DLBA.LanguageViaEmbedDLBA M embed = LBA.LanguageViaEmbed (DLBA.toLBA' M) embed

theorem is_DLBA_subset_is_LBA {T : Type} [Fintype T] [DecidableEq T] {L : Language T} (h : is_DLBA L) : is_LBA L

theorem DLBA_subset_LBA {T : Type} [Fintype T] [DecidableEq T] : DLBA ⊆ LBA