Recursively enumerable languages as erasing images of context-sensitive languages

The padded grammar from Grammars.NonContracting.ErasingImage turns an arbitrary unrestricted grammar into a non-contracting grammar over Option T. Erasing the added none terminal recovers the source language. Since non-contracting languages are context-sensitive, every recursively enumerable language is therefore an erasing homomorphic image of a context-sensitive language.

Main declarations

• is_RE_exists_CS_homomorphicImage

theorem is_RE_exists_CS_homomorphicImage {T : Type} [Fintype T] {L : Language T} (hL : is_RE L) : ∃ (K : Language (Option T)), is_CS K ∧ K.homomorphicImage Grammar.ErasingImage.erasePadding = L

Every recursively enumerable language over a finite alphabet is the erasing homomorphic image of a context-sensitive language over the alphabet with one added padding symbol.