Context-Sensitive Languages Are Not Closed Under Regular Right Quotient

This is the standard Hopcroft--Ullman padding reduction. The noncontracting simulation of an unrestricted grammar appends padding to the generated word. Intersecting with the regular language some* none* keeps representatives whose padding is a suffix; quotienting by none* then exposes the source language. Instantiating the source with the unary halting language contradicts the fact that every context-sensitive language is recursive.

theorem CS_notClosedUnderRightQuotientWithRegular : ¬ClosedUnderRightQuotientWithRegular is_CS

Context-sensitive languages are not closed under right quotient with regular languages.

theorem CS_notClosedUnderRightQuotientWithRegular_of_embedding {α : Type} [Fintype α] (e : Option Unit ↪ α) : ¬ClosedUnderRightQuotientWithRegular is_CS

Context-sensitive languages are not closed under regular right quotient over any finite alphabet into which the binary witness alphabet embeds.

theorem CS_notClosedUnderRightQuotientWithRegular_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) : ¬ClosedUnderRightQuotientWithRegular is_CS

Context-sensitive languages are not closed under regular right quotient over any finite alphabet with at least two symbols.