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 four symbols.

Main results

• exists_Linear_concat_not_Linear — two linear languages whose concatenation is not linear.
• Linear_not_closedUnderConcatenation — Linear is not closed under concatenation, with an _of_card variant for 4 ≤ Fintype.card T.

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

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 that admits an embedding of four distinct symbols.

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 that admits an embedding of four distinct symbols.

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 four symbols.