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.
Type de document :
Communication dans un congrès
Jos C. M. Baeten; Tom Ball; Frank S. Boer. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-7604, pp.357-371, 2012, Theoretical Computer Science. 〈10.1007/978-3-642-33475-7_25〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01556213
Contributeur : Hal Ifip <>
Soumis le : mardi 4 juillet 2017 - 17:45:38
Dernière modification le : mardi 4 juillet 2017 - 17:47:02
Document(s) archivé(s) le : vendredi 15 décembre 2017 - 01:19:07

Fichier

978-3-642-33475-7_25_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Takeshi Tsukada, Naoki Kobayashi. An Intersection Type System for Deterministic Pushdown Automata. Jos C. M. Baeten; Tom Ball; Frank S. Boer. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-7604, pp.357-371, 2012, Theoretical Computer Science. 〈10.1007/978-3-642-33475-7_25〉. 〈hal-01556213〉

Partager

Métriques

Consultations de la notice

27

Téléchargements de fichiers

11