LBA Languages ⊆ Recursive Languages

Every language recognised by a (nondeterministic) linearly bounded automaton is recursive (decidable). This follows immediately from two results already in the library, composed:

• LBA_subset_CS — every endmarker-LBA language is context-sensitive (Myhill, the LBA ⊆ CS direction of CS = LBA, Equivalence/ContextSensitive.lean);
• CS_subset_Recursive_class — every context-sensitive language is recursive, via Post's theorem (Classes/ContextSensitive/Inclusion/Recursive.lean).

So the membership problem for an LBA is decidable, even though the open LBA ⇔? DLBA question (whether nondeterministic and deterministic LBAs recognise the same class) is not settled here.

Main results

• LBA_subset_Recursive — (LBA : Set (Language T)) ⊆ Recursive.
• LBA_strict_subclass_Recursive — (LBA : Set (Language T)) ⊂ Recursive over every nonempty finite computably encoded alphabet.
• LBA_strict_subclass_Recursive_of_card — the cardinality-based strict variant.

theorem LBA_subset_Recursive {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : LBA ⊆ Recursive

Every LBA language is recursive (decidable). Compose LBA ⊆ CS (Myhill) with CS ⊆ Recursive (Post).

theorem LBA_strict_subclass_Recursive {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] [Nonempty T] : LBA ⊂ Recursive

LBA-recognizable languages form a strict subclass of recursive languages over every nonempty finite computably encoded alphabet.

theorem LBA_strict_subclass_Recursive_of_card {T : Type} [Fintype T] [DecidableEq T] (hT : 1 ≤ Fintype.card T) : LBA ⊂ Recursive

LBA-recognizable languages form a strict subclass of recursive languages over every finite alphabet containing at least one symbol.