Deterministic Context-Free Languages Are Not Closed Under Concatenation

The reduction uses the standard DCFL union witnesses. If DCFLs were closed under concatenation, then prefixing one branch by a fresh marker and concatenating with the marker star would let an intersection and a left quotient recover the union of the two witness languages.

theorem DCFConcatenation.DPDA.is_DCF_optional_marked_union_no_initial_epsilon {T Q₁ Q₂ S₁ S₂ : Type} [Fintype T] [Fintype Q₁] [Fintype Q₂] [Fintype S₁] [Fintype S₂] (M₁ : DPDA Q₁ T S₁) (M₂ : DPDA Q₂ T S₂) (hnoε : M₂.epsilon_transition M₂.initial_state M₂.start_symbol = none) : is_DCF {x : List (Bool ⊕ T) | (∃ (w : List T), x = Sum.inl false :: List.map Sum.inr w ∧ w ∈ M₁.acceptsByFinalState) ∨ ∃ (w : List T), x = List.map Sum.inr w ∧ w ∈ M₂.acceptsByFinalState}

theorem DCFConcatenation.DCF_optional_marked_union {T : Type} [Fintype T] {L₁ L₂ : Language T} (hL₁ : is_DCF L₁) (hL₂ : is_DCF L₂) : is_DCF {x : List (Bool ⊕ T) | (∃ (w : List T), x = Sum.inl false :: List.map Sum.inr w ∧ w ∈ L₁) ∨ ∃ (w : List T), x = List.map Sum.inr w ∧ w ∈ L₂}

If L₁ and L₂ are deterministic context-free, so is the language that contains either a marked payload from L₁ or an unmarked payload from L₂.

theorem DCFConcatenation.DCF_notClosedUnderConcatenation : ¬ClosedUnderConcatenation is_DCF

Deterministic context-free languages over Bool ⊕ Fin 3 are not closed under concatenation.