Context-sensitive languages are not closed under homomorphism

The unary halting language is recursively enumerable, so it is the erasing image of a context-sensitive padded language. If context-sensitive languages were closed under arbitrary string homomorphisms, the unary halting language would therefore be context-sensitive and hence recursive, a contradiction.

Main declaration

• CS_notClosedUnderHomomorphism

theorem CS_notClosedUnderHomomorphism : ¬ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_CS

Context-sensitive languages are not closed under arbitrary string homomorphisms. The counterexample is a context-sensitive padded cover of the unary halting language; erasing its padding yields a non-recursive language.