Deterministic Context-Free Languages Are Not Closed Under Reversal

The counterargument packages two DPDAs behind distinct leading markers. If DCFLs were closed under reversal, those markers would move to the right. Regular right quotient removes either marker, a second reversal restores the payloads, and inverse homomorphism removes the payload tag. This would make DCFLs closed under union, contradicting the established union counterexample.

The construction first gives a five-symbol witness alphabet Bool ⊕ Fin 3. An injective relabelling then transports failure to every finite alphabet with at least five symbols.

theorem DCF_notClosedUnderReverse_of_regularQuotient (hquotient : ClosedUnderRightQuotientWithRegular is_DCF) : ¬ClosedUnderReverse is_DCF

If regular right quotient is available, DCFLs over the five-symbol marked alphabet cannot be closed under reversal.

theorem DCF_notClosedUnderReverse : ¬ClosedUnderReverse is_DCF

Deterministic context-free languages over the five-symbol marked alphabet are not closed under reversal.

theorem DCF_notClosedUnderReverse_of_embedding {α : Type} [Fintype α] (e : Bool ⊕ Fin 3 ↪ α) : ¬ClosedUnderReverse is_DCF

DCFL reversal non-closure transports through any embedding of the five-symbol witness alphabet.

theorem DCF_notClosedUnderReverse_of_card {α : Type} [Fintype α] (hα : 5 ≤ Fintype.card α) : ¬ClosedUnderReverse is_DCF

DCFLs are not closed under reversal over any finite alphabet with at least five symbols.