Strict inclusion of indexed languages in context-sensitive languages

Every recursively enumerable language over a finite alphabet is an erasing homomorphic image of a context-sensitive language. Apply this construction to the unary halting language. Its padded cover uses the binary alphabet Option Unit and is context-sensitive. It cannot be indexed: indexed languages are closed under arbitrary homomorphisms, so erasing the padding would make the halting language indexed, hence context-sensitive and therefore recursive.

The resulting binary witness proves Indexed ⊊ CS. Injective terminal relabelling and reflection transport the witness to every finite alphabet with at least two symbols.

Main declarations

• exists_indexedCSStrictWitness
• indexedCSStrictWitness
• indexedCSStrictWitness_is_CS
• indexedCSStrictWitness_erasingImage
• indexedCSStrictWitness_not_Indexed
• Indexed_subclass_CS_and_exists_strict
• Indexed_strict_subclass_CS

theorem exists_indexedCSStrictWitness : ∃ (K : Language (Option Unit)), is_CS K ∧ K.homomorphicImage Grammar.ErasingImage.erasePadding = haltingUnaryLanguage

There is a context-sensitive language over the binary alphabet Option Unit whose padding-erasing image is the unary halting language.

noncomputable def indexedCSStrictWitness : Language (Option Unit)

A binary context-sensitive language whose padding erases to the unary halting language.

Equations

• indexedCSStrictWitness = Classical.choose exists_indexedCSStrictWitness

theorem indexedCSStrictWitness_is_CS : is_CS indexedCSStrictWitness

The binary strictness witness is context-sensitive.

theorem indexedCSStrictWitness_erasingImage : indexedCSStrictWitness.homomorphicImage Grammar.ErasingImage.erasePadding = haltingUnaryLanguage

Erasing the distinguished padding symbol from the binary witness gives the unary halting language.

theorem indexedCSStrictWitness_not_Indexed : ¬is_Indexed indexedCSStrictWitness

The binary context-sensitive witness is not indexed.

theorem Indexed_subclass_CS_and_exists_strict : (∀ (T : Type) (L : Language T), is_Indexed L → is_CS L) ∧ ∃ (T : Type) (L : Language T), is_CS L ∧ ¬is_Indexed L

Indexed languages are included in context-sensitive languages over every alphabet, and the inclusion is strict over at least one alphabet.

theorem Indexed_strict_subclass_CS {T : Type} [Fintype T] (hT : 2 ≤ Fintype.card T) : Indexed ⊂ CS

For every finite alphabet with at least two symbols, indexed languages form a strict subclass of the context-sensitive languages.