Context-sensitive closure under Kleene star

The usual fresh-start construction for context-free grammars is not sound for the noncontracting unrestricted grammars used to define is_CS: a rule with a left or right context could straddle two adjacent copies of the start symbol. The construction below prevents this by alternating two colours. Every symbol of one simulated copy, terminals included, carries the copy's colour. Hence a rule of the source grammar can only act inside one maximal colour run. After the simulation we forget the colours by an epsilon-free homomorphism.

A list localization lemma

The alternating-copy grammar

Soundness invariant

Reading a terminal good form

Erasing the colours

Removing ε from the base language does not change its Kleene star.

theorem CS_closedUnderKleeneStar {T : Type} : ClosedUnderKleeneStar is_CS

Context-sensitive languages are closed under Kleene star.