著者

塚田 武志 小林 直樹

出版者

情報処理学会

雑誌

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

巻号頁・発行日

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

---

言語の包含判定問題とは,与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり,理論的な興味の対象であるだけでなく,プログラム検証などへの広い応用を持つ重要な問題である.この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である.このオリジナルの証明は,Greibach と Friedman によって与えられている.我々はこの問題に対して,小林らによって提案されている型に基づく言語の包含判定の手法を適用し,決定可能性に対する別証明を与えた.この手法は以下のような利点を持つ.(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる.(2) 型推論を効率的に行う方法は多数提案されており,それらを利用することができる.また,提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり,その他の非正規言語クラスへの応用も期待される.The language containment problem, which asks whether L1 ⊆ L2 for given languages L1 and L2, is an important problem in the field of formal language theory and has a variety of applications including program verification. One of the strongest result about this problem is the decidability for the case where L1 and L2 are context free and superdeterministic languages respectively, originally proved by Greibach and Friedman. In this paper, we give a new proof of the decidability, inspired by Kobayashi's type-based approach to language containment problems. The new proof has the following advantages. (1) The key notions and lemmas in the proof are well-known ones, such as subtyping and Pumping Lemma. (2) We can apply well-studied techniques for efficient typability checking. Furthermore, our proof is the first application of the type-based approach to the inclusion between non-regular languages and it seems applicable to other cases.