Deterministic Context-Free Right Quotients

This file proves that deterministic context-free languages are not closed under right quotient. The witness is the same quotient used for CFL non-closure:

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

Both witness languages are deterministic context-free, by the DPDAs in DeterministicContextFree/Examples. If DCFLs were closed under right quotient, their quotient would be a DCFL and therefore context-free, contradicting the CFL pumping argument already proved in ContextFree/Closure/Quotient.

theorem DCF_notClosedUnderRightQuotient : ¬ClosedUnderRightQuotient is_DCF

Deterministic context-free languages are not closed under right quotient.

theorem DCF_notClosedUnderRightQuotient_of_embedding {α : Type} [Fintype α] (e : Bool ↪ α) : ¬ClosedUnderRightQuotient is_DCF

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

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

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