Context-sensitive languages are closed under inverse homomorphism

The proof uses fixed-width blocks. For a homomorphism h : A → List B, one physical input cell stores the (bounded) list h a. Empty blocks are allowed. A cellwise finite verifier checks one move of the target LBA on the logical tape obtained by concatenating the nonempty positions of all blocks. CertifiedRowSystem then compiles the verifier to an input-sized LBA.

This construction is uniform in both finite alphabet types; no distinguished letters or fixed witness alphabets are used.

The semantic logical-tape step

A finite checker for VirtualStep

Logical rows and actual bounded-tape configurations

Fixed-width physical rows

The physical verifier scans fixed-width optional slots, whereas DenseRun scans only the occupied logical cells. The lemmas below are the generic bridge between these views.

theorem is_CS_inverseHomomorphicImage {A B : Type} [Fintype A] [Fintype B] (L : Language B) (h : A → List B) (hL : is_CS L) : is_CS {w : List A | List.flatMap h w ∈ L}

Context-sensitive languages over arbitrary finite alphabets are closed under inverse string homomorphism, including homomorphisms that erase letters.

theorem CS_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => is_CS

The class of context-sensitive languages is closed under inverse string homomorphism over all finite source and target alphabet types.