{"links":{},"id":16935,"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00016935","sets":["934:935:978:980"]},"path":["980"],"owner":"1","recid":"16935","title":["古典線形論理型プログラミング言語の静的解析の一手法について"],"pubdate":{"attribute_name":"公開日","attribute_value":"2000-06-15"},"_buckets":{"deposit":"7a0f883d-5c16-470b-90bd-8317c4d62ced"},"_deposit":{"id":"16935","pid":{"type":"depid","value":"16935","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"古典線形論理型プログラミング言語の静的解析の一手法について","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"古典線形論理型プログラミング言語の静的解析の一手法について"},{"subitem_title":"A Static Analysis Method for a Classical Linear Logic Programming Language","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"通常論文","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2000-06-15","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"神戸大学大学院自然科学研究科"},{"subitem_text_value":"奈良工業高等専門学校"},{"subitem_text_value":"神戸大学工学部"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Graduate School of Science and Technology, Kobe University","subitem_text_language":"en"},{"subitem_text_value":"Nara National College of Technology","subitem_text_language":"en"},{"subitem_text_value":"Faculty of Engineering, Kobe 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/16935/files/IPSJ-TPRO4104006.pdf"},"date":[{"dateType":"Available","dateValue":"2002-06-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO4104006.pdf","filesize":[{"value":"1.4 MB"}],"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":"ba664521-924b-4780-8689-f1a2085bd47c","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2000 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"姜京順"},{"creatorName":"番原, 睦則"},{"creatorName":"田村, 直之"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Kyoung-Sun, Kang","creatorNameLang":"en"},{"creatorName":"Mutsunori, Banbara","creatorNameLang":"en"},{"creatorName":"Naoyuki, Tamura","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":"本稿では古典線形論理に基づいた論理型プログラミング言語の静的解析方法を提案する．線形論理に基づく論理型プログラミング言語としては　Lolli，LinLog，LO，Lygon，Forumなどが提案されている．特に，Forumは古典線形論理に対し完全である論理型プログラミング言語である．しかし，Forumのプログラムの証明探索は非決定性が非常に大きいため，静的解析することでプログラムの実行前に証明不可能なシーケントを取り除くことは重要である．Andreoliらは古典線形論理に基づく論理型プログラミング言語LOの静的解析方法を提案している．しかし，その方法は「リソースを意識した」線形論理型プログラミング言語で最も有用な演算子である乗法的論理積の解析には適用できないのである．そこで，我々は乗法的論理和，含意に加えて乗法的論理積を解析できる静的解析方法を考案した．我々の方法ではまず，プログラムと証明すべきゴールが与えられたら，そのシーケントのあり得る全ての証明を1つのAND‐ORグラフに表現する．そして，データフロー解析のための前方伝搬と後方伝搬を繰り返すことによって証明不可能な節点をグラフから取り除いていく．本稿の静的解析方法に基づくプロトタイプ解析機を開発し，実際にForumで書かれたソーティングプログラムを解析した結果，6要素のソーティングに対し，解析していない時の実行速度に比べ1000倍以上遠くなった．","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"We propose a new static analysis method applicable to a classical linear logic programming language. Andreoli et al. proposed a static analysis method for a classical linear logic programming language LO, but their method cannot handle multiplicative connectives, which can be seen as the most important connective for a resource-sensitive feature of linear logic. Our method, in contrast, covers multiplicative conjunctions in addition to multiplicative disjunctions and linear implications. Abstract proof graph, which is an AND-OR graph representing all possible sequent proofs, is constructed from a given program and goal sequent. The graph can be repeatedly refined by propagating information to remove unprovable nodes from the graph. We applied the result of our prototype analyzer to a sorting program written in Forum. The sorting program was improved more than 1000 times faster for sorting 6 elements.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"55","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"42","bibliographicIssueDates":{"bibliographicIssueDate":"2000-06-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"SIG04(PRO7)","bibliographicVolumeNumber":"41"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"created":"2025-01-18T22:50:04.161192+00:00","updated":"2025-01-22T23:36:16.859664+00:00"}