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

For letters a and b, Language.anbn a b is the language of the words consisting of n copies of a followed by n copies of b. It is language (10i) of [Cho57] (§3.2), the first of three languages there that are not finite state, and it is the standard witness that the context-free languages properly contain the regular ones (Language.setOf_isRegular_ssubset_setOf_isContextFree).

For distinct letters the language is not regular: the words aⁿ have pairwise distinct left quotients, since bⁿ completes aᵐ exactly when m = n. It is generated by the grammar S → a S b | ε, whose sentential forms are exactly aⁿ S bⁿ and aⁿ bⁿ.

Main definitions

• Language.anbn a b: the language {aⁿbⁿ | n ∈ ℕ}.
• ContextFreeGrammar.anbn a b: the grammar S → a S b | ε.

Main results

• Language.replicate_append_replicate_mem_anbn_iff: for a ≠ b, aᵐbⁿ is in the language exactly when m = n.
• Language.not_isRegular_anbn: for a ≠ b, the language is not regular.
• ContextFreeGrammar.language_anbn: the grammar generates the language, so Language.isContextFree_anbn.
• Language.setOf_isRegular_ssubset_setOf_isContextFree: over a finite alphabet with two letters, the regular languages are a proper subclass of the context-free languages.

References

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

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

The language {aⁿbⁿ | n ∈ ℕ} of the words consisting of n copies of the letter a followed by n copies of the letter b.

Equations

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

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

theorem Language.replicate_append_replicate_mem_anbn {α : Type u_1} {a b : α} (n : ℕ) : List.replicate n a ++ List.replicate n b ∈ anbn a b

@[simp]

theorem Language.replicate_append_replicate_mem_anbn_iff {α : Type u_1} {a b : α} (hab : a ≠ b) {m n : ℕ} : List.replicate m a ++ List.replicate n b ∈ anbn a b ↔ m = n

theorem Language.not_isRegular_anbn {α : Type u_1} {a b : α} (hab : a ≠ b) : ¬(anbn a b).IsRegular

For distinct letters, {aⁿbⁿ} is not regular: the left quotients by the words aⁿ are pairwise distinct, since bⁿ is in the one by aᵐ exactly when m = n.

def ContextFreeGrammar.anbn {α : Type u_1} (a b : α) : ContextFreeGrammar α

The grammar S → a S b | ε, with a single nonterminal.

Equations

• One or more equations did not get rendered due to their size.

theorem ContextFreeGrammar.mem_rules_anbn {α : Type u_1} {a b : α} {r : ContextFreeRule α Unit} : r ∈ (anbn a b).rules ↔ r = { input := (), output := [Symbol.terminal a, Symbol.nonterminal (), Symbol.terminal b] } ∨ r = { input := (), output := [] }

theorem ContextFreeGrammar.derives_anbn {α : Type u_1} {a b : α} (n : ℕ) : (anbn a b).Derives [Symbol.nonterminal ()] (List.map Symbol.terminal (List.replicate n a) ++ [Symbol.nonterminal ()] ++ List.map Symbol.terminal (List.replicate n b))

theorem ContextFreeGrammar.derives_anbn_iff {α : Type u_1} {a b : α} {v : List (Symbol α (anbn a b).NT)} : (anbn a b).Derives [Symbol.nonterminal ()] v ↔ ∃ (n : ℕ), v = List.map Symbol.terminal (List.replicate n a) ++ [Symbol.nonterminal ()] ++ List.map Symbol.terminal (List.replicate n b) ∨ v = List.map Symbol.terminal (List.replicate n a ++ List.replicate n b)

The sentential forms of anbn are aⁿ S bⁿ and aⁿbⁿ.

theorem ContextFreeGrammar.language_anbn {α : Type u_1} {a b : α} : (anbn a b).language = Language.anbn a b

theorem Language.isContextFree_anbn {α : Type u_1} (a b : α) : (anbn a b).IsContextFree

theorem Language.setOf_isRegular_ssubset_setOf_isContextFree {α : Type u_1} [Finite α] [Nontrivial α] : {L : Language α | L.IsRegular} ⊂ {L : Language α | L.IsContextFree}

Over a finite alphabet with two distinct letters a and b, the regular languages are a proper subclass of the context-free languages, as {aⁿbⁿ} witnesses.