著者

塚田 武志 小林 直樹

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.4, no.2, pp.31-47, 2011-03-25

---

言語の包含判定問題とは,与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり,理論的な興味の対象であるだけでなく,プログラム検証などへの広い応用を持つ重要な問題である.この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である.このオリジナルの証明は,Greibach と Friedman によって与えられている.我々はこの問題に対して,小林らによって提案されている型に基づく言語の包含判定の手法を適用し,決定可能性に対する別証明を与えた.この手法は以下のような利点を持つ.(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる.(2) 型推論を効率的に行う方法は多数提案されており,それらを利用することができる.また,提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり,その他の非正規言語クラスへの応用も期待される.