Computability of Emptiness for Deterministic Context-Free Languages

We use the same presentation as DCFL membership: a raw EncodedCFG, under the semantic promise that its language is deterministic context-free. CFG emptiness is uniformly decidable on every raw code, so in particular it is decidable on the promised DCFL codes.

This argument is specific to emptiness. It does not turn semantic closure under complement into an effective construction on this presentation: a valid code is not accompanied by an encoded deterministic automaton.

theorem DCFEncodedCFG.dcf_computableEmptiness {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : ComputableEmptiness DCF contextFreeLanguageOf Valid

DCFL emptiness is uniformly computable from a valid encoded CFG.

Valid codes present exactly the deterministic context-free languages, raw CFG membership is semidecidable, and the CFG emptiness checker works on every raw encoded grammar.