# An Intersection Type System for Deterministic Pushdown Automata

Takeshi Tsukada, Naoki Kobayashi

► To cite this version:

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

HAL Id: hal-01556213

https://inria.hal.science/hal-01556213

Submitted on 4 Jul 2017

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
An Intersection Type System for Deterministic
Pushdown Automata

Takeshi Tsukada¹ and Naoki Kobayashi²

¹ Tohoku University

² University of Tokyo

**Abstract.** We propose a generic method for deciding the language inclusion problem between context-free languages and deterministic context-free 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.

# 1 Introduction

The language inclusion problem, which asks whether $\mathcal{L}_0 \subseteq \mathcal{L}_1$ for languages $\mathcal{L}_0$ and $\mathcal{L}_1$, is a fundamental problem in the field of formal language theory. We are interested in its decidability, mainly motivated by applications to program verification [1, 7, 12]. We consider the case that $\mathcal{L}_0$ and $\mathcal{L}_1$ range over context-free languages. It is well known that the inclusion $\mathcal{L}_0 \subseteq \mathcal{L}_1$ is undecidable for context-free languages $\mathcal{L}_0$ and $\mathcal{L}_1$. For some subclasses of context-free languages, however, the inclusion is decidable [3].

In the present paper, we propose a generic method for deciding the inclusion problem. Our method extends a decision procedure for a subclass of context-free languages to another decision procedure for a more general subclass. For example, consider the languages consisting of open and close tags, like XML documents. It is known to be decidable whether a given context-free language is included in the Dyck language, which is the set of all words consisting of correctly nested tags. Using our method, we can extend this result to obtain a new proof of the decidability of inclusion between context-free languages and regular hedge languages [12].
Our method can be outlined as follows. Suppose that a decision procedure is given, which takes a language $\mathcal{L}_0$ and decides whether $\mathcal{L}_0 \subseteq \mathcal{L}_2$ for a fixed language $\mathcal{L}_2$ (in the example above, the language of all correctly nested tags). We assume that the procedure returns a "proof" of $\mathcal{L}_0 \subseteq \mathcal{L}_2$ if it is the case. By using this procedure, our method provides a way of deciding whether $\mathcal{L}_0 \subseteq \mathcal{L}_1$, where $\mathcal{L}_1$ is a subset of $\mathcal{L}_2$, called a *refinement* [19] of $\mathcal{L}_2$ (in the above example, a regular hedge language). To decide $\mathcal{L}_0 \subseteq \mathcal{L}_1$, we first decide whether $\mathcal{L}_0 \subseteq \mathcal{L}_2$, using the decision procedure. If $\mathcal{L}_0 \not\subseteq \mathcal{L}_2$, we conclude $\mathcal{L}_0 \not\subseteq \mathcal{L}_1$. If $\mathcal{L}_0 \subseteq \mathcal{L}_2$, the procedure returns a "proof" of it, and we decide the inclusion $\mathcal{L}_0 \subseteq \mathcal{L}_1$ by refining the "proof" of $\mathcal{L}_0 \subseteq \mathcal{L}_2$.

To formalize the idea, we employ a type-based approach inspired by Kobayashi's intersection type system [7] for the model checking of higher-order recursion schemes. For each deterministic context-free language $\mathcal{L}_i$, we develop a type system characterizing context-free grammars $\mathcal{G}$ such that $\mathcal{L}_G \subseteq \mathcal{L}_i$, i.e., a type system $\mathcal{T}_i$ such that $\mathcal{G}$ is typable in $\mathcal{T}_i$ if and only if $\mathcal{L}_G \subseteq \mathcal{L}_i$. Then, the inclusion problem $\mathcal{L}_G \subseteq \mathcal{L}_i$ is reduced to the typability of $\mathcal{G}$ in $\mathcal{T}_i$. We check it by (i) first checking whether $\mathcal{G}$ is typable in a "simpler" type system $\mathcal{T}_2$, and (ii) if $\mathcal{G}$ is typable in $\mathcal{T}_1$, enumerating "refinements" of the type derivation of $\mathcal{T}_2 \vdash \mathcal{G}$ and checking whether there exists a type derivation for $\mathcal{G}$ in $\mathcal{T}_1$ among them. (We will substantiate the meaning of "simpler type system" and "refinements" in later sections.)

We demonstrate the usefulness of the method by giving simpler proofs of two previous decidability results: (1) The result of Minamide and Tozawa [12] on the inclusion between context-free languages and regular hedge languages; (2) The result of Greibach and Friedman [5] on the inclusion between context-free languages and superdeterministic languages, which is, to our knowledge, one of the strongest results about the inclusion problems.

The rest of the paper is organized as follows. In Section 2, we define some notions and notations about context-free grammars and pushdown automata. In Section 3, we construct an intersection type system characterizing the inclusion problem. In Section 4, we develop a procedure which refines a type derivation and we give a sufficient condition for the termination of the procedure. In Section 5, we apply our method to prove some decidability results. In Section 6, we discuss the related work and we conclude in Section 7. Omitted proofs can be found in the full version, available from the authors' web pages.

## 2 Preliminaries

*Context-free Grammars* We present context-free grammars for words in the form of (a special case of) context-free tree grammars generating monadic trees (i.e., trees of the form $a_1(a_2(...(a_n(\$))...)$). The definition is consistent with the standard definition of the context-free grammars.

We use a special letter $\$,$ which can occur only at the end of a word, and distinguish between two kinds of words: those that end with $\$,$ called *terminating words*, and those that end with a normal letter, called *normal words* (or
simply, words). A sort $κ$ is o describing terminating words, or $o \to o$ describing normal words. A normal word $w$ can be considered as a function that takes a terminating word $w'$$\$ and returns the terminating word $ww'$$\$; that is why we assign a function sort to normal words. A *context-free grammar* (CFG, for short) is a quadruple $G = (\mathcal{N}, \Sigma, \mathcal{R}, S)$, where:

1. $\mathcal{N}$ is a finite set of symbols called *non-terminals*. They have the sort $o \to o$. Non-terminals are ranged over by $F$.

2. $\Sigma$ is a finite set of symbols called *terminals*. We use *metavariables* $a$ and $b$ for terminals. They also have the sort $o \to o$.

3. $\mathcal{R}$ is a set of rewriting rules of the form $F x \to t$, where $x$ is a variable of the sort $o$ and $t$ is a term of the form $\alpha_1(\alpha_2(\dots(\alpha_n(x))\dots))$ with $\alpha_i \in \Sigma \cup \mathcal{N}$. There can be more than one rule for the same non-terminal.

4. $S$ is a distinguished non-terminal, called the *initial symbol*.

We use $t$ and $s$ as *metavariables* of terms and $\alpha$ as a *metavariable* ranging over $\Sigma \cup \mathcal{N}$. The *rewriting relation* $\Rightarrow_R$ is defined by:

$$F s \Rightarrow_R t[s/x] \text{ if } (F x \to t) \in \mathcal{R} \qquad \alpha t \Rightarrow_R \alpha t' \text{ if } t \Rightarrow_R t'$$

Here $t[s/x]$ is the term obtained by substituting $s$ for $x$ in $t$. We write $\Rightarrow_R^*$ for the reflexive and transitive closure of $\Rightarrow_R$. We often omit $\mathcal{R}$ if it is clear from the context. For a given non-terminal $F$, we define the *language generated by F* as $\mathcal{L}_G(F) = \{a_1a_2\dots a_n \in \Sigma^* | F \ $ $\Rightarrow^* a_1(a_2(\dots(a_n(\$))\dots))\}$. The *language generated by G*, written $\mathcal{L}_G$, is $\mathcal{L}_G(S)$.

**Example 1.** For a given alphabet $\Sigma$, we define the set of open tags $\Sigma^* = \{\acute{a} | a \in \Sigma\}$ and close tags $\bar{\Sigma} = \{\acute{a} | a \in \Sigma\}$. Let $G_0 = (\{S, F_a, F_b\}, \Sigma_0 \cup \bar{\Sigma}_0, \mathcal{R}, S)$, where $\Sigma_0 = \{\mathbf{a}, \mathbf{b}\}$ and $\mathcal{R} = \{Sx \to x, Sx \to \acute{a}(F_a(x)), Sx \to F_b(\mathbf{b}(x)), F_a x \to S(\acute{a}(x)), F_b x \to \acute{b}(S(x))\}$. The language $\mathcal{L}_G$ consists of words of the form $\acute{a}_1\acute{a}_2\dots\acute{a}_n\acute{a}_{n+1}\dots\acute{a}_1$, where $a_i \in \{\mathbf{a}, \mathbf{b}\}$ for all $1 \le i \le n$.

The rules of this CFG can be written in the standard notation as:

$$S \to \varepsilon \mid \acute{a} F_a \mid F_b \acute{b}, \qquad F_a \to S \acute{a}, \qquad F_b \to \acute{b} S,$$

where $\varepsilon$ denotes the empty word. $\square$

<figure><img src="image_2.png" /></figure>

**Pushdown Automaton** A pushdown automaton (PDA, for short) is a quadruple $M = (Q, \Sigma, \Gamma, \delta)$, where (1) $Q$ is a finite set of states; (2) $\Sigma$ is an alphabet; (3) $\Gamma$ is a finite set of stack symbols (we use *metavariables* $A$ and $B$ for stack symbols), and (4) $\delta \subseteq Q \times \Gamma \times (\Sigma \cup \{\varepsilon\}) \times Q \times \Gamma^*$ is a *transition relation*. We use $\tilde{A}$ and $\tilde{B}$ to denote (possibly empty) sequences of stack symbols. For $q \in Q$, $A \in \Gamma$ and $a \in \Sigma \cup \{\varepsilon\}$, we define $\delta(q, A, a) = \{(q', \tilde{A}') | (q, A, a, q', \tilde{A}') \in \delta\}$. A pushdown automaton is *deterministic* if for any $q \in Q$, $A \in \Gamma$ and $a \in \Sigma$, the set $\delta(q, A, a) \cup \delta(q, A, \varepsilon)$ has exactly one element. In the rest of the paper, we consider only deterministic pushdown automata.

We call an element of $Q \times \Gamma^*$ a *configuration*. If $(q, A, a, q', \tilde{A}') \in \delta$ (here $a \in \Sigma \cup \{\varepsilon\}$), we write $(q, \tilde{B}A) \Vdash_M^a (q', \tilde{B}\tilde{A}')$. We say a configuration $c$ is in
reading mode if $c$ has no $\epsilon$-transition, i.e., there is no configuration $c'$ such that $c \models_M^\epsilon c'$. For configurations $c$ and $c'$ in reading mode and $a \in \Sigma$, we write $c \models_M^{a} c'$ if

$$c \models_M^a d_1 \models_M^\epsilon d_2 \models_M^\epsilon \cdots \models_M^\epsilon d_n \models_M^\epsilon c' \not\models_M^\epsilon.$$

For $w = a_1a_2\dots a_n \in \Sigma^*$, we write $c \models_M^w c'$ if $c \models_M^{a_1} d_1 \models_M^{a_2} d_2 \models_M^{a_3} \dots \models_M^{a_n} c'$.

For a given configuration $c$ in reading mode and a given set $\mathcal{F}$ of configurations in reading mode, we define $\mathcal{L}_M(c, \mathcal{F}) = \{w \in \Sigma^* | \exists c' \in \mathcal{F}, c \models_M^w c'\}$. Here $c$ indicates the initial configuration and $\mathcal{F}$ the set of accepting configurations.

**Example 2.** Recall $\Sigma_0$ and $\mathcal{G}_0$ defined in Example 1. We define $\mathcal{A}_2 = \langle \{q\}, \hat{\Sigma}_0 \cup \hat{\Sigma}_0, \{\star\}, \delta_{\mathcal{A}_2}\rangle$, where $\delta_{\mathcal{A}_2} = \{(q, \star, \acute{a}, q, \star\star), (q, \star, \acute{a}, q, \epsilon) | a \in \Sigma_0\}$. The automaton $\mathcal{A}_2$ counts and records the difference between the numbers of open tags and close tags, ignoring their labels. Let $L = \mathcal{L}_{\mathcal{A}_2}((q, \star), \{(q, \star)\})$. Then $L$ is the set of all balanced tags, e.g., $\acute{a}\hat{b} \in L$ but $\acute{a}\hat{a}\hat{b}\hat{b} \notin L$. It is obvious that $\mathcal{L}_{\mathcal{G}_0} \subseteq \mathcal{L}_{\mathcal{A}_2}((q, \star), \{(q, \star)\})$.

We define a different PDA $\mathcal{A}_1 = \langle \{q_1, q_2\}, \hat{\Sigma}_0 \cup \hat{\Sigma}_0, \Sigma \cup \{\perp\}, \delta_{\mathcal{A}_1}\rangle$, where $\delta_{\mathcal{A}_1} = \{(q_1, A, \acute{a}, q_1, Aa) | A \in \Sigma_0 \cup \{\perp\}, a \in \Sigma_0\} \cup \{(q_1, a, \acute{a}, q_2, \epsilon), (q_2, a, \acute{a}, q_2, \epsilon) | a \in \Sigma_0\}$. In addition to counting the difference of open tags and close tags, $\mathcal{A}_1$ records labels of open tags on its stack, and checks if end tags are already read, by using its state. Let $L' = \mathcal{L}_{\mathcal{A}_1}((q_1, \perp), \{(q_1, \perp), (q_2, \perp)\})$. Then $L'$ is the set of all words of the form $\acute{a}_1\acute{a}_2\dots\acute{a}_n\acute{a}_n\dots\acute{a}_2\acute{a}_1$, where $a_i \in \Sigma_0$. Thus $\mathcal{L}_{\mathcal{G}_0} = L'$. $\square$

### 3 Type System

We construct a type system $\mathcal{T}_M$ for each PDA $M$ which characterizes the CFGs generating languages accepted by $M$. In the rest of this section, we fix a PDA $M$ and discuss the definition and properties of the type system $\mathcal{T}_M$.

The syntax of types is defined by: $\tau ::= c \mid \bigwedge \Theta \to c$, where $c$ ranges over configurations of $M$ in reading mode and $\Theta$ is a (possibly infinite) set of configurations in reading mode. We often abbreviate $\bigwedge \{d\} \to c$ as $d \to c$. We say a type $c$ has the sort $o$ (written as $c :: o$) and a type $\bigwedge \Theta \to c$ has the sort $o \to o$ (written as $\bigwedge \Theta \to c :: o \to o$). Intuitively, the type $c$ is for terminating words accepted from $c$ (by ignoring $\$$ at the end). Interpretations of $\to$ and $\bigwedge$ are standard: $d \to c$ describes functions from $d$ to $c$ and $c_1 \bigwedge c_2$ describes terminating words accepted from the both of $c_1$ and $c_2$. Thus a normal word $w = a_1\dots a_n$, which can be considered as a function $\lambda x. a_1(a_2(\dots(a_n(x))\dots))$, has a type $d \to c$ if $c \models_M^{a_1 a_2 \dots a_n} d$.

A type environment is a (possible infinite) set of bindings of the form $x : \tau$ or $F : \tau$. We allow multiple bindings for the same variable (or the same non-terminal), as in $\{x : \tau_1, x : \tau_2\}$. We often omit curly brackets, and simply write $x_1 : \tau_1, \dots, x_n : \tau_n$ for $\{x_1 : \tau_1, \dots, x_n : \tau_n\}$. We abbreviate $\{x : c | c \in \Theta\}$ as $x : \bigwedge \Theta$. We define $\Delta(x) = \{\tau | x : \tau \in \Delta\}$. A type environment $\Delta$ is well-formed if it respects the sort, i.e., $x : \tau \in \Delta$ implies $\tau :: o$ and $F : \tau \in \Delta$ implies $\tau :: o \to o$. We assume that all type environments appearing in the sequel are well-formed.
The typing rules are listed as follows.

$$ \frac{x : \tau \in \Delta \qquad F : \tau \in \Delta \qquad \frac{\Delta \vdash_M t_1 : \bigwedge \Theta \to c \qquad \Delta \vdash_M t_2 : d \quad (\text{for all } d \in \Theta)}{\Delta \vdash_M F : \tau \qquad \Delta \vdash_M t_1 t_2 : c} \qquad \frac{c \Vdash_M^a c'}{\Delta \vdash_M a : c' \to c}$$

These are standard rules for intersection type systems except for the last rule for constants, which is inspired by Kobayashi's type system [7]. Types of constants depend on the transition rule of the automaton, as explained below. Assume $c \Vdash_M^a c'$. Then for any (normal) word $w$ accepted from $c'$, $aw$ is accepted from $c$. By using type-based notations, for any (terminated) word $w(\$) : c'$, we have $a(w(\$)) : c$. Thus $a$ can be considered as a function of type $c' \to c$.

We say that a type environment $\Delta$ is an invariant of the rules $\mathcal{R}$, written $\Delta \vdash_M \mathcal{R}$, if $\Delta, x : \bigwedge \Theta \vdash_M t : c$ holds for all $F : \bigwedge \Theta \to c \in \Delta$ and $Fx \to t \in \mathcal{R}$. We write $\Delta \vdash_M (\mathcal{R}, S) : \bigwedge \Theta \to c$ if $\Delta \vdash_M \mathcal{R}$ and $\Delta, \$ : \bigwedge \Theta \vdash_M S\$ : c$ (in the type system, $\$$ is treated as a variable).

**Theorem 1.** Let $\mathcal{G} = (\mathcal{N}, \Sigma, \mathcal{R}, S)$ be a CFG, $M$ be a PDA, $c$ be a configuration of $M$ and $\mathcal{F}$ be a set of configurations of $M$. Then $\mathcal{L}_{\mathcal{G}}(S) \subseteq \mathcal{L}_{M}(c, \mathcal{F})$ if and only if $\Delta \vdash_M (\mathcal{R}, S) : \bigwedge \mathcal{F} \to c$ for some type environment $\Delta$.

*Proof.* The "if" direction follows from the facts that typing is preserved by reductions of $S\$$, and that $\$ : \bigwedge \mathcal{F} \vdash_M w\$ : c$ implies $w \in \mathcal{L}_M(c, \mathcal{F})$. For the other direction, let $\Delta = \{F : \bigwedge \Theta \to d \mid \mathcal{L}_G(F) \subseteq \mathcal{L}_M(d, \Theta)\}$. $\square$

By Theorem 1, the pair of the initial configuration $c$ and the set $\mathcal{F}$ of accepting configurations can be identified with the type $\bigwedge \mathcal{F} \to c$. We call the type $\iota = \bigwedge \mathcal{F} \to c$ the initial type and write $\mathcal{L}_M(\iota)$ for $\mathcal{L}_M(c, \mathcal{F})$. When $\Delta \vdash_M (\mathcal{R}, S) : \tau$, the environment $\Delta$ is called a witness of $\vdash_M (\mathcal{R}, S) : \tau$.

We introduce a partial order on witnesses and show the existence of the minimum witness.

**Definition 1.** The refinement ordering $\sqsubseteq$ is the smallest partial order that satisfies: (1) $\Theta_1 \sqsubseteq \Theta_2$ if $\Theta_1 \subseteq \Theta_2$, (2) $(\bigwedge \Theta_1 \to c_1) \sqsubseteq (\bigwedge \Theta_2 \to c_2)$ if $c_1 = c_2$ and $\Theta_1 \sqsubseteq \Theta_2$, and (3) $\Delta_1 \sqsubseteq \Delta_2$ if $\Delta_1(x) \sqsubseteq \Delta_2(x)$ for every $x$. $\square$

**Lemma 1.** Let $\mathcal{G} = (\mathcal{N}, \Sigma, \mathcal{R}, S)$ be a CFG, $M$ be a PDA and $\iota$ be its initial type. Assume that $\mathcal{L}_{\mathcal{G}}(S) \subseteq \mathcal{L}_{M}(\iota)$. Then the set of witnesses of $\vdash_M (\mathcal{R}, S) : \iota$, i.e., $\{\Delta \mid \Delta \vdash_M (\mathcal{R}, S) : \iota\}$, has the minimum element with respect to $\sqsubseteq$.

*Proof.* Let $\iota = \bigwedge \Theta \to c$. For a non-terminal $F$, we define $\text{pre}(F) = \{w \mid S\$ \Rightarrow^*_{\mathcal{R}} wFv\$\}$. Let $\Delta_0 = \{F : \bigwedge \Theta' \to c' \mid \exists w \in \text{pre}(F), c \Vdash_M^w c'$ and $\Theta' = \{d' \mid \exists u \in \mathcal{L}_G(F), c' \Vdash_M^u d'\}\}$. Then $\Delta_0 \vdash_M (\mathcal{R}, S) : \iota$ and $\Delta_0$ is minimum: See the full version for more details. $\square$

**Example 3.** Let $G_0$ be the CFG defined in Example 1, $A_2$ be the PDA defined in Example 2 and $\iota_2 = (q, \star) \to (q, \star)$. Since $\mathcal{L}_{G_0} \subseteq \mathcal{L}_{A_2}(\iota_2)$, by Theorem 1, there is $\Delta$ such that $\Delta \vdash_{A_2} (\mathcal{R}, S) : \iota_2$. The minimum witnesses is given by $\{S : (q, \tilde{A}) \to (q, \tilde{A}), F_a : (q, \tilde{A}) \to (q, \tilde{A}\star), F_b : (q, \tilde{A}\star) \to (q, \tilde{A}) \mid \tilde{A} \in \{\star\}^+\}$, where $\{\star\}^+$ is the set of non-empty sequences of $\star$. $\square$
Note that a minimum type environment may be infinite as in Example 3. In the rest of this section, we develop a way to finitely describe (some of) infinite type environments.

An important property of pushdown automata is that only the top of the stack affects its transition. Especially, we can add any stack symbols to the bottom, preserving the transition. For example, let $\mathcal{A}_1$ be the automaton defined in Example 2 and $w = \text{aatb}$. Then we have a transition $(q_1, \mathbf{bbb}) \models_{\mathcal{A}_1}^w (q_2, \mathbf{bb})$. By adding $\perp\mathbf{aa}$ to the bottom of the stack, we obtain $(q_1, \perp\mathbf{aabb}) \models_{\mathcal{A}_1}^w (q_2, \perp\mathbf{aabb})$. More generally, for any sequence $\tilde{A}$ of stack symbols, we have $(q_1, \tilde{A}\mathbf{bbb}) \models_{\mathcal{A}_1}^w (q_2, \tilde{A}\mathbf{bb})$. This does not depend on the choice of $w$, i.e., for any $w$ such that $(q_1, \mathbf{bbb}) \models_{\mathcal{A}_1}^w (q_2, \mathbf{bb})$, we have $(q_1, \tilde{A}\mathbf{bbb}) \models_{\mathcal{A}_1}^w (q_2, \tilde{A}\mathbf{bb})$.

We will formally state this fact in terms of intersection types (see Lemma 2).

**Definition 2.** For a given (possible empty) sequence $\tilde{B}$ of stack symbols and a given configuration $(q, \tilde{A})$, we define the stack extension $(q, \tilde{A}) \upharpoonright \tilde{B}$ as $(q, \tilde{B}\tilde{A})$. We define $(\Theta \upharpoonright \tilde{B}) = \{c \upharpoonright \tilde{B} \mid c \in \Theta\}$ for the set of configurations, $(\wedge \Theta \to c) \upharpoonright \tilde{B} = \wedge (\Theta \upharpoonright \tilde{B}) \to (c \upharpoonright \tilde{B})$ for the type, $\Delta \upharpoonright \tilde{B} = \{x : (\tau \upharpoonright \tilde{B}) \mid x : \tau \in \Delta\}$ for the type environment and $(\Delta \vdash t : \tau) \upharpoonright \tilde{B} = (\Delta \upharpoonright \tilde{B}) \vdash t : (\tau \upharpoonright \tilde{B})$ for the judgement. We define $\Delta^{\upharpoonright} = \cup_{\tilde{B}} (\Delta \upharpoonright \tilde{B})$. $\square$

**Lemma 2.** If $\Delta \vdash_M t : \tau$, then for any $\tilde{B}$, we have $(\Delta \vdash_M t : \tau) \upharpoonright \tilde{B}$.

*Proof.* Easy induction on $\Delta \vdash_M t : \tau$. $\square$

We write $\Delta \vdash_M^{\upharpoonright} \mathcal{R}$, read “$\Delta$ is an invariant of $\mathcal{R}$ up-to stack extensions”, if for every $F : \wedge \Theta \to c \in \Delta$ and $Fx \to t \in \mathcal{R}$, we have $(\Delta^{\upharpoonright})$, $x : \wedge \Theta \vdash_M t : c$. Note that while $F : \wedge \Theta \to c$ is chosen from $\Delta$, the environment to type the body of $F$ is $\Delta^{\upharpoonright}$. The judgement $\Delta \vdash_M^{\upharpoonright} (\mathcal{R}, S) : \wedge \Theta \to c$ is defined as $\Delta \vdash_M^{\upharpoonright} \mathcal{R}$ and $(\Delta^{\upharpoonright})$, $S : \wedge \Theta \vdash_M S : c$. $\square$

By using this up-to technique, we can sometimes (but not always) finitely describe a witness type environment as shown in the example below.

*Example 4.* Recall Example 3. We have $\Delta \vdash_{A_2}^{\upharpoonright} (\mathcal{R}, S) : \iota_2$, where $\Delta = \{S : (q, \star) \to (q, \star), F_a : (q, \star) \to (q, \star), F_b : (q, \star) \to (q, \star)\}$. Note that $\Delta$ is a finite set. $\square$

This up-to technique is sound in the sense that if a CFG is typable up-to stack expansions, then it is typable without using the up-to technique.

**Theorem 2.** $\Delta \vdash_M^{\upharpoonright} (\mathcal{R}, S) : \iota$ implies $(\Delta^{\upharpoonright}) \vdash_M (\mathcal{R}, S) : \iota$.

*Proof.* We should show that $(\Delta^{\upharpoonright}) \vdash_M \mathcal{R}$ and $(\Delta^{\upharpoonright})$, $S : \wedge \Theta \vdash_M S : c$, where $\iota = \wedge \Theta \to c$. The latter comes from the assumption. To show the former, assume $F : \tau \in (\Delta^{\upharpoonright})$ and $Fx \to t \in \mathcal{R}$. Then we have $F : \sigma \in \Delta$ and $\tau = (\sigma \upharpoonright \tilde{A})$ for some $\sigma$ and $\tilde{A}$. Let $\sigma = \wedge \Xi \to d$. Then $\tau = \wedge (\Xi \upharpoonright \tilde{A}) \to (d \upharpoonright \tilde{A})$. We should show that $(\Delta^{\upharpoonright})$, $(x : \wedge \Xi \upharpoonright \tilde{A}) \vdash_M t : (d \upharpoonright \tilde{A})$. By the assumption, $(\Delta^{\upharpoonright})$, $x : \wedge \Xi \vdash_M t : d$. By the previous lemma, we have $((\Delta^{\upharpoonright}) \upharpoonright \tilde{A})$, $(x : \wedge \Xi \upharpoonright \tilde{A}) \vdash_M t : (d \upharpoonright \tilde{A})$. Because $((\Delta^{\upharpoonright}) \upharpoonright \tilde{A}) \subseteq (\Delta^{\upharpoonright})^{\upharpoonright} = \Delta^{\upharpoonright}$, we conclude $(\Delta^{\upharpoonright})$, $(x : \wedge \Xi \upharpoonright \tilde{A}) \vdash_M t : (d \upharpoonright \tilde{A})$. $\square$
# 4 Refining Witnesses

It is in general difficult (in fact undecidable) to check whether a given CFG $\mathcal{G}$ is typable in $\mathcal{T}_{M_1}$ for a given PDA $M_1$, so that we first consider a simpler PDA $M_2$ and check whether $\mathcal{G}$ is typable in $\mathcal{T}_{M_2}$. If we choose $M_2$ so that (i) we have a witness of typability of $\mathcal{G}$ in $\mathcal{T}_{M_2}$ and (ii) $M_1$ is a refinement of $M_2$, then $\mathcal{G}$ is typable in $\mathcal{T}_{M_1}$ if and only if there is a witness that is a refinement of the witness in $\mathcal{T}_{M_2}$ (Section 4.1). Moreover, if a witness in $\mathcal{T}_{M_2}$ is finite, then the set of its refinements is a finite set. Thus, we can decide the typability in $\mathcal{T}_{M_1}$ by exhaustively searching a witness from the (finite) set of refinements of the witness in $\mathcal{T}_{M_2}$ (Section 4.2).

## 4.1 Refinements of Automata

We first define the notion of refinements of automata. As we will see below, if $M_1$ is a refinement of $M_2$, then $M_2$ is a good over-approximation of $M_1$.

**Definition 3 (Refinement of Automata).** Let $M_1 = (Q_1, \Sigma, \Gamma_1, \delta_1)$ and $M_2 = (Q_2, \Sigma, \Gamma_2, \delta_2)$ be pushdown automata. A homomorphism $f: M_1 \to M_2$ is a pair of mappings $f^Q: Q_1 \to Q_2$ and $f^\Gamma: \Gamma_1 \to \Gamma_2$ such that for any $(q, A, a, q', \tilde{B}) \in \delta_1$, $(f^Q(q), f^\Gamma(A), a, f^Q(q'), f^\Gamma(\tilde{B})) \in \delta_2$, where $f^\Gamma(B_1B_2\dots B_n) = f^\Gamma(B_1)f^\Gamma(B_2)\dots f^\Gamma(B_n)$. We often omit superscripts $Q$ and $\Gamma$, and simply write $f(q)$ and $f(\tilde{A})$. $\square$

The homomorphism $f: M_1 \to M_2$ can be naturally extended to mappings on configurations, types, type environments and judgements, e.g., the mapping on configurations is defined by $f((q, \tilde{A})) = (f^Q(q), f^\Gamma(\tilde{A}))$.

When there is a homomorphism $f: M_1 \to M_2$, we say $M_2$ is an approximation of $M_1$ and $M_1$ is a refinement of $M_2$. A type $\tau_1$ in $\mathcal{T}_{M_1}$ is a refinement of $\tau_2$ in $\mathcal{T}_{M_2}$ if $f(\tau_1) \subseteq \tau_2$. Refinements of type environments are defined similarly. We can always find a homomorphism $f: M_1 \to M_2$ if it exists, since both of $Q_1 \to Q_2$ and $\Gamma_1 \to \Gamma_2$ are finite. We write $f: (M_1, \iota_1) \to (M_2, \iota_2)$ if $f: M_1 \to M_2$ and $f(\iota_1) = \iota_2$. The next lemma justifies to say that $M_2$ is an (over-)approximation of $M_1$.

**Lemma 3.** If $f: (M_1, \iota_1) \to (M_2, \iota_2)$, then $\mathcal{L}_{M_1}(\iota_1) \subseteq \mathcal{L}_{M_2}(\iota_2)$. $\square$

**Example 5.** Let $\mathcal{A}_1$ and $\mathcal{A}_2$ be automata defined in Example 2. Then $\mathcal{A}_1$ is a refinement of $\mathcal{A}_2$ by a homomorphism $(h^Q, h^\Gamma): \mathcal{A}_1 \to \mathcal{A}_2$ given by $h^Q(q_1) = h^Q(q_2) = q$ and $h^\Gamma(\mathbf{a}) = h^\Gamma(\mathbf{b}) = h^\Gamma(\perp) = \star$. $\square$

In the following, we fix two pushdown automata (with their initial types) $(M_1, \iota_1)$ and $(M_2, \iota_2)$ and a homomorphism $f: (M_1, \iota_1) \to (M_2, \iota_2)$ between them. For readability, we write $\mathcal{T}_1$ instead of $\mathcal{T}_{M_1}$, $\mathcal{L}_1$ instead of $\mathcal{L}_{M_1}$ and so on. Validity of type judgements and minimality of a witness are preserved by $f$.

**Theorem 3.** Let $\mathcal{G} = (\mathcal{N}, \Sigma, \mathcal{R}, S)$ be a CFG, $M_1$ and $M_2$ be PDAs, $\iota_1$ and $\iota_2$ be their initial types and $f: (M_1, \iota_1) \to (M_2, \iota_2)$ be a homomorphism.
1. If $\Delta \vdash_{M_1} (\mathcal{R}, F) : \iota_1$, then $f(\Delta) \vdash_{M_2} (\mathcal{R}, F) : \iota_2$.

2. If $\Delta$ is the minimum witness of $\vdash_{M_1} (\mathcal{R}, F) : \iota_1$, then $f(\Delta)$ is the minimum witness of $\vdash_{M_2} (\mathcal{R}, F) : \iota_2$.

*Proof.* It is easy to prove that $\Delta \vdash_{M_1} t : \tau$ implies $f(\Delta) \vdash_{M_2} t : f(\tau)$ by induction on $t$. The first part of the claim is an easy consequence of this proposition. The second part is clear from the construction of the minimum witness in the proof of Lemma 1. $\square$

A witness $\Delta_2$ in $\mathcal{T}_2$ ensures the existence of a “smaller” witness in $\mathcal{T}_1$.

**Theorem 4.** Let $\mathcal{G} = (\mathcal{N}, \Sigma, \mathcal{R}, S)$ be a CFG, $M_1$ and $M_2$ be PDAs, $\iota_1$ and $\iota_2$ be their initial types and $f : (M_1, \iota_1) \to (M_2, \iota_2)$ be a homomorphism. Assume that $\Delta_2 \vdash_{M_2}^{\upharpoonright} (\mathcal{R}, S) : \iota_2$. If $\Delta_1 \vdash_{M_1}^{\upharpoonright} (\mathcal{R}, S) : \iota_1$, then there exists $\Delta'_1$ such that $\Delta'_1 \vdash_{M_1}^{\upharpoonright} (\mathcal{R}, S) : \iota_1$ and $f(\Delta'_1) \subseteq \Delta_2$.

*Proof.* Here, we give a proof sketch. Since $\Delta_1 \vdash_{M_1}^{\upharpoonright} (\mathcal{R}, S) : \iota_1$, there is the minimum witness type environment by Lemma 1. Let $\Delta'_1$ be the minimum witness of $\vdash_{M_1} (\mathcal{R}, S) : \iota_1$. Note that $f(\Delta'_1) \subseteq \Delta'_2$ by Theorem 3.

We shorten the types in $\Delta'_1$, appropriately. We define $(q, A_1A_2...A_m) \downarrow n = (q, A_{n+1}...A_m)$ if $m > n$ (and undefined otherwise). This operation is extended to types by $(\bigwedge \Theta \to c) \downarrow n = \bigwedge \{d \downarrow n \mid d \in \Theta\} \to (c \downarrow n)$. Let $(F, \tau'_1, \tau_2, \tilde{A}_2)$ be a quadruple such that $F : \tau'_1 \in \Delta'_1$, $F : \tau_2 \in \Delta_2$ and $f(\tau'_1) \subseteq (\tau_2 \upharpoonright \tilde{A}_2)$. The corresponding type binding $F : \tau'_1$ of the quadruple is defined by $\tau'_1 = \tau'_1 \downarrow n$, where $n$ is the length of $\tilde{A}_2$. Let $\Delta'_1$ be the set of all such bindings $F : \tau'_1$. Then $\Delta'_1$ satisfies the above conditions: See the full version for a more detailed proof. $\square$

## 4.2 Procedure and Sufficient Condition for Termination

Recall the overall picture of our method to understand the role of the procedure developed here. The final goal is to decide whether $\mathcal{G}$ is typable in $\mathcal{T}_1$. To solve the problem, we first check whether $\mathcal{G}$ is typable in $\mathcal{T}_2$, and if so, use the derivation for $\mathcal{T}_2$ and Theorem 4 to check whether $\mathcal{G}$ is typable in $\mathcal{T}_1$. The procedure developed here takes care of this last step.

Before describing the procedure, we define the notion of finiteness. We say that any base type $q$ is finite and a type $\bigwedge \Theta \to c$ is finite if $\Theta$ is a finite set. A type environment $\Delta$ is finite if $\Delta$ is a finite set and for every type binding $x : \tau \in \Delta$, $\tau$ is finite.

Figure 1 shows the procedure that refines a finite witness in $\mathcal{T}_2$ to one in $\mathcal{T}_1$. Here for a given grammar $\mathcal{G}$ and its rewriting relation $\mathcal{R}$, the function $\mathcal{H}$ on type environments in $\mathcal{T}_1$ is defined by

$$ \mathcal{H}(\Delta_1) = \{F : \bigwedge \Theta \to c \in \Delta_1 \mid \forall (Fx \to t) \in \mathcal{R}. \Delta_1, x : \bigwedge \Theta \vdash_{M_1}^{\upharpoonright} t : c\}. $$

The procedure takes five arguments: a grammar $\mathcal{G}$, two PDAs with the initial types $(M_1, \iota_1)$ and $(M_2, \iota_2)$, a homomorphism $f : (M_1, \iota_1) \to (M_2, \iota_2)$ and a finite
**Refine**($\mathcal{G}$, $(M_1, \iota_1)$, $(M_2, \iota_2)$, $f$, $\Delta_2$).

1. Let $n := 0$ and $\Delta_1^0 := \{F : \tau_1 \mid \exists \tau_2. F : \tau_2 \in \Delta_2 \text{ and } f(\tau_1) \subseteq \tau_2\}$.

2. Compute a fixed-point $\Delta_1$ of $\mathcal{H}$ starting from $\Delta_1^0$ as follows:

(a) Let $\Delta_1^{n+1} := \mathcal{H}(\Delta_1^n)$.

(b) If $\Delta_1^n = \Delta_1^{n+1}$, then $\Delta_1^n$ is a fixed-point of $\mathcal{H}$.

(c) Otherwise, let $n := n + 1$ and goto (a).

3. Check whether $S: \iota_1 \in \Delta_1$. If so, return $\Delta_1$. Otherwise, return **untypable**.

**Fig. 1.** The procedure to refine a witness

type environment $\Delta_2$ in $\mathcal{T}_2$ such that $\Delta_2 \vdash_{M_2}^{\uparrow} (\mathcal{R}, S): \iota_2$. The finiteness of the type environment ensures the termination of the procedure. The procedure returns a witness if it exists, and otherwise returns **untypable**.

**Example 6.** Let $\mathcal{G}_0$ be the CFG defined in Example 1, $\mathcal{A}_1$ and $\mathcal{A}_2$ be PDAs defined in Example 2, $\Delta'$ be the finite witness of $\vdash_{\mathcal{A}_2} (\mathcal{R}, S) : \iota_{\mathcal{A}_2}$ defined in Example 4, $f : \mathcal{A}_1 \to \mathcal{A}_2$ be the homomorphism defined in Example 5 and $\iota_{\mathcal{A}_1} = (q_1, \perp) \wedge (q_2, \perp) \to (q_1, \perp)$. We compute a witness of $\vdash_{\mathcal{A}_1} (\mathcal{R}, S) : \iota_{\mathcal{A}_1}$ by our procedure **Refine**.

The starting point $\Delta_1^0$ for computing a fixed-point of $\mathcal{H}$ is the set of all refinements of type bindings in $\Delta'$. For example, $\Delta_1^0(S)$ is given by

$$ \left\{ \begin{array}{llll} \wedge \emptyset & \to (q_1, \mathbf{a}), & \wedge \emptyset & \to (q_1, \mathbf{b}), & \wedge \emptyset & \to (q_1, \perp) \\ \wedge \emptyset & \to (q_2, \mathbf{a}), & \wedge \emptyset & \to (q_2, \mathbf{b}), & \wedge \emptyset & \to (q_2, \perp) \\ (q_1, \mathbf{a}) & \to (q_1, \mathbf{a}), & (q_1, \mathbf{a}) & \to (q_1, \mathbf{b}), & (q_1, \mathbf{a}) & \to (q_1, \perp) \\ (q_1, \mathbf{a}) & \to (q_2, \mathbf{a}), & (q_1, \mathbf{a}) & \to (q_2, \mathbf{b}), & (q_1, \mathbf{a}) & \to (q_2, \perp) \\ (q_1, \mathbf{b}) & \to (q_1, \mathbf{a}), & (q_1, \mathbf{b}) & \to (q_1, \mathbf{b}), & (q_1, \mathbf{b}) & \to (q_1, \perp) \\ \vdots & & & & & \\ (q_1, \mathbf{a}) \wedge (q_1, \mathbf{b}) & \to (q_1, \mathbf{a}), & \dots & & & \\ (q_1, \mathbf{a}) \wedge (q_1, \mathbf{b}) \wedge (q_2, \mathbf{a}) & \to (q_1, \mathbf{b}), & \dots & & & \end{array} \right\} $$

since $\Delta'(S) = \{(q, \star) \to (q, \star)\}$. The type $\tau = (q_1, \mathbf{a}) \to (q_2, \mathbf{ab})$ does not belong to $\Delta_1^0(S)$, since $f(\tau) = (q, \star) \to (q, \star\star) \not\subseteq (q, \star) \to (q, \star)$. The set $\Delta_1^0(S)$ contains $2^6 \times 6$ elements, because there are 6 refinements of $(q, \star)$. Similarly, $\Delta_1^0(F_a)$ contains $2^6 \times 18$ elements and $\Delta_1^0(F_b)$ contains $2^{18} \times 6$ elements.

Then we filter out wrong type bindings such as $S : \wedge \emptyset \to (q_1, \mathbf{b}) \in \Delta_1^0$ by iteratively applying $\mathcal{H}$. For example, $S : \wedge \emptyset \to (q_1, \mathbf{b}) \notin \mathcal{H}(\Delta_1^0)$ because $Sx \to x \in \mathcal{R}$ and $\Delta_1^0, x : \wedge \emptyset \not\subseteq_{\mathcal{A}_1} x : (q_1, \mathbf{b})$.

Be repeated applications of $\mathcal{H}$, we obtain the following fixed-point:

$$ \Delta_1 = \left\{ \begin{array}{ll} S : \wedge \left( \left\{ (q_1, B), (q_2, B) \right\} \cup \Theta_1 \right) \to (q_1, B) & B \in \{\mathbf{a}, \mathbf{b}, \perp\} \\ F_a : \wedge \left( \left\{ (q_2, B) \right\} \cup \Theta_1 \right) \to (q_1, B\mathbf{a}) & f(\Theta_1) \subseteq \{(q, \star)\} \\ F_b : \wedge \left( \left\{ (q_1, B\mathbf{b}), (q_2, B\mathbf{b}) \right\} \cup \Theta_2 \right) \to (q_1, B) & f(\Theta_2) \subseteq \{(q, \star\star)\} \end{array} \right\} $$

$\Delta_1$ is an invariant of $\mathcal{R}$ and contains $S: \iota_{\mathcal{A}_1}$. So $\Delta_1$ is a witness and returned by **Refine**. $\square$
We show the correctness and termination of Refine.

**Lemma 4.** Let $M_1$ be a PDA. Given a finite environment $\Delta_1$, a term $t$ and a finite type $\tau$, whether $\Delta_1 \vdash_{M_1}^t \tau$ is decidable.

*Proof.* Induction on the structure of $t$. □

**Lemma 5.** Let $(M_1, \iota_1)$ and $(M_2, \iota_2)$ be PDAs with the initial symbols, $f: (M_1, \iota_1) \to (M_2, \iota_2)$ be a homomorphism and $\Delta_2$ be a finite type environment in $\mathcal{T}_2$. Then the type environment $\Delta_1^0$ defined in Fig. 1 is finite.

*Proof.* We first show that the following two propositions hold for any finite type $\tau_2$ by induction on $\tau_2$: (i) for any type $\tau_1$ in $\mathcal{T}_1$, $f(\tau_1) \subseteq \tau_2$ implies finiteness of $\tau_1$ and (ii) the set $\{\tau_1 \mid f(\tau_1) \subseteq \tau_2\}$ is a finite set. Since there are finitely many type bindings in $\Delta_2$, propositions (i) and (ii) imply finiteness of $\Delta_1^0$. □

**Theorem 5.** Let $\mathcal{G} = (\mathcal{N}, \Sigma, \mathcal{R}, S)$ be a CFG, $(M_1, \iota_1)$ and $(M_2, \iota_2)$ be PDAs with the initial types, $f: (M_1, \iota_1) \to (M_2, \iota_2)$ be a homomorphism and $\Delta_2$ be a finite witness of $\vdash_{M_2}^{\uparrow}(\mathcal{R}, S) : \iota_2$. Then Refine($\mathcal{G}$, $(M_1, \iota_2)$, $(M_2, \iota_2)$, $f, \Delta_2$) always terminates, and returns a witness of $\vdash_{M_1}^{\uparrow}(\mathcal{R}, S) : \iota_1$ if and only if it exists.

*Proof.* First, we show the termination of the step 2 in Figure 1. It is easy to show that $\Delta_1^n$ is a finite type environment by induction on $n$ (for the base case, we use Lemma 5). Thus Lemma 4 implies that we can compute $\mathcal{H}(\Delta_1^n)$. Since $\mathcal{H}$ is decreasing with respect to the set inclusion ordering, i.e., $\mathcal{H}(\Delta_1) \subseteq \Delta_1$ for any environment $\Delta_1$, and $\Delta_1^0$ is a finite set, the fixed-point iteration must terminate. So the procedure Refine terminates.

Let $\Delta'_1$ be a witness of $\vdash_{M_1}^{\uparrow}(\mathcal{R}, S) : \iota_1$. Theorem 4 ensures that we can assume without loss of generality that $f(\Delta'_1) \subseteq \Delta_2$. Thus $\Delta'_1 \subseteq \Delta_1^0$ because $\Delta_1^0$ is the set of all refinement type bindings. By induction on $n$, we have $\Delta'_1 = \mathcal{H}^n(\Delta'_1) \subseteq \mathcal{H}^n(\Delta_1^0) = \Delta_1^n$, since $\Delta'_1$ is a fixed-point of $\mathcal{H}$ and $\mathcal{H}$ is monotonic. So $S: \iota_1 \in \Delta_1^n$ for any $n$, especially $S: \iota_1 \in \Delta_1$. □

# 5 Applications: Some Decidability Results

## 5.1 Balanced Parenthesis and Regular Hedge Languages

Let $\Sigma$ be an alphabet. We define a PDA $\mathcal{B} = (\{q\}, \hat{\Sigma} \cup \tilde{\Sigma}, \Sigma \cup \{\bot\}, \delta)$, where $\delta = \{(q, A, \acute{a}, q, Aa) \mid A \in \Sigma \cup \{\bot\}, a \in \Sigma\} \cup \{(q, a, \acute{a}, q, \varepsilon) \mid a \in \Sigma\}$ with the initial type $\iota_B = (q, \bot) \to (q, \bot)$. Then $\mathcal{L}_B(\iota_B)$ is the set of all balanced tags. For example, $\acute{a}b_1b_1\acute{b}_2b_2\acute{a} \in \mathcal{L}_B(\iota_B)$ and $\acute{b}_1b_2 \notin \mathcal{L}_B(\iota_B)$, where $a, b_1, b_2 \in \Sigma$. It is known that, for a given CFG $\mathcal{G}$, whether $\mathcal{L}_G \subseteq \mathcal{L}_B$ is decidable. Moreover, if $\mathcal{L}_G \subseteq \mathcal{L}_B$, we can construct a finite type environment $\Delta$ such that $\Delta \vdash_B^{\uparrow}(\mathcal{R}, S) : \iota_B$.

Assume that $(M, \iota)$ is a refinement of $(\mathcal{B}, \iota_B)$, i.e., there is $f: (M, \iota) \to (\mathcal{B}, \iota_B)$. Then we can decide $\mathcal{L}_G \subseteq \mathcal{L}_M$ in the following way. First, we decide whether $\mathcal{L}_G \subseteq \mathcal{L}_B$. If not, then $\mathcal{L}_G \not\subseteq \mathcal{L}_M$ by Lemma 3. If $\mathcal{L}_G \subseteq \mathcal{L}_B$, we construct a finite witness $\Delta$ and call Refine($\mathcal{G}$, $(M, \iota)$, $(\mathcal{B}, \iota_B)$, $f, \Delta$).

This argument leads to the following decidability result.
**Theorem 6.** Let $\mathcal{G}$ be a CFG and $M$ be a refinement of $\mathcal{B}$. Then $\mathcal{L}_{\mathcal{G}} \subseteq \mathcal{L}_{M}(\iota)$ is decidable. $\square$

We have the following theorem for the class of refinements of $\mathcal{B}$.

**Theorem 7.** A language is accepted by a refinement of $\mathcal{B}$ if and only if it is a regular hedge language [14].

*Proof.* It is easy to prove using an algebraic representation of a regular hedge language, called binoid [12, 18]. $\square$

The above argument therefore gives a new definition of the class of regular hedge languages and a new decidability proof of the inclusion problem between CFLs and regular hedge languages.

## 5.2 Counting Automata and Superdeterministic Languages

We define the class of PDAs named $C$-machines.

**Definition 4.** A PDA $(M, \iota_M)$ with the initial type is called a $C$-machine if its stack alphabet is singleton and $\iota_M$ is finite. $\square$

A configuration of a $C$-machine is expressed by a pair $(q, n)$ of a state $q$ and a natural number $n$ representing the length of the stack sequence. We define the stack extension $\uparrow m$ for $C$-machines by $(q, n) \uparrow m = (q, n+m)$ and $(\bigwedge \Theta \to c) \uparrow m = \bigwedge \{d \uparrow m \mid d \in \Theta\} \to (c \uparrow m)$.

**Theorem 8.** For a given CFG $\mathcal{G}$ and $C$-machine $(M, \iota_M)$, whether $\mathcal{L}_{\mathcal{G}} \subseteq \mathcal{L}_{M}(\iota_M)$ is decidable. Moreover, when $\mathcal{L}_{\mathcal{G}} \subseteq \mathcal{L}_{M}(\iota_M)$, we can construct a finite type environment $\Delta$ such that $\Delta \vdash_{\uparrow M} (\mathcal{R}, S) : \iota_M$.

*Proof.* We give a proof sketch: See the full version for more detail. For simplicity, we assume that $\iota_M = c_E \to c_S$. Let $c_E = (q_E, n_E)$ and $c_S = (q_S, n_S)$. Let $N$ be a finite-state automaton obtained by removing the counter of $M$, i.e., $q \models_N^a p$ if and only if $(q, n) \models_M^a (p, m)$ for some $n$ and $m$. Roughly speaking, $N$ is an “approximation” of $M$. So we can “refine” a witness in $\mathcal{T}_N$ to a witness in $\mathcal{T}_M$. Since $N$ is finite-state, we can decide whether $\mathcal{L}_{\mathcal{G}} \subseteq \mathcal{L}_{\mathcal{N}}(q_E \to q_S)$. If not, then $\mathcal{L}_{\mathcal{G}} \not\subseteq \mathcal{L}_{\mathcal{M}}(\iota_M)$. Assume $\mathcal{L}_{\mathcal{G}} \subseteq \mathcal{L}_{\mathcal{N}}(q_E \to q_S)$ and let $\Delta_N$ be the minimum witness of $\vdash_N(\mathcal{R}, S) : q_E \to q_S$ (here $\mathcal{T}_N$ is the type system whose base types are states of $N$, instead of configurations).

For a given type binding $F : \bigwedge\{q_1, \dots, q_m\} \to q \in \Delta_N$, we construct a corresponding type binding in $\mathcal{T}_M$. Since $\Delta_N$ is minimum, from the construction of the minimum witness (see the proof of Lemma 1), we have $w \in \text{pre}(F)(=\{v \mid \exists u. S \Rightarrow^* vFu\})$ and $w_i \in \mathcal{L}_G(F)$ ($1 \le i \le m$) such that $q_S \models_N^w q$ and $q \models_N^{w_i} q_i$ for all $i$ (a different choice of $w$ and $w_i$ gives a different upper-bound of witnesses). We define $n$ and $n_i$ by $(q_E, n_E) \models_M^w (q, n)$ and $(q, n) \models_M^{w_i} (q_i, n_i)$. Then the corresponding type binding is $F : \bigwedge\{(q_1, n_1), \dots, (q_m, n_m)\} \to (q, n)$.
Let $\Delta'_M$ be the type environment collecting such type bindings. We define
$\Delta_M = \{F:\tau \mid \exists \sigma, k. F:\sigma \in \Delta'_M$ and $\tau \upharpoonright k = \sigma\}$. Then $\Delta_M$ gives an upper-bound
in the sense that if a witness of $\vdash_M^{\upharpoonright} (\mathcal{R}, S) : \iota_M$ exists, then a witness included
by $\Delta_M$ exists. $\square$

Similarly to the argument in the previous subsection, Theorem 8 leads to the
following decidability result.

**Theorem 9.** For a given context-free grammar $\mathcal{G}$ and a pushdown automaton $M$ which is a refinement of a $C$-machine $N$, whether $\mathcal{L}_{\mathcal{G}} \subseteq \mathcal{L}_M$ is decidable. $\square$

The class of refinements of *C*-machines is closely related to the class of superdeterministic pushdown automata proposed by Greibach and Friedman [5].

**Definition 5 (Superdeterministic PDAs [5]).** A pushdown automaton $M$ is of delay $d$ if for any series of one-step transitions by $\epsilon$, its length is less than or equal to $d$, i.e., if $c_0 \Vdash_M^\epsilon c_1 \Vdash_M^\epsilon \cdots \Vdash_M^\epsilon c_n$ then $n \le d$. A pushdown automaton $M(\iota)$ is superdeterministic if it satisfies the following properties: (1) $M$ is of delay $d$ for some finite number $d$, (2) if $(q, \tilde{A}_1) \Vdash_M^w (p_1, \tilde{B}_1)$ and $(q, \tilde{A}_2) \Vdash_M^w (p_2, \tilde{B}_2)$, then $p_1 = p_2$ and $|\tilde{B}_1| - |\tilde{A}_1| = |\tilde{B}_2| - |\tilde{A}_2|$, here $|\tilde{A}|$ is the length of $A$, and (3) $\iota$ is finite. A language $\mathcal{L}$ is superdeterministic if $\mathcal{L} = \mathcal{L}_M$ for some superdeterministic pushdown automaton $M$. $\square$

The class of refinements of *C*-machines and of superdeterministic PDAs are
incomparable as classes of PDAs. However, they are equally expressive in the
sense that the class of languages accepted by refinements of *C*-machines is equiv-
alent to the one accepted by superdeterministic PDAs.

**Theorem 10.** A language is superdeterministic if and only if it is accepted by a refinement of a *C*-machine.

*Proof.* We give a proof sketch. We first prove the right-to-left direction. A state $q$ of $\mathcal{C}$-machine $\mathcal{C}$ has a $\varepsilon$-loop if there is a sequence of $\varepsilon$-transitions starting from and ending with $q$, i.e., $(q, n) \Vdash_{\mathcal{C}}^{\varepsilon} \cdots \Vdash_{\mathcal{C}}^{\varepsilon} (q, m)$ for some $n$ and $m$. By removing states which have $\varepsilon$-loops, we can construct an equivalent $\mathcal{C}$-machine that is of finite delay. Similarly, we can assume without loss of generality that any refinement of a $\mathcal{C}$-machine is of finite delay. Consider condition (2) in Definition 5. The condition on the stack length must be satisfied by all refinements of $\mathcal{C}$-machines, but the condition on the state may not in general. However we can always construct another refinement that satisfies the condition by moving the refined state information to the stack top, i.e., instead of refining a configuration of the $\mathcal{C}$ machine $(q, n)$ to $(q', A_1 \dots A_n)$, refining it to $(q, \langle A_1, q_1 \rangle \dots \langle A_n, q' \rangle)$. So for all refinements of $\mathcal{C}$-machines, we can construct another refinement which is superdeterministic and accepts the same language.

For the other direction, let $M$ be a superdeterministic PDA and $d$ be its delay.
Note that for any configuration $(q, \tilde{B}A_{d+1} \dots A_1)$, only $d+1$ stack symbols at
the top (i.e., $A_{d+1} \dots A_1$) affect a transition $(q, \tilde{B}\tilde{A}) \Vdash_M^a (q', \tilde{B}\tilde{C})$. So we can
construct another superdeterministic PDA $M'$, whose transition coincides with the transition of $M$ and is normalized as follows:

$$ (q, \tilde{B}\tilde{A}) \Vdash_{M'}^a ((q, a), \tilde{B}\tilde{A}) \\ \Vdash_{M'}^\epsilon ((q, a, A_1), \tilde{B}A_{d+1} \dots A_2) \\ \vdots \\ \Vdash_{M'}^\epsilon ((q, a, \tilde{A}), \tilde{B}) \\ \Vdash_{M'}^\epsilon (q', \tilde{B}\tilde{C}). $$

In the first stage of the transition, $M'$ records $a$ on its state, pops its stack $d$ times and records them on the state. Then the state is a triple of the form $\langle q, a, \tilde{A} \rangle$. In the last stage, $M'$ computes $q'$ and $\tilde{C}$ from its state $\langle q, a, \tilde{A} \rangle$. See the full version for more details about the construction of $M'$.

Let $\mathfrak{h}(\cdot)$ be a mapping which forgets stack symbols such as

$$ \mathfrak{h}((\langle q, a, A_n \dots A_1 \rangle, B_m \dots B_1)) = (\langle q, a, n \rangle, m). $$

The mapping $\mathfrak{h}(\cdot)$ and the transition relation $\delta$ of $M$ induces a transition relation $\mathfrak{h}(\delta)$ of some $C$-machine, which is an approximation of $M$. Condition (2) in Definition 5 ensures that $\mathfrak{h}(\delta)$ is deterministic. $\square$

The decidability of the inclusion problem between context-free languages and superdeterministic languages has been proved by Greibach and Friedman [5]. The proof of Theorem 9 with Theorem 10 is an alternative and arguably simpler proof of the result.

# 6 Related Work

There have been a number of studies on the inclusion problems for subclasses of context-free languages (see [3] for a survey).

One of the strongest decidability results is about the inclusion between context-free languages and superdeterministic languages, proved by Greibach and Friedman [5]. Nguyen and Ogawa [15] gave a new proof by simplifying the technique used in [5]. Greibach and Friedman [5] reduced the problem to the emptiness problem for a pushdown automaton and Nguyen and Ogawa [15] gave simpler construction of a pushdown automaton.

Minamide and Tozawa [12] have proposed an algorithm for inclusion between context-free languages and regular hedge languages, motivated by the validation of dynamically generated HTML documents. As demonstrated in Section 5.1, our method gives an alternative algorithm for the same problem, although our algorithm may not be as efficient as Minamide and Tozawa's. Møller and Schwarz [13] have developed an algorithm to validate a context-free grammar against SGML DTDs, dealing with tag omissions and exceptions. It is not clear whether our method can provide a similar result.
The subclass of the context-free languages named *visibly pushdown languages* [1, 2] has many good properties such as boolean closure and decidability of the emptiness problem in polynomial time. Some researchers have extended the class preserving such properties. Caucal [4] has introduced a notion of *synchronized pushdown automata* and Nowotka and Srba [16] have proposed *height-deterministic pushdown automata*. The refinement of a counter machine is similar to those notions. Since the class of visibly pushdown automata can be defined as the class of refinements of a certain automaton, our notion of refinements may give an extension of them.

Recently, type-based approaches to model-checking, verification and language inclusion problems have been extensively studied [7–9, 11, 19, 20]. Kobayashi and Ong [7, 9] have proposed a type system for recursion schemes that is equivalent to the modal μ-calculus model-checking of recursion schemes (the decidability of the model-checking problem has been proved by Ong [17]). These type systems have been applied to verification of higher-order programs [7, 11, 10], and practically effective typability checkers have been developed [6, 8]. The present work extends type systems to deal with infinite state systems, namely deterministic pushdown automata. Types are now configurations of pushdown automata, rather than states of automata, which are finite a priori.

In our previous work [20], we gave a type-based proof for the inclusion problem between context-free languages and superdeterministic languages. But the proof is specific to superdeterministic languages, and difficult to generalize.

# 7 Conclusion and Future Work

We have proposed an intersection type system characterizing the inclusion by a deterministic context-free language, and given a sufficient condition of decidability of its typability. Future work includes extensions in two directions, extending grammars and automata. A naive extension to higher-order recursion schemes fails to establish the counterpart of Theorem 4. That is because the up-to technique used in this paper is too crude to deal with them. To extend automata is easier than grammars. For example, we can develop a framework for higher-order pushdown automata. So what we should do is to find a language accepted by a higher-order pushdown automaton which has decidable inclusion problem and a practical use.

**Acknowledgement.** The authors would like to thank the anonymous reviewers for their valuable comments. This work is partially supported by Kakenhi 23220001 and 22-3842.

# References

1. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC. pp. 202–211. ACM (2004)
2. Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 1–43 (2009)

3. Asveld, P.R.J., Nijholt, A.: The inclusion problem for some subclasses of context-free languages. Theor. Comput. Sci. 230(1-2), 247–256 (2000)

4. Caucal, D.: Synchronization of pushdown automata. In: Ibarra, O.H., Dang, Z. (eds.) Developments in Language Theory. Lecture Notes in Computer Science, vol. 4036, pp. 120–132. Springer (2006)

5. Greibach, S.A., Friedman, E.P.: Superdeterministic PDAs: A subcase with a decidable inclusion problem. J. ACM 27(4), 675–700 (1980)

6. Kobayashi, N.: Model-checking higher-order functions. In: Porto, A., López-Fraguas, F.J. (eds.) PPDP. pp. 25–36. ACM (2009)

7. Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Shao, Z., Pierce, B.C. (eds.) POPL. pp. 416–428. ACM (2009)

8. Kobayashi, N.: A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In: FoSSaCS. pp. 260–274. Springer (2011)

9. Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS. pp. 179–188. IEEE Computer Society (2009)

10. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) PLDI. pp. 222–233. ACM (2011)

11. Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL. pp. 495–508. ACM (2010)

12. Minamide, Y., Tozawa, A.: XML validation for context-free grammars. In: Kobayashi, N. (ed.) APLAS. Lecture Notes in Computer Science, vol. 4279, pp. 357–373. Springer (2006)

13. Møller, A., Schwarz, M.: HTML validation of context-free languages. In: FoSSaCS, pp. 426–440. Springer (2011)

14. Murata, M.: Hedge automata: a formal model for XML schemata (1999), http://www.xml.gr.jp/relax/hedge_nice.html

15. Nguyen, V.T., Ogawa, M.: Alternate stacking technique revisited: Inclusion problem of superdeterministic pushdown automata. IPSJ Transactions on Programming 1(1), 36–46 (2008)

16. Nowotka, D., Srba, J.: Height-deterministic pushdown automata. In: Kucera, L., Kucera, A. (eds.) MFCS. Lecture Notes in Computer Science, vol. 4708, pp. 125–134. Springer (2007)

17. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS. pp. 81–90. IEEE Computer Society (2006)

18. Pair, C., Quéré, A.: Définition et étude des bilangages réguliers. Information and Control 13(6), 565–593 (1968)

19. Tsukada, T., Kobayashi, N.: Untyped recursion schemes and infinite intersection types. In: Ong, C.H.L. (ed.) FOSSACS. Lecture Notes in Computer Science, vol. 6014, pp. 343–357. Springer (2010)

20. Tsukada, T., Kobayashi, N.: A type-theoretic proof of the decidability of the language containment between context-free languages and superdeterministic languages (in japanese). IPSJ Transactions on Programming 4(2), 31–47 (2011)