文脈依存言語

規則 $\gamma A\delta\to\gamma\alpha\delta$ について、$|\gamma A\delta|=|\gamma|+1+|\delta|$、$|\gamma\alpha\delta|=|\gamma|+|\alpha|+|\delta|$ であり、$\alpha\ne\varepsilon$ より $|\alpha|\ge1$ なので $|\gamma A\delta|\le|\gamma\alpha\delta|$ である。非収縮文法では定義そのものである。一歩 $\gamma'\alpha\delta'\Rightarrow\gamma'\beta\delta'$ で長さは $|\beta|-|\alpha|\ge0$ だけ変わるので、長さの列は単調非減少である。最後に、$S\to\varepsilon$ を含む文法では $S$ は右辺に現れないので、$S$ が現れる文字列は導出の最初の $S$ だけである。$S\to\varepsilon$ をこれに適用すると $\varepsilon$ になり、$\varepsilon$ からは何も導出できない。よって $w\ne\varepsilon$ の導出では $S\to\varepsilon$ は使われない。

（$\supset$）$n\ge1$ とする。$S\to aSBC$ を $n-1$ 回、$S\to aBC$ を $1$ 回適用して $S\Rightarrow^{*}a^{n}(BC)^{n}$ を得る。$CB\to BC$ を繰り返して、$C$ の右にある $B$ を順に左へ移せば $a^{n}B^{n}C^{n}$ になる（$C$ の右にある $B$ の個数の和は各適用で $1$ 減るので有限回で終わる）。次に $aB\to ab$ を $1$ 回、$bB\to bb$ を $n-1$ 回適用して $a^{n}b^{n}C^{n}$、$bC\to bc$ を $1$ 回、$cC\to cc$ を $n-1$ 回適用して $a^{n}b^{n}c^{n}$ を得る（句構造言語 の記事の命題（導出の文脈への代入合致性）により、部分文字列の書き換えは全体の中で実行できる）。
（$\subset$）$S$ から導出されるすべての文字列 $\theta$ について、次の三つが成り立つことを導出の長さに関する帰納法で示す。記号 $x$ の $\theta$ における出現回数を $\#_x(\theta)$ と書く。

1. $\#_a(\theta)=\#_B(\theta)+\#_b(\theta)=\#_C(\theta)+\#_c(\theta)$。
2. $\theta=a^{k}\mu$ または $\theta=a^{k}S\mu$（$k\in\mathbb{N}$、$\mu\in\{B,C,b,c\}^{*}$）の形をしている。すなわち $a$ はすべて左端にあり、$S$ があればその直後に、$S$ がなければ $a$ の直後に $\{B,C,b,c\}$ 上の文字列が続く。
3. 2 の $\mu$ は $\mu=\nu\rho$、$\nu\in\{b,c\}^{*}$、$\rho\in\{B,C\}^{*}$ と書け、$\nu\in b^{*}c^{*}$ である。さらに $S$ が現れるときは $\nu=\varepsilon$ である。
   $\theta=S$ ではすべて成り立つ（$k=0$、$\mu=\varepsilon$）。各規則の適用がこれらを保つことを確かめる。$S\to aSBC$、$S\to aBC$：1 について $a,B,C$ が一つずつ増える。2 について、$S$ は $a^{k}$ の直後にあるので、適用後は $a^{k+1}SBC\mu$ または $a^{k+1}BC\mu$ の形になる。3 について、適用前に $S$ があるので $\nu=\varepsilon$、すなわち $\mu=\rho\in\{B,C\}^{*}$ であり、適用後の $\mu'=BC\rho$ も $\{B,C\}^{*}$ の元で、$S$ が残るなら $\nu'=\varepsilon$ のままである。$CB\to BC$：1 は変わらず、$\mu$ の中の $\rho$ の内部の書き換えなので 2、3 も保たれる（$\nu$ には $C,B$ が含まれないので、左辺 $CB$ の出現は $\rho$ の中にある）。$aB\to ab$：左辺の $a$ は $a^{k}$ の最後の $a$ であり、その直後が $B$ であることから $S$ はなく $\mu=B\rho'$、$\nu=\varepsilon$ である。適用後は $\nu'=b\in b^{*}c^{*}$、$\rho'$ はそのままで、1 も $B$ が一つ減り $b$ が一つ増えるだけで保たれる。$bB\to bb$：$b$ の直後の $B$ は $\rho$ の先頭であり、$\nu$ の末尾が $b$ なので $\nu\in b^{*}$ であり、$\nu'=\nu b\in b^{*}$。$bC\to bc$：同様に $\nu\in b^{*}$ で $\nu'=\nu c\in b^{*}c^{*}$。$cC\to cc$：$\nu$ の末尾が $c$ なので $\nu\in b^{*}c^{+}$ で $\nu'=\nu c\in b^{*}c^{*}$。1 はいずれも大文字が一つ減り対応する小文字が一つ増えるだけで保たれる。
   終端文字列 $w\in L(G)$ では $S$ も $B,C$ も現れないので、2、3 により $w=a^{k}\nu$、$\nu\in b^{*}c^{*}$、すなわち $w=a^{k}b^{i}c^{j}$ であり、1 により $k=i=j$ である。また $S$ を消すには $S\to aBC$ を使う必要があるので $k\ge1$ である。よって $w\in\{a^{n}b^{n}c^{n}\mid n\ge1\}$。

$L$ を文脈自由言語とする。文脈自由言語 の記事の命題（空語規則の除去）により、$L=L(G')$ となる文脈自由文法 $G'=(V,\Sigma,R',S')$ で、$\varepsilon$ 規則が高々 $S'\to\varepsilon$ だけであり、それがあるのは $\varepsilon\in L$ のときに限り、$S'$ がどの規則の右辺にも現れないものがとれる。$R'$ の $S'\to\varepsilon$ 以外の各規則 $A\to\alpha$ は $\alpha\ne\varepsilon$ を満たすので、$\gamma=\delta=\varepsilon$ とおいた文脈依存文法の規則 $\gamma A\delta\to\gamma\alpha\delta$ である。$S'\to\varepsilon$ があれば、それは文脈依存文法の空語の規約をちょうど満たす。よって $G'$ はそのまま文脈依存文法であり、導出と生成言語の定義は同じであるから $L=L(G')$ は文脈依存言語である。逆が成り立たないことは ex-context-sensitive-language-anbncn と prop-context-sensitive-language-anbncn による。

$w=\varepsilon$ の場合：prop-context-sensitive-language-nondecreasing により、$S\to\varepsilon$ 以外の規則は長さを減らさないので、$\varepsilon$ に至る導出は最初の $S$ に直接 $S\to\varepsilon$ を適用するものに限る（$S$ が長さ $2$ 以上の文字列の一部になった後は、$S\to\varepsilon$ を適用しても長さ $1$ 以上の文字列が残り、以後長さは減らない。また $S$ は右辺に現れないので、$S$ 以外の長さ $1$ の文字列から $S$ に戻ることもない）。よって $\varepsilon\in L(G)$ であることは $S\to\varepsilon\in R$ と同値であり、有限の検査で判定できる。
$w\ne\varepsilon$ の場合：$n:=|w|$ とおく。同じ命題により、$S\Rightarrow^{*}w$ の導出は $S\to\varepsilon$ を使わず、途中に現れる文字列の長さはすべて $n$ 以下である。$V\cup\Sigma$ 上の長さ $n$ 以下の文字列全体 $\Gamma_n$ は有限集合であり、$\eta,\theta\in\Gamma_n$ について $\eta\Rightarrow\theta$ かどうかは、$\eta$ の各部分文字列と $R$ の各規則の左辺を比べればよいので有限の手続きで決まる。したがって $\Gamma_n$ を頂点、$\Rightarrow$ を辺とする有限の有向グラフが構成でき、$w\in L(G)$ は「このグラフで $S$ から $w$ に到達できる」ことと同値である。有限グラフの到達可能性は、$S$ から到達できる頂点の集合を辺をたどって順に拡げていく（既に加えた頂点は再訪しない）ことで有限回で計算できる。