Linear languages are not closed under concatenation

A corollary of the linear pumping lemma: the witness {0ⁿ1ⁿ2ᵐ3ᵐ} is the concatenation of the two linear languages {0ⁿ1ⁿ} and {2ᵐ3ᵐ}, yet it is itself not linear. Hence the class of linear languages is not closed under concatenation (unlike the context-free languages). As with the strict inclusion, this transports to any alphabet with at least 4 elements.

Main results

• exists_Linear_concat_not_Linear — two linear languages whose concatenation is not linear.
• Linear_not_closedUnderConcatenation — Linear is not closed under concatenation over alphabets with at least 4 elements.

theorem map_concat_eq_map_anbncmdm {T : Type} (e : Fin 4 ↪ T) : (Language.map (⇑e ∘ f4)) anbn * (Language.map (⇑e ∘ g4)) anbn = (Language.map ⇑e) anbncmdm

The two linear factors concatenate to the relabelled witness language.

theorem map_comp_f4_is_Linear {T : Type} (e : Fin 4 ↪ T) : is_Linear ((Language.map (⇑e ∘ f4)) anbn)

{aⁿbⁿ} (the first factor over T) is linear.

theorem map_comp_g4_is_Linear {T : Type} (e : Fin 4 ↪ T) : is_Linear ((Language.map (⇑e ∘ g4)) anbn)

{cᵐdᵐ} (the second factor over T) is linear.

theorem exists_Linear_concat_not_Linear {T : Type} (e : Fin 4 ↪ T) : ∃ (L₁ : Language T) (L₂ : Language T), is_Linear L₁ ∧ is_Linear L₂ ∧ ¬is_Linear (L₁ * L₂)

There exist linear languages whose concatenation is not linear over any alphabet with at least 4 elements.

theorem Linear_not_closedUnderConcatenation {T : Type} (e : Fin 4 ↪ T) : ¬ClosedUnderConcatenation is_Linear

The class of linear languages is not closed under concatenation over any alphabet with at least 4 elements.

theorem Linear_not_closedUnderConcatenation_of_card {T : Type} [Fintype T] (hT : 4 ≤ Fintype.card T) : ¬ClosedUnderConcatenation is_Linear

The class of linear languages is not closed under concatenation over any finite alphabet with at least 4 elements.