The language {aⁿbⁿcⁿ | n ∈ ℕ}

For letters a, b and c, Language.anbncn a b c is the language of the words consisting of n copies of a, then n copies of b, then n copies of c. For distinct letters it is not context-free, the standard application of the pumping lemma: a window of the pumped word aᵖbᵖcᵖ no longer than p cannot meet both the a block and the c block, so pumping it out leaves the count of a or of c at p while removing letters.

The argument shows more: a language that contains aⁿbⁿcⁿ for infinitely many n, and whose words all have as many a as b as c, is not context-free.

Main definitions

• Language.anbncn a b c: the language {aⁿbⁿcⁿ | n ∈ ℕ}.

Main results

• Language.not_isContextFree_of_replicate_mem_of_count_eq: a language containing infinitely many of the words aⁿbⁿcⁿ, whose words have as many a as b as c, is not context-free.
• Language.not_isContextFree_anbncn: for distinct letters, {aⁿbⁿcⁿ} is not context-free.

References

• J. E. Hopcroft, R. Motwani and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation (2000)

def Language.anbncn {α : Type u_1} (a b c : α) : Language α

The language {aⁿbⁿcⁿ | n ∈ ℕ} of the words consisting of n copies of the letter a, then n copies of b, then n copies of c.

Equations

• Language.anbncn a b c = {w : List α | ∃ (n : ℕ), List.replicate n a ++ List.replicate n b ++ List.replicate n c = w}

theorem Language.mem_anbncn {α : Type u_1} {a b c : α} {w : List α} : w ∈ anbncn a b c ↔ ∃ (n : ℕ), List.replicate n a ++ List.replicate n b ++ List.replicate n c = w

theorem Language.replicate_append_replicate_append_replicate_mem_anbncn {α : Type u_1} {a b c : α} (n : ℕ) : List.replicate n a ++ List.replicate n b ++ List.replicate n c ∈ anbncn a b c

theorem Language.not_isContextFree_of_replicate_mem_of_count_eq {α : Type u_1} {a b c : α} [DecidableEq α] {X : Language α} (h : [a, b, c].Nodup) (hmem : ∃ᶠ (n : ℕ) in Filter.atTop, List.replicate n a ++ List.replicate n b ++ List.replicate n c ∈ X) (hcount : ∀ w ∈ X, List.count a w = List.count b w ∧ List.count b w = List.count c w) : ¬X.IsContextFree

A language containing aⁿbⁿcⁿ for infinitely many n, whose words have as many a as b as c, is not context-free. Pumping out a window of aⁿbⁿcⁿ no longer than the pumping length leaves a or c untouched, so by the counts no letter is removed at all.

theorem Language.not_isContextFree_anbncn {α : Type u_1} {a b c : α} [DecidableEq α] (h : [a, b, c].Nodup) : ¬(anbncn a b c).IsContextFree

For distinct letters, {aⁿbⁿcⁿ} is not context-free.