Context-Free Right Quotients

This file proves the sharp closure behavior for right quotients of context-free languages:

• CFLs are closed under right quotient with regular languages: if L is context-free and R is regular, then L / R is context-free.
• CFLs are not closed under right quotient with context-free languages.

Regular Quotient Strategy

For the positive theorem, we use an abstract, closure-property-based proof. The key idea is to "tag" each letter with whether it belongs to the kept prefix (Sum.inl) or the removed suffix (Sum.inr), then intersect with a regular "block" language that enforces the structure and R-membership, and finally erase the suffix tags via substitution.

Concretely, given a CFL L over T and a regular language R over T:

1. Tag substitution σ : T → Language (T ⊕ T) maps each letter a to {[inl a], [inr a]}. Since each σ(a) is CF, L.subst σ is CF (by CF_of_subst_CF).

2. Block language blockLang R over T ⊕ T consists of words of the form u.map inl ++ v.map inr where v ∈ R. This is regular (we construct a DFA).

3. Intersection: L.subst σ ⊓ blockLang R is CF (CF ∩ Regular = CF).

4. Erasure η : (T ⊕ T) → Language T keeps inl-tagged letters and erases inr-tagged ones. Since each η(x) is CF, (L.subst σ ⊓ blockLang R).subst η is CF.

5. Correctness: (L.subst σ ⊓ blockLang R).subst η = L / R.

CFL Quotient Counterexample

For the negative theorem, the witness is quotientNumerator / quotientDenominator, where

• quotientNumerator = {a^(2n)b^n | n ≥ 1}*
• quotientDenominator = {b^n a^n | n ≥ 1}* {b}

with false = a and true = b. Both languages are CFLs. Their quotient has unary regular slice exactly {a^(2^(k+1)) | k ∈ ℕ}, which is not CFL by the pumping lemma.

Main declarations

• blockLang — the regular "block" language
• blockLangDFA — a DFA recognising blockLang R
• is_CF_rightQuotient_regular — the main theorem (is_CF formulation)
• Language.IsContextFree.rightQuotient_regular — Mathlib-style formulation
• quotient_slice_eq_unaryPow2 — identifies the unary slice of the CFL/CFL quotient
• CF_notClosedUnderRightQuotient — CFLs are not closed under right quotient by CFLs

def blockLang {T : Type} (R : Language T) : Language (T ⊕ T)

The "block language" over the tagged alphabet T ⊕ T. A word belongs to blockLang R iff it has the form u.map Sum.inl ++ v.map Sum.inr with v ∈ R.

Equations

• blockLang R = {w : List (T ⊕ T) | ∃ (u : List T) (v : List T), w = List.map Sum.inl u ++ List.map Sum.inr v ∧ v ∈ R}

def blockLangDFA {T : Type} {σ : Type u_1} (D : DFA T σ) : DFA (T ⊕ T) (Option (Bool × σ))

Given a DFA D for R, build a DFA over T ⊕ T that recognises blockLang (D.accepts).

States: Option (Bool × σ) where

• some (false, q) = phase 1 (reading inl-tagged letters), DFA state q
• some (true, q) = phase 2 (reading inr-tagged letters), DFA state q
• none = dead (saw inl after inr)

Equations

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

theorem blockLangDFA_accepts {T : Type} {σ : Type u_1} (D : DFA T σ) : (blockLangDFA D).accepts = blockLang D.accepts

def tagSubst {T : Type} : T → Language (T ⊕ T)

Tag substitution: each letter a can be tagged as either inl a or inr a.

Equations

• tagSubst a = {[Sum.inl a], [Sum.inr a]}

def eraseInr {T : Type} : T ⊕ T → Language T

Erasure substitution: keep inl-tagged letters, erase inr-tagged ones.

Equations

• eraseInr (Sum.inl a) = {[a]}
• eraseInr (Sum.inr val) = {[]}

theorem is_CF_tagSubst {T : Type} (a : T) : is_CF (tagSubst a)

Each tagSubst a is a two-element language, hence context-free.

theorem is_CF_eraseInr {T : Type} (x : T ⊕ T) : is_CF (eraseInr x)

Each eraseInr x is a singleton language, hence context-free.

theorem subst_inter_block_subst_eq_rightQuotient {T : Type} (L R : Language T) : (L.subst tagSubst ⊓ blockLang R).subst eraseInr = L / R

theorem is_CF_rightQuotient_regular {T : Type} {L R : Language T} (hL : is_CF L) (hR : R.IsRegular) : is_CF (L / R)

Context-free languages are closed under right quotient with regular languages (is_CF formulation).

theorem Language.IsContextFree.rightQuotient_regular {T : Type} {L : Language T} (hL : L.IsContextFree) {R : Language T} (hR : R.IsRegular) : (L / R).IsContextFree

Context-free languages are closed under right quotient with regular languages (Mathlib-style Language.IsContextFree formulation).

theorem is_CF_prefixLang' {T : Type} {L : Language T} (hL : is_CF L) : is_CF L.prefixLang

prefixLang as a special case: if L is CF, then prefixLang L is CF.

theorem CF_closedUnderRightQuotientWithRegular {T : Type} : ClosedUnderRightQuotientWithRegular is_CF

The class of context-free languages is closed under right quotient with regular languages.

Standard CFL/CFL quotient witnesses

The eventual counterexample uses ({a^(2n)b^n | n ∈ ℕ})* / (({b^n a^n | n ∈ ℕ})* {b}). The unary slice of this quotient is unaryPow2.

def quotientLeftBlocks (ns : List ℕ) : List Bool

Flattened concatenation of positive left-block sizes.

Equations

• quotientLeftBlocks ns = (List.map (fun (n : ℕ) => List.replicate (2 * n) false ++ List.replicate n true) ns).flatten

def quotientRightBlocks (ns : List ℕ) : List Bool

Flattened concatenation of positive right-block sizes.

Equations

• quotientRightBlocks ns = (List.map (fun (n : ℕ) => List.replicate n true ++ List.replicate n false) ns).flatten

def quotientRightWitnessBlocks : ℕ → List (List Bool)

Denominator blocks for the explicit suffix witnessing a^(2^(k+1)) ∈ quotientNumerator / quotientDenominator.

Equations

• quotientRightWitnessBlocks 0 = []
• quotientRightWitnessBlocks k.succ = (List.replicate (2 ^ (k + 1)) true ++ List.replicate (2 ^ (k + 1)) false) :: quotientRightWitnessBlocks k

def quotientWitnessSuffix (k : ℕ) : List Bool

The suffix b^(2^k)a^(2^k) ... b²a² b used for the forward slice inclusion.

Equations

• quotientWitnessSuffix k = (quotientRightWitnessBlocks k).flatten ++ [true]

def quotientLeftWitnessBlocks : ℕ → List (List Bool)

Numerator blocks matching a^(2^(k+1)) ++ quotientWitnessSuffix k.

Equations

• quotientLeftWitnessBlocks 0 = [List.replicate 2 false ++ [true]]
• quotientLeftWitnessBlocks k.succ = (List.replicate (2 ^ (k + 2)) false ++ List.replicate (2 ^ (k + 1)) true) :: quotientLeftWitnessBlocks k

theorem quotientRightWitnessBlocks_mem (k : ℕ) (y : List Bool) : y ∈ quotientRightWitnessBlocks k → y ∈ quotientRightBlock

theorem quotientLeftWitnessBlocks_mem (k : ℕ) (y : List Bool) : y ∈ quotientLeftWitnessBlocks k → y ∈ quotientLeftBlock

theorem quotientWitnessSuffix_mem_denominator (k : ℕ) : quotientWitnessSuffix k ∈ quotientDenominator

theorem prefix_quotientWitnessSuffix_eq_leftWitnessBlocks (k : ℕ) : List.replicate (2 ^ (k + 1)) false ++ quotientWitnessSuffix k = (quotientLeftWitnessBlocks k).flatten

def unaryFalseStar : Language Bool

The regular unary language a*, with false = a.

Equations

• unaryFalseStar = KStar.kstar {[false]}

theorem unaryFalseStar_regular : unaryFalseStar.IsRegular

theorem unaryPow2_subset_quotient_slice : unaryPow2 ≤ quotientNumerator / quotientDenominator ⊓ unaryFalseStar

theorem quotient_slice_subset_unaryPow2 : quotientNumerator / quotientDenominator ⊓ unaryFalseStar ≤ unaryPow2

theorem quotient_slice_eq_unaryPow2 : quotientNumerator / quotientDenominator ⊓ unaryFalseStar = unaryPow2

theorem notCF_quotient : ¬is_CF (quotientNumerator / quotientDenominator)

Since the quotient's unary regular slice is unaryPow2, the quotient cannot be CFL.

theorem CF_notClosedUnderRightQuotient : ¬ClosedUnderRightQuotient is_CF

CFLs are not closed under right quotient by CFLs.

theorem CF_notClosedUnderRightQuotient_of_embedding {α : Type} (e : Bool ↪ α) : ¬ClosedUnderRightQuotient is_CF

CFLs are not closed under right quotient over any alphabet into which the binary witness alphabet embeds.

theorem CF_notClosedUnderRightQuotient_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) : ¬ClosedUnderRightQuotient is_CF

CFLs are not closed under right quotient over any finite alphabet with at least two symbols.