Context-Sensitive Languages Are Closed Under Intersection With Regular Languages

The construction works at the LBA level. Before simulating the LBA for the context-sensitive language, a finite-control scan evaluates a DFA on the untouched input. If the DFA rejects there is no successor computation. If it accepts, the machine rewinds to the left endmarker and starts the original LBA on exactly its original initial tape.

theorem CS_inter_regular {T : Type} [Fintype T] [DecidableEq T] (L R : Language T) (hL : is_CS L) (hR : R.IsRegular) : is_CS (L ⊓ R)

The intersection of a context-sensitive language and a regular language is context-sensitive (over the library's standard finite alphabets).

theorem CS_closedUnderIntersectionWithRegular {T : Type} [Fintype T] [DecidableEq T] : ClosedUnderIntersectionWithRegular is_CS

Context-sensitive languages are closed under intersection with regular languages.