再帰的データ型の包含性の判定、わかった
結局、分かった後から眺めれば、正規表現型のときと事情は同じだ。あからさまに（陽に）正規表現を使ってなくても、再帰的な定義を入れれば、結局は正規言語になる。「再帰的データ型（の領域）＝正規言語」と言ってよいから、正規表現型の導入と再帰的なデータ型の導入は同じこと。だから、やることも同じ。
次の3つの問題が同じなのだ。
- 集合の包含性の判定
- オーマトンの模倣の存在を示す
- 無限正規木の埋め込み可能性の判定
包含性の判定をそのままやるのは難しい。論理計算に持ち込む方法として、ホヴランド（Hovland）のアルゴリズムとかコゥゼン（Kozen）の集合制約（set constraints）の解法とかあるが、難しいし効率も芳しくない。
制限（明瞭性）を付けてオーマトン（あるいは余代数）の模倣構成問題にしたほうがやさしいし高速な解法がある。それが1年弱前に考えていた拡張ダイクストラ法。
今回も状況は同じだから拡張ダイクストラ法が使える。一般的な明瞭オートマトンに比べると、サイクル付きの林の形をしているので少し扱いやすい。有限な状態空間のあいだの関係をビット行列として作っていく方法。林のリーフノード全体の集合が終状態となる。
すべてのノードをくまなくチェックしたことの確認が難しい。全体として木の形をしているから、普通の深さ優先探索順序でスキャンしていけば良いと思われるが、ループのところでもうまく処理できるかを確認しないと。
工夫の余地はあるが、大筋は大丈夫そうだ。
