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 metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01556213
Contributor : Hal Ifip <>
Submitted on : Tuesday, July 4, 2017 - 5:45:38 PM
Last modification on : Tuesday, July 4, 2017 - 5:47:02 PM
Long-term archiving on: : Friday, December 15, 2017 - 1:19:07 AM

File

978-3-642-33475-7_25_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

118

Files downloads

144