An Intersection Type System for Deterministic Pushdown Automata - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

## An Intersection Type System for Deterministic Pushdown Automata

(1) , (2)
1
2
• Function : Author
Naoki Kobayashi
• Function : Author

#### 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.

#### Domains

Computer Science [cs]

### Dates and versions

hal-01556213 , version 1 (04-07-2017)

### Licence

Attribution - CC BY 4.0

### Identifiers

• HAL Id : hal-01556213 , version 1
• DOI :

### Cite

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⟩

### Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

66 View