Skip to Main content Skip to Navigation
Conference papers

An Intersection Type System for Deterministic Pushdown Automata

Abstract : We propose a generic method for deciding the language inclusion problem between context-free languages and deterministic contextfree languages. Our method extends a given decision procedure for a subclass to another decision procedure for a more general subclass called a refinement of the former. To decide $\mathcal{L}_0 \subseteq \mathcal{L}_1$, we take two additional arguments: a language $\mathcal{L}_2$ of which $\mathcal{L}_1$ is a refinement, and a proof of $\mathcal{L}_0 \subseteq \mathcal{L}_2$. Our technique then refines the proof of $\mathcal{L}_0 \subseteq \mathcal{L}_2$ to a proof or a refutation of $\mathcal{L}_0 \subseteq \mathcal{L}_1$. Although the refinement procedure may not terminate in general, we give a sufficient condition for the termination. We employ a type-based approach to formalize the idea, inspired from Kobayashi’s intersection type system for model-checking recursion schemes. To demonstrate the usefulness, we apply this method to obtain simpler proofs of the previous results of Minamide and Tozawa on the inclusion between context-free languages and regular hedge languages, and of Greibach and Friedman on the inclusion between context-free languages and superdeterministic languages.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Tuesday, July 4, 2017 - 5:45:38 PM
Last modification on : Monday, May 17, 2021 - 12:00:04 PM
Long-term archiving on: : Friday, December 15, 2017 - 1:19:07 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Takeshi Tsukada, Naoki Kobayashi. An Intersection Type System for Deterministic Pushdown Automata. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.357-371, ⟨10.1007/978-3-642-33475-7_25⟩. ⟨hal-01556213⟩



Record views


Files downloads