Deterministic context-free right quotients by regular languages

For a DPDA configuration (q, gamma) and a DFA state d, the set of stacks from which some continuation accepted by the DFA leads the DPDA to a final state is regular. We obtain its stack DFA by P-automaton saturation. The quotient DPDA then simulates the original machine while storing, below every stack symbol, the transition summary of all these stack DFAs. Consequently the finite control can decide at every input boundary whether an admissible accepting continuation exists.

The construction is uniform in every finite input alphabet; it does not use a distinguished letter or a fixed finite witness alphabet.

Saturation for regular continuations

Stack-summary DPDA

A run consuming w ++ y has a boundary configuration after exactly w has been consumed. Epsilon moves may occur on either side of that boundary.

Class-level closure theorem

theorem is_DCF_rightQuotient_regular {T : Type} [Fintype T] {L R : Language T} (hL : is_DCF L) (hR : R.IsRegular) : is_DCF (L / R)

A deterministic context-free language is closed under right quotient by a regular language, uniformly over every finite alphabet.

theorem DCF_closedUnderRightQuotientWithRegular {T : Type} [Fintype T] : ClosedUnderRightQuotientWithRegular is_DCF

The class of deterministic context-free languages is closed under right quotient with regular languages, for an arbitrary finite alphabet.