Deterministic Context-Free Languages are Closed Under Complementation (Hopcroft and Ullman)

Kaan Taskin 📧 and Tobias Nipkow 📧

August 24, 2026

Abstract

A deterministic context-free language (DCFL) is a language accepted by a deterministic pushdown automaton (DPDA). This entry proves that the deterministic context-free languages are closed under complementation. The proof follows the one in the book by Hopcroft and Ullman (1979).

License

BSD License

Note

No AI was used.

Topics

Session DPDA_Complement_HU

Depends on

Cite

× 
@article{DPDA_Complement_HU-AFP,
  author  = {Kaan Taskin and Tobias Nipkow},
  title   = {Deterministic Context-Free Languages are Closed Under   Complementation (Hopcroft and Ullman)},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/DPDA_Complement_HU.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download