WEKO3
-
RootNode
アイテム
文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明
https://ipsj.ixsq.nii.ac.jp/records/73762
https://ipsj.ixsq.nii.ac.jp/records/7376268114727-6541-48a2-a35e-19cbc8f7a429
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO0402004.pdf (397.0 kB)
|
Copyright (c) 2011 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2011-03-25 | |||||||
| タイトル | ||||||||
| タイトル | 文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Type-theoretic Proof of the Decidability of the Language Containment between Context-free Languages and Superdeterministic Languages | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 通常論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 東北大学大学院情報科学研究科／日本学術振興会特別研究員DC | ||||||||
| 著者所属 | ||||||||
| 東北大学大学院情報科学研究科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Tohoku University / JSPS Research Fellow | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Tohoku University | ||||||||
| 著者名 |
塚田, 武志
小林, 直樹
× 塚田, 武志 小林, 直樹
|
|||||||
| 著者名(英) |
Takeshi, Tsukada
Naoki, Kobayashi
× Takeshi, Tsukada Naoki, Kobayashi
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 言語の包含判定問題とは，与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり，理論的な興味の対象であるだけでなく，プログラム検証などへの広い応用を持つ重要な問題である．この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である．このオリジナルの証明は，Greibach と Friedman によって与えられている．我々はこの問題に対して，小林らによって提案されている型に基づく言語の包含判定の手法を適用し，決定可能性に対する別証明を与えた．この手法は以下のような利点を持つ．(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる．(2) 型推論を効率的に行う方法は多数提案されており，それらを利用することができる．また，提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり，その他の非正規言語クラスへの応用も期待される． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 4, 号 2, p. 31-47, 発行日 2011-03-25 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
