{"id":73762,"updated":"2025-01-21T21:49:01.135741+00:00","links":{},"created":"2025-01-18T23:31:34.933458+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00073762","sets":["934:935:6375:6387"]},"path":["6387"],"owner":"11","recid":"73762","title":["文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明"],"pubdate":{"attribute_name":"公開日","attribute_value":"2011-03-25"},"_buckets":{"deposit":"37c9aa46-db01-4e3c-a858-fd8f632ac55e"},"_deposit":{"id":"73762","pid":{"type":"depid","value":"73762","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明"},{"subitem_title":"A Type-theoretic Proof of the Decidability of the Language Containment between Context-free Languages and Superdeterministic Languages","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"通常論文","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2011-03-25","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"東北大学大学院情報科学研究科／日本学術振興会特別研究員DC"},{"subitem_text_value":"東北大学大学院情報科学研究科"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Graduate School of Information Science, Tohoku University / JSPS Research Fellow","subitem_text_language":"en"},{"subitem_text_value":"Graduate School of Information Science, Tohoku University","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/73762/files/IPSJ-TPRO0402004.pdf"},"date":[{"dateType":"Available","dateValue":"2013-03-25"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO0402004.pdf","filesize":[{"value":"397.0 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"d08ecf1e-de92-4d7c-9835-faa51622f9b6","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2011 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"塚田, 武志"},{"creatorName":"小林, 直樹"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Takeshi, Tsukada","creatorNameLang":"en"},{"creatorName":"Naoki, Kobayashi","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"言語の包含判定問題とは，与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり，理論的な興味の対象であるだけでなく，プログラム検証などへの広い応用を持つ重要な問題である．この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である．このオリジナルの証明は，Greibach と Friedman によって与えられている．我々はこの問題に対して，小林らによって提案されている型に基づく言語の包含判定の手法を適用し，決定可能性に対する別証明を与えた．この手法は以下のような利点を持つ．(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる．(2) 型推論を効率的に行う方法は多数提案されており，それらを利用することができる．また，提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり，その他の非正規言語クラスへの応用も期待される．","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"47","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"31","bibliographicIssueDates":{"bibliographicIssueDate":"2011-03-25","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"2","bibliographicVolumeNumber":"4"}]},"relation_version_is_last":true,"weko_creator_id":"11"}}