Pumping Lemma Proofs

Key results:

• {aⁿbⁿcⁿdⁿ} is not context-free (anbncndn_not_pumpable)
• {aⁿbⁿcⁿ} is not context-free (anbnc_not_pumpable)

These are used by:

• Theories.Syntax.CCG.Formal.GenerativeCapacity — proving CCG > CFG
• Phenomena.WordOrder.Studies.Shieber1985 — proving Swiss German ∉ CFL

inductive FourSymbol : Type

Alphabet for cross-serial dependency patterns.

• a : FourSymbol
• b : FourSymbol
• c : FourSymbol
• d : FourSymbol

instance instDecidableEqFourSymbol : DecidableEq FourSymbol

Equations

• instDecidableEqFourSymbol x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprFourSymbol.repr : FourSymbol → ℕ → Std.Format

Equations

• instReprFourSymbol.repr FourSymbol.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.a")).group prec✝
• instReprFourSymbol.repr FourSymbol.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.b")).group prec✝
• instReprFourSymbol.repr FourSymbol.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.c")).group prec✝
• instReprFourSymbol.repr FourSymbol.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.d")).group prec✝

instance instReprFourSymbol : Repr FourSymbol

Equations

• instReprFourSymbol = { reprPrec := instReprFourSymbol.repr }

instance instBEqFourSymbol : BEq FourSymbol

Equations

• instBEqFourSymbol = { beq := instBEqFourSymbol.beq }

def instBEqFourSymbol.beq : FourSymbol → FourSymbol → Bool

Equations

• instBEqFourSymbol.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instLawfulBEqFourSymbol : LawfulBEq FourSymbol

@[reducible, inline]

abbrev FourString : Type

Equations

• FourString = List FourSymbol

def isInLanguage_anbncndn (w : FourString) : Bool

The language {aⁿbⁿcⁿdⁿ | n ≥ 0}, modeling Dutch cross-serial dependencies.

Equations

• One or more equations did not get rendered due to their size.
• isInLanguage_anbncndn [] = true

def makeString_anbncndn (n : ℕ) : FourString

Generate aⁿbⁿcⁿdⁿ.

Equations

• makeString_anbncndn n = List.replicate n FourSymbol.a ++ List.replicate n FourSymbol.b ++ List.replicate n FourSymbol.c ++ List.replicate n FourSymbol.d

def HasPumpingProperty4 (inLang : FourString → Bool) : Prop

The CFL pumping property for languages over FourSymbol. Every context-free language has this property (pumping lemma). Showing a language lacks it proves it's not context-free.

Equations

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

theorem makeString_in_language (n : ℕ) : isInLanguage_anbncndn (makeString_anbncndn n) = true

makeString_anbncndn n is always in the language {aⁿbⁿcⁿdⁿ}.

theorem pump_breaks_anbncndn (p : ℕ) (_hp : p > 0) : have w := makeString_anbncndn p; ∀ (u v x y z : FourString), w = u ++ v ++ x ++ y ++ z → List.length (v ++ x ++ y) ≤ p → List.length v + List.length y ≥ 1 → ∃ (i : ℕ), isInLanguage_anbncndn (u ++ (List.replicate i v).flatten ++ x ++ (List.replicate i y).flatten ++ z) = false

Pumping breaks membership in {aⁿbⁿcⁿdⁿ}: for any decomposition of aᵖbᵖcᵖdᵖ into uvxyz with |vxy| ≤ p and |vy| ≥ 1, pumping at i=0 breaks membership.

Key insight: |vxy| ≤ p means vxy can't contain both.a and.d (they're separated by 2p positions). Pumping down (i=0) preserves one count at p while reducing the total, making counts unequal.

theorem anbncndn_not_pumpable : ¬HasPumpingProperty4 isInLanguage_anbncndn

{aⁿbⁿcⁿdⁿ} does NOT have the CFL pumping property, hence is not context-free.

Proof: for any pumping constant p, the word aᵖbᵖcᵖdᵖ ∈ L witnesses failure. By pump_breaks_anbncndn, every valid decomposition can be pumped down (i=0) to break membership, contradicting the pumping property's ∀ i guarantee.

inductive ThreeSymbol : Type

Alphabet for {aⁿbⁿcⁿ}.

• a : ThreeSymbol
• b : ThreeSymbol
• c : ThreeSymbol

instance instDecidableEqThreeSymbol : DecidableEq ThreeSymbol

Equations

• instDecidableEqThreeSymbol x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instReprThreeSymbol : Repr ThreeSymbol

Equations

• instReprThreeSymbol = { reprPrec := instReprThreeSymbol.repr }

def instReprThreeSymbol.repr : ThreeSymbol → ℕ → Std.Format

Equations

• instReprThreeSymbol.repr ThreeSymbol.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThreeSymbol.a")).group prec✝
• instReprThreeSymbol.repr ThreeSymbol.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThreeSymbol.b")).group prec✝
• instReprThreeSymbol.repr ThreeSymbol.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ThreeSymbol.c")).group prec✝

instance instBEqThreeSymbol : BEq ThreeSymbol

Equations

• instBEqThreeSymbol = { beq := instBEqThreeSymbol.beq }

def instBEqThreeSymbol.beq : ThreeSymbol → ThreeSymbol → Bool

Equations

• instBEqThreeSymbol.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instLawfulBEqThreeSymbol : LawfulBEq ThreeSymbol

def isInLanguage_anbnc (w : List ThreeSymbol) : Bool

The language {aⁿbⁿcⁿ | n ≥ 0}.

Equations

• One or more equations did not get rendered due to their size.
• isInLanguage_anbnc [] = true

def makeString_anbnc (n : ℕ) : List ThreeSymbol

Generate aⁿbⁿcⁿ.

Equations

• makeString_anbnc n = List.replicate n ThreeSymbol.a ++ List.replicate n ThreeSymbol.b ++ List.replicate n ThreeSymbol.c

def HasPumpingProperty3 (inLang : List ThreeSymbol → Bool) : Prop

The CFL pumping property for languages over ThreeSymbol.

Equations

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

theorem anbnc_not_pumpable : ¬HasPumpingProperty3 isInLanguage_anbnc

{aⁿbⁿcⁿ} does NOT have the CFL pumping property, hence is not context-free. Same structure as the four-symbol case: contiguity forces either.a or.c absent from vxy, preserving one count at p while the total decreases.