The language {aᵐbⁿcᵐdⁿ | m, n ∈ ℕ}

For letters a, b, c and d, Language.ambncmdn a b c d is the language of the words aᵐbⁿcᵐdⁿ, in which the a block is matched by the c block and the b block by the d block, so that the two dependencies cross. For distinct letters it is not context-free; it is the language to which the argument of [Shi85] that Swiss German is not weakly context-free reduces.

The pumping argument shows more: a language that contains aⁿbⁿcⁿdⁿ for infinitely many n, and whose words have no more a than c and no more b than d, is not context-free. Pumping aⁿbⁿcⁿdⁿ down and up forces the pumped window to carry as many a as c and as many b as d, and a window no longer than the pumping length meets neither pair.

Main definitions

• Language.ambncmdn a b c d: the language {aᵐbⁿcᵐdⁿ | m, n ∈ ℕ}.

Main results

• Language.not_isContextFree_of_replicate_mem_of_count_le: a language containing infinitely many of the words aⁿbⁿcⁿdⁿ, whose words have no more a than c and no more b than d, is not context-free.
• Language.not_isContextFree_ambncmdn: for distinct letters, {aᵐbⁿcᵐdⁿ} is not context-free.

References

• S. M. Shieber, Evidence against the Context-Freeness of Natural Language (1985)
• J. E. Hopcroft, R. Motwani and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation (2000)

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

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

Equations

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

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

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

A language containing aⁿbⁿcⁿdⁿ for infinitely many n, whose words have no more a than c and no more b than d, is not context-free.

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

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