Context-Free Closure Under Prefix

Proof that context-free languages are closed under the prefix operation, via the PDA equivalence (the "all states accept" / verification-mode approach).

Strategy

Given a CFL L accepted by PDA M (empty-stack), we build a prefix PDA whose language is exactly prefixLang L. The prefix PDA has two operating modes:

• Normal mode (Sum.inl states) – follows M's transitions, consuming input.
• Verification mode (Sum.inr states) – entered nondeterministically from normal mode (only when the input has been fully consumed). In this mode all of M's transitions (including reads) become ε-transitions, so the PDA can check that the remaining stack is "completable", i.e. that there exists some continuation word v under which M would reach empty stack.

Main declarations

• PDA.input_splitting – splitting a computation at a given input boundary
• PrefixClosure.prefixPDA – the prefix PDA construction
• is_PDA_prefixLang – is_PDA L → is_PDA (prefixLang L)
• Language.IsContextFree.prefixLang – CFLs are closed under prefix

theorem PDA.input_splitting_reachesIn {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] {M : PDA Q T S} {n : ℕ} {q p : Q} {w v : List T} {α δ : List S} (h : ReachesIn n { state := q, input := w ++ v, stack := α } { state := p, input := [], stack := δ }) : ∃ (q' : Q) (γ : List S) (n₁ : ℕ) (n₂ : ℕ), ReachesIn n₁ { state := q, input := w, stack := α } { state := q', input := [], stack := γ } ∧ ReachesIn n₂ { state := q', input := v, stack := γ } { state := p, input := [], stack := δ }

theorem PDA.input_splitting {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] {M : PDA Q T S} {q p : Q} {w v : List T} {α δ : List S} (h : Reaches { state := q, input := w ++ v, stack := α } { state := p, input := [], stack := δ }) : ∃ (q' : Q) (γ : List S), Reaches { state := q, input := w, stack := α } { state := q', input := [], stack := γ } ∧ Reaches { state := q', input := v, stack := γ } { state := p, input := [], stack := δ }

Input splitting (Reaches version).

noncomputable def PrefixClosure.prefixPDA {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) : PDA (Q ⊕ Q) T S

The prefix PDA. States are Q ⊕ Q where Sum.inl q is normal mode and Sum.inr q is verification mode.

Equations

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

theorem PrefixClosure.prefixPDA_supset {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) : M.acceptsByEmptyStack.prefixLang ≤ (prefixPDA M).acceptsByEmptyStack

theorem PrefixClosure.prefixPDA_subset {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) : (prefixPDA M).acceptsByEmptyStack ≤ M.acceptsByEmptyStack.prefixLang

theorem is_PDA_prefixLang {T : Type} [Fintype T] {L : Language T} (h : PDA.is_PDA L) : PDA.is_PDA L.prefixLang

PDA-recognisable languages are closed under prefix.

theorem Language.IsContextFree.prefixLang {T : Type} [Fintype T] {L : Language T} (h : L.IsContextFree) : L.prefixLang.IsContextFree

Context-free languages are closed under the prefix operation (proved via the PDA equivalence with the "all states accept" construction).

theorem is_CF_prefixLang {T : Type} [Fintype T] {L : Language T} (h : is_CF L) : is_CF L.prefixLang

Context-free languages are closed under the prefix operation (project-level is_CF formulation).