プッシュダウンオートマトン

$n$ に関する帰納法により、一歩の場合を示せばよい。$(q,aw_1,X\alpha_1)\vdash(p,w_1,\gamma\alpha_1)$ が遷移 $(q,a,X,p,\gamma)$ による一歩なら、同じ遷移を様相 $(q,aw_1x,X\alpha_1\beta)$ に適用して $(p,w_1x,\gamma\alpha_1\beta)$ を得る。一歩の定義は一番上の記号と入力の先頭の記号しか見ないので、後ろに $x$、底に $\beta$ を付け足しても適用できる。

$k$ に関する帰納法。$k=1$ なら $p_1=r$、$w_1=w$、$n_1=n$ でよい。$k\ge2$ とし、計算を $C_0\vdash C_1\vdash\cdots\vdash C_n$、$C_i=(q_i,u_i,\gamma_i)$ と書く。$\gamma_0=X_1\cdots X_k$、$\gamma_n=\varepsilon$ である。一歩でスタックの長さは高々 $1$ しか減らない（一番上の記号を一つ取り除き、文字列を積む）ので、$|\gamma_t|\le k-1$ となる最小の $t$ が存在し、$1\le t\le n$、$|\gamma_t|=k-1$ である。
$i\le t$ について $\gamma_i=\delta_iX_2\cdots X_k$ と書け、$i< t$ なら $\delta_i\ne\varepsilon$、$i=t$ なら $\delta_t=\varepsilon$ であることを $i$ に関する帰納法で示す。$i=0$ では $\delta_0=X_1$。$i< t$ で $\gamma_i=\delta_iX_2\cdots X_k$、$\delta_i\ne\varepsilon$ なら、一歩 $C_i\vdash C_{i+1}$ は $\delta_i$ の先頭の記号を取り除いて文字列 $\gamma$ を積むので、$\gamma_{i+1}=\delta_{i+1}X_2\cdots X_k$（$\delta_{i+1}$ は $\delta_i$ の先頭を $\gamma$ に置き換えたもの）である。$i+1< t$ なら $t$ の最小性により $|\gamma_{i+1}|\ge k$ なので $\delta_{i+1}\ne\varepsilon$、$i+1=t$ なら $|\gamma_t|=k-1$ なので $\delta_t=\varepsilon$ である。
各一歩は未読の入力から先頭の高々一記号を取り除くだけなので、$u_0=w_1u_t$ となる $w_1$ があり、各 $i\le t$ について $u_i=v_iu_t$（$v_i$ は時刻 $i$ から $t$ までに読む部分）と書ける。時刻 $i< t$ の一歩は、一番上の記号（$\delta_i$ の先頭）と、読むなら $v_i$ の先頭の記号しか使わないので、底の $X_2\cdots X_k$ と入力の残り $u_t$ を取り去った $(q_i,v_i,\delta_i)\vdash(q_{i+1},v_{i+1},\delta_{i+1})$ も同じ遷移による一歩である。よって $(p,w_1,X_1)\vdash^{t}(q_t,\varepsilon,\varepsilon)$ が成り立つ。$p_1:=q_t$、$n_1:=t$ とおくと、残りの計算は $(p_1,u_t,X_2\cdots X_k)\vdash^{n-t}(r,\varepsilon,\varepsilon)$ であり、長さ $k-1$ の場合の帰納法の仮定から $p_2,\ldots,p_k$、$w_2,\ldots,w_k$、$n_2,\ldots,n_k$ が得られる。

$P=(Q,\Sigma,\Gamma,\delta,q_0,Z_0,F)$ とし、新しい状態 $s,e,g\notin Q$ と新しいスタック記号 $X_0\notin\Gamma$ をとる。
（$L(P)$ を空スタックで受理する機械）$P':=(Q\cup\{s,e\},\Sigma,\Gamma\cup\{X_0\},\delta',s,X_0,\emptyset)$ とし、$\delta'$ は $\delta$ に、$(s,\varepsilon,X_0,q_0,Z_0X_0)$ と、各 $f\in F\cup\{e\}$、$Y\in\Gamma\cup\{X_0\}$ についての $(f,\varepsilon,Y,e,\varepsilon)$ を加えたものとする。$w\in L(P)$ で $(q_0,w,Z_0)\vdash^{*}(f,\varepsilon,\alpha)$ なら、lem-pda-extend により $P'$ で
$$(s,w,X_0)\vdash(q_0,w,Z_0X_0)\vdash^{*}(f,\varepsilon,\alpha X_0)\vdash^{*}(e,\varepsilon,\varepsilon)$$
（最後は状態 $f$、$e$ からの $\varepsilon$ 遷移で一記号ずつ降ろす）となり $w\in N(P')$。逆に $w\in N(P')$ とし、空スタックに至る $P'$ の計算をとる。最初の一歩は $(q_0,w,Z_0X_0)$ に移るもので、記号 $X_0$ を取り除けるのは状態 $F\cup\{e\}$ からの新しい遷移だけであり、状態 $e$ に入るのもそれらの遷移だけである。そこで状態 $e$ に初めて入る時刻を考えると、それまでの各様相は $(q,u,\alpha X_0)$（$q\in Q$）の形で、$\delta$ の遷移による一歩は $\alpha\ne\varepsilon$ の一番上の記号だけを使うので、$P$ の計算 $(q_0,w,Z_0)\vdash^{*}(q,u,\alpha)$ を与える。$e$ に入る一歩はある $f\in F$ の様相 $(f,u,\alpha X_0)$ からの $\varepsilon$ 遷移であり、その後は状態 $e$ の $\varepsilon$ 遷移しか使えないので入力は読まれず、$u=\varepsilon$ である。よって $(q_0,w,Z_0)\vdash^{*}(f,\varepsilon,\alpha)$、$w\in L(P)$。
（$N(P)$ を受理状態で受理する機械）$P'':=(Q\cup\{s,g\},\Sigma,\Gamma\cup\{X_0\},\delta'',s,X_0,\{g\})$ とし、$\delta''$ は $\delta$ に、$(s,\varepsilon,X_0,q_0,Z_0X_0)$ と、各 $q\in Q$ についての $(q,\varepsilon,X_0,g,\varepsilon)$ を加えたものとする。$(q_0,w,Z_0)\vdash^{*}(q,\varepsilon,\varepsilon)$ なら $(s,w,X_0)\vdash(q_0,w,Z_0X_0)\vdash^{*}(q,\varepsilon,X_0)\vdash(g,\varepsilon,\varepsilon)$ である。逆に $(s,w,X_0)\vdash^{*}(g,\varepsilon,\beta)$ とすると、$g$ に入る一歩は様相 $(q,u,X_0)$（$q\in Q$）からのものであり、それまでの様相は $(q',u',\alpha X_0)$ の形で、$\delta$ の遷移は $\alpha\ne\varepsilon$ のときしか適用できない。前段と同じく $P$ の計算 $(q_0,w,Z_0)\vdash^{*}(q,u,\varepsilon)$ が得られ、$g$ からの遷移はないので $u=\varepsilon$ である。よって $w\in N(P)$。

$X=a\in\Sigma$ のときは、終端記号に適用できる規則はないので $a\Rightarrow^{*}w$ は $w=a$ と同値である。一方 $(q,w,a)$ から適用できる遷移は $(q,a,a,q,\varepsilon)$ だけ（変数記号を置き換える遷移は一番上が変数記号のときに限る）なので、空スタックに至るのは $w=a$ のとき、一歩で $(q,\varepsilon,\varepsilon)$ に至る場合に限る。よって主張は成り立つ。以下 $X=A\in V$ とする。
（$\Rightarrow$）$A\Rightarrow^{*}w$ とすると、文脈自由言語 の記事の補題「構文木と導出の対応」により、$A$ を根とし生成文字列が $w$ の完全な構文木がある。その頂点数に関する帰納法で $(q,w,A)\vdash^{*}(q,\varepsilon,\varepsilon)$ を示す。根で使われる規則を $A\to X_1\cdots X_k$ とする。$k=0$（規則 $A\to\varepsilon$）なら $w=\varepsilon$ で、遷移 $(q,\varepsilon,A,q,\varepsilon)$ の一歩で空スタックに至る。$k\ge1$ なら、根の子 $X_i$ を根とする部分木の生成文字列を $w_i$ として $w=w_1\cdots w_k$ であり、$X_i$ が変数記号ならその部分木はより頂点数の少ない完全な構文木なので帰納法の仮定により、$X_i$ が終端記号なら前段により、$(q,w_i,X_i)\vdash^{*}(q,\varepsilon,\varepsilon)$ である。lem-pda-extend を使ってこれらをつなぐと
$$(q,w,A)\vdash(q,w_1\cdots w_k,X_1\cdots X_k)\vdash^{*}(q,w_2\cdots w_k,X_2\cdots X_k)\vdash^{*}\cdots\vdash^{*}(q,\varepsilon,\varepsilon)$$
となる。
（$\Leftarrow$）$(q,w,A)\vdash^{n}(q,\varepsilon,\varepsilon)$ の長さ $n$ に関する帰納法。スタックは空でないので $n\ge1$ であり、一番上が変数記号 $A$ なので最初の一歩はある規則 $A\to\alpha$ に対応する遷移 $(q,\varepsilon,A,q,\alpha)$ による。よって $(q,w,\alpha)\vdash^{n-1}(q,\varepsilon,\varepsilon)$。$\alpha=\varepsilon$ なら、空スタックからは進めないので $n-1=0$、$w=\varepsilon$ であり、$A\Rightarrow\varepsilon$ である。$\alpha=X_1\cdots X_k$（$k\ge1$）なら、lem-pda-split（状態は $q$ だけ）により $w=w_1\cdots w_k$、$(q,w_i,X_i)\vdash^{n_i}(q,\varepsilon,\varepsilon)$、$n_1+\cdots+n_k=n-1$ と書ける。各 $X_i$ について、終端記号なら前段により、変数記号なら $n_i< n$ なので帰納法の仮定により、$X_i\Rightarrow^{*}w_i$ である。句構造言語 の記事の命題「導出の文脈への代入合致性」によりこれらを並べて、$A\Rightarrow X_1\cdots X_k\Rightarrow^{*}w_1\cdots w_k=w$ を得る。
最後に $X=S$ とおけば、$w\in L(G)\iff S\Rightarrow^{*}w\iff(q,w,S)\vdash^{*}(q,\varepsilon,\varepsilon)\iff w\in N(P_G)$ である。

$Q,\Gamma,\delta$ が有限なので $V$ と $R$ は有限であり、各規則の左辺は一つの変数記号だから $G_P$ は文脈自由文法である。
（$\Leftarrow$）$(p,w,X)\vdash^{n}(q,\varepsilon,\varepsilon)$ の長さ $n\ge1$ に関する帰納法。最初の一歩の遷移を $(p,a,X,r,Y_1\cdots Y_k)$ とすると、$w=aw'$ で $(r,w',Y_1\cdots Y_k)\vdash^{n-1}(q,\varepsilon,\varepsilon)$ である。$k=0$ なら、空スタックからは進めないので $n-1=0$、$w'=\varepsilon$、$r=q$ であり、規則 $[pXq]\to a$ により $[pXq]\Rightarrow a=w$。$k\ge1$ なら、lem-pda-split により状態 $r=r_0,r_1,\ldots,r_k=q$ と $w'=w_1\cdots w_k$ があって $(r_{i-1},w_i,Y_i)\vdash^{n_i}(r_i,\varepsilon,\varepsilon)$、$n_i\le n-1$ となる。帰納法の仮定により $[r_{i-1}Y_ir_i]\Rightarrow^{*}w_i$ であり、この状態の列に対応する規則 $[pXq]\to a[r_0Y_1r_1]\cdots[r_{k-1}Y_kr_k]$ があるので、句構造言語 の記事の命題「導出の文脈への代入合致性」により $[pXq]\Rightarrow a[r_0Y_1r_1]\cdots[r_{k-1}Y_kr_k]\Rightarrow^{*}aw_1\cdots w_k=w$ である。
（$\Rightarrow$）$[pXq]\Rightarrow^{*}w$ とし、文脈自由言語 の記事の補題「構文木と導出の対応」により $[pXq]$ を根とし生成文字列 $w$ の完全な構文木をとって、その頂点数に関する帰納法で示す。根で使われる規則は、ある遷移 $(p,a,X,r,Y_1\cdots Y_k)$ と状態の列 $r_1,\ldots,r_k$（$r_k=q$、$k=0$ なら $r=q$）から作られたものである。$k=0$ なら $w=a$ であり、その遷移の一歩で $(p,a,X)\vdash(q,\varepsilon,\varepsilon)$ となる。$k\ge1$ なら、子 $[r_{i-1}Y_ir_i]$ を根とする部分木の生成文字列を $w_i$ として $w=aw_1\cdots w_k$ であり、帰納法の仮定により $(r_{i-1},w_i,Y_i)\vdash^{*}(r_i,\varepsilon,\varepsilon)$ である。lem-pda-extend でつないで
$$(p,aw_1\cdots w_k,X)\vdash(r_0,w_1\cdots w_k,Y_1\cdots Y_k)\vdash^{*}(r_1,w_2\cdots w_k,Y_2\cdots Y_k)\vdash^{*}\cdots\vdash^{*}(r_k,\varepsilon,\varepsilon)$$
を得る。$r_k=q$ なので主張が成り立つ。
最後に、$S$ の規則は $S\to[q_0Z_0q]$ だけなので、$w\in L(G_P)$ は「ある $q$ について $[q_0Z_0q]\Rightarrow^{*}w$」と同値であり、これは「ある $q$ について $(q_0,w,Z_0)\vdash^{*}(q,\varepsilon,\varepsilon)$」、すなわち $w\in N(P)$ と同値である。

1 から 2 は prop-pda-from-grammar による（そこで作る $P_G$ は状態が一つである）。2 から 1 は prop-pda-to-grammar による。2 と 3 の同値は prop-pda-final-empty による。

thm-pda-cfg により $L=L(P)$ となる $P=(Q,\Sigma,\Gamma,\delta,q_0,Z_0,F)$ がある。正規言語 の記事の命題「右線形文法と有限オートマトンの同値性」と 有限オートマトン の記事の命題「部分集合構成」により、$M$ を受理する決定性有限オートマトン $D=(Q_D,\Sigma,\eta,s_0,F_D)$（$\eta\colon Q_D\times\Sigma\to Q_D$ は写像）がある。$\eta(s,\varepsilon):=s$ と約束し、$\eta$ を文字列に拡張したものも $\eta$ と書く。
$$P':=(Q\times Q_D,\Sigma,\Gamma,\delta',(q_0,s_0),Z_0,F\times F_D),\qquad\delta':=\{\,((q,s),a,X,(p,\eta(s,a)),\gamma)\mid(q,a,X,p,\gamma)\in\delta,\ s\in Q_D\,\}$$
とおく。$n$ に関する帰納法により、
$$((q_0,s_0),w,Z_0)\vdash_{P'}^{n}((q,s),u,\alpha)\iff(q_0,w,Z_0)\vdash_{P}^{n}(q,u,\alpha)\text{ かつ }w=vu,\ s=\eta(s_0,v)\text{ となる }v\text{ がある}$$
が成り立つ。実際 $n=0$ では両辺とも $(q,s,u,\alpha)=(q_0,s_0,w,Z_0)$ を意味し、一歩進めるときは $P'$ の遷移が $P$ の遷移と一対一に対応し、読んだ記号 $a$（$\varepsilon$ でもよい）に応じて第二成分が $\eta(s,a)$ に変わる。読み終えた部分 $v$ に $a$ を付け足すと $\eta(s_0,va)=\eta(\eta(s_0,v),a)$ となるので、対応が保たれる。よって $w\in L(P')$ は、ある計算 $(q_0,w,Z_0)\vdash^{*}(f,\varepsilon,\alpha)$（$f\in F$）があって $\eta(s_0,w)\in F_D$ となること、すなわち $w\in L(P)\cap L(D)=L\cap M$ と同値である。