Theory Ogden_Example
section ‹Example: ‹{a⇧ib⇧jc⇧k | i ≠ j ∧ j ≠ k ∧ i ≠ k}› is not context-free›
theory Ogden_Example
imports "Context_Free_Grammar.Ogdens_Lemma" "ABC_Words"
begin
text ‹
This is Example 6.3 of Hopcroft and Ullman \cite{HopcroftU79}:
the language ‹L⇩4 = {a⇧ib⇧jc⇧k | i ≠ j ∧ j ≠ k ∧ i ≠ k}› is not context-free.
The proof uses Ogden's lemma in derivation form (@{thm [source] Ogden_Lemma}): we mark the
‹a›-positions of ‹z = a⇧n b⇧n⇧+⇧n⇧! c⇧n⇧+⇧2⇧n⇧!› and pump.
Following Hopcroft and Ullman, the marked block ‹v› and ‹x› must each be uniform (one letter),
and since the marks are on ‹a›s at least one of ‹v x› consists of ‹a›s. Hence ‹v x› omits ‹b›
or omits ‹c›. The factorials in the exponents are chosen so that pumping the ‹a›s (a block of
size ‹p ≤ n›, so ‹p› divides ‹n!›) lands the number of ‹a›s exactly on the number of ‹b›s
(‹n+n!›) or ‹c›s (‹n+2n!›) -- forcing a forbidden equality.
›
definition L4 :: "letter list set" where
"L4 = {abcword i j k | i j k. i ≠ j ∧ j ≠ k ∧ i ≠ k}"
lemma abcword_in_L4_iff: "abcword i j k ∈ L4 ⟷ i ≠ j ∧ j ≠ k ∧ i ≠ k"
by (auto simp: L4_def dest: abcword_inj)
text ‹A word of ‹L⇩4› has three pairwise-distinct letter counts.›
lemma L4_counts_distinct:
assumes "w ∈ L4"
shows "count_list w A ≠ count_list w B"
and "count_list w B ≠ count_list w C"
and "count_list w A ≠ count_list w C"
using assms by (auto simp: L4_def count_abcword)
text ‹Order the alphabet ‹A < B < C›, so that an ‹abcword› is exactly a ‹sorted› word.›
lemma L4_sorted: "w ∈ L4 ⟹ sorted w"
using abcword_sorted by (auto simp: L4_def)
text ‹The Ogden marking that distinguishes exactly the ‹A›-positions of a word.›
abbreviation amark :: "letter list ⇒ bool list" where
"amark zs ≡ map (λx. x = A) zs"
lemma dcount_amark: "dcount (amark zs) = count_list zs A"
by (induction zs) auto
text ‹Splitting a word splits its marking the same way (matching segment lengths).›
lemma append5_eq:
assumes "a1 @ a2 @ a3 @ a4 @ a5 = b1 @ b2 @ b3 @ b4 @ b5"
and "length a1 = length b1" "length a2 = length b2" "length a3 = length b3"
"length a4 = length b4" "length a5 = length b5"
shows "a1 = b1 ∧ a2 = b2 ∧ a3 = b3 ∧ a4 = b4 ∧ a5 = b5"
using assms by (auto)
lemma amark_split:
assumes z: "z = u @ v @ w @ x @ y"
and ds: "amark z = du @ dv @ dw @ dx @ dy"
and l: "length du = length u" "length dv = length v" "length dw = length w"
"length dx = length x" "length dy = length y"
shows "dv = amark v" "dw = amark w" "dx = amark x"
proof -
have eq: "du @ dv @ dw @ dx @ dy = amark u @ amark v @ amark w @ amark x @ amark y"
using ds z by simp
have "length du = length (amark u)" "length dv = length (amark v)"
"length dw = length (amark w)" "length dx = length (amark x)"
"length dy = length (amark y)"
using l by simp_all
from append5_eq[OF eq this]
show "dv = amark v" "dw = amark w" "dx = amark x" by simp_all
qed
text ‹Main theorem:›
theorem L4_not_CFL:
assumes finP: "finite (P :: ('n::fresh0, letter) Prods)"
shows "Lang P S ≠ L4"
proof
assume eq: "Lang P S = L4"
from Ogden_Lemma[OF finP, of S] obtain n where ogden: "ogden_property (Lang P S) n" ..
text ‹The witness word and its ‹a›-marking.›
define z where z_def: "z = abcword n (n + fact n) (n + 2 * fact n)"
have zL4: "z ∈ L4" using fact_gt_zero by (simp add: z_def abcword_in_L4_iff)
have zin: "z ∈ Lang P S" using zL4 eq by simp
have len: "length (amark z) = length z" by simp
have dcn: "dcount (amark z) = n" by (simp add: dcount_amark z_def count_abcword)
text ‹Apply Ogden's lemma with the ‹a›-marking.›
have nle: "n ≤ dcount (amark z)" using dcn by simp
from bspec[OF ogden zin, rule_format, OF conjI[OF len nle]]
obtain u v w x y du dv dw dx dy where
O1: "z = u @ v @ w @ x @ y"
and O2: "amark z = du @ dv @ dw @ dx @ dy"
and O3: "length du = length u" and O4: "length dv = length v"
and O5: "length dw = length w" and O6: "length dx = length x"
and O7: "length dy = length y"
and O8: "1 ≤ dcount (dv @ dx)"
and O9: "dcount (dv @ dw @ dx) ≤ n"
and pumpL4: "⋀i. u @ v ^^ i @ w @ x ^^ i @ y ∈ L4"
unfolding eq by blast
text ‹The marking restricted to the blocks counts the ‹a›s of those blocks.›
note splits = amark_split[OF O1 O2 O3 O4 O5 O6 O7]
have dvx: "dcount (dv @ dx) = count_list (v @ x) A"
by (simp add: splits dcount_amark)
have dvwx: "dcount (dv @ dw @ dx) = count_list (v @ w @ x) A"
by (simp add: splits dcount_amark)
text ‹So the number ‹p› of marked ‹a›s in ‹v x› satisfies ‹1 ≤ p ≤ n›, hence ‹p› divides ‹n!›.›
have vxA1: "1 ≤ count_list (v @ x) A" using O8 dvx by simp
have vxAn: "count_list (v @ x) A ≤ n"
using O9 dvwx by force
have dvdA: "count_list (v @ x) A dvd fact n" using vxA1 vxAn by (rule dvd_fact)
have dvd2A: "count_list (v @ x) A dvd 2 * fact n" using vxA1 vxAn by (simp add: dvd_fact)
text ‹Pumping with ‹i = 2› shows ‹v› and ‹x› are each uniform (sorted squares).›
have v2: "v ^^ 2 = v @ v" and x2: "x ^^ 2 = x @ x"
by (simp_all add: numeral_2_eq_2)
have srt2: "sorted (u @ v @ v @ w @ x @ x @ y)"
using L4_sorted[OF pumpL4[of 2]] by (simp add: v2 x2)
have uniform_v: "⋀a b. a ∈ set v ⟹ b ∈ set v ⟹ a = b"
using sorted_factor_uniform srt2 by blast
have uniform_x: "⋀a b. a ∈ set x ⟹ b ∈ set x ⟹ a = b"
by (meson sorted_append sorted_factor_uniform srt2)
text ‹Since ‹v x› contains an ‹a› and ‹v, x› are uniform, ‹v x› misses ‹b› or misses ‹c›.›
have AinVX: "A ∈ set (v @ x)"
using vxA1 by (metis count_list_0_iff not_one_le_zero)
have disj: "count_list (v @ x) B = 0 ∨ count_list (v @ x) C = 0"
using uniform_v uniform_x AinVX by (auto simp: count_list_0_iff)
text ‹Letter counts of a pumped word, and of ‹z› itself.›
have countX: "count_list (u @ v ^^ i @ w @ x ^^ i @ y) c
= count_list (u @ w @ y) c + i * (count_list v c + count_list x c)" for i c
by (simp add: count_list_pow_list algebra_simps)
have zsplit: "count_list z c = count_list (u @ w @ y) c + (count_list v c + count_list x c)" for c
using O1 by (simp)
have zA: "count_list z A = n" by (simp add: z_def count_abcword)
have zB: "count_list z B = n + fact n" by (simp add: z_def count_abcword)
have zC: "count_list z C = n + 2 * fact n" by (simp add: z_def count_abcword)
from disj show False
proof (elim disjE)
text ‹‹v x› has no ‹B›: pump ‹A›s up to ‹n+n! = › number of ‹B›s, contradicting ‹i ≠ j›.›
assume B0: "count_list (v @ x) B = 0"
define i0 where "i0 = Suc (fact n div count_list (v @ x) A)"
let ?word = "u @ v ^^ i0 @ w @ x ^^ i0 @ y"
have wordA: "count_list ?word A = n + fact n"
using countX dvdA i0_def zA zsplit by auto
have wordB: "count_list ?word B = n + fact n"
by (metis B0 countX count_list_append mult_is_0 zB zsplit)
from wordA wordB L4_counts_distinct(1)[OF pumpL4[of i0]] show False by simp
next
text ‹‹v x› has no ‹C›: pump ‹A›s up to ‹n+2n! = › number of ‹C›s, contradicting ‹i ≠ k›.›
assume C0: "count_list (v @ x) C = 0"
define i0 where "i0 = Suc (2 * fact n div count_list (v @ x) A)"
let ?word = "u @ v ^^ i0 @ w @ x ^^ i0 @ y"
have wordA: "count_list ?word A = n + 2 * fact n"
using countX dvd2A i0_def zA zsplit by auto
have wordC: "count_list ?word C = n + 2 * fact n"
by (metis C0 countX count_list_append mult_is_0 zC zsplit)
from wordA wordC L4_counts_distinct(3)[OF pumpL4[of i0]] show False by simp
qed
qed
end