Deciding Presentations for DCF Languages

This file isolates the target normal form used by DCF complement closure. A is_DCF_total presentation is an ordinary final-state DPDA presentation whose automaton reaches some empty-input configuration on every input, and whose reachable empty-input configurations all agree on final-state membership.

theorem is_DCF_of_is_DCF_total {T : Type} [Fintype T] {L : Language T} (hL : is_DCF_total L) : is_DCF L

Every deciding-DPDA language is a DCF in the ordinary final-state sense.

def EveryDCFHasDeciderPresentation (T : Type) [Fintype T] : Prop

The totalization/normalization principle needed for unconditional DCF complement closure: every final-state DPDA language has an equivalent deciding-DPDA presentation.

Equations

• EveryDCFHasDeciderPresentation T = ∀ (L : Language T), is_DCF L → is_DCF_total L