{"created":"2021-03-01T06:26:31.141985+00:00","id":19059,"links":{},"metadata":{"_buckets":{"deposit":"aed4a9fa-15b1-47fa-afcc-a8b384676416"},"_deposit":{"id":"19059","owners":[],"pid":{"revision_id":0,"type":"depid","value":"19059"},"status":"published"},"_oai":{"id":"oai:nagoya.repo.nii.ac.jp:00019059","sets":["312:313:314"]},"author_link":["55669","55670","55671","55672","55673","55674","55675","55676"],"item_10_alternative_title_19":{"attribute_name":"その他のタイトル","attribute_value_mlt":[{"subitem_alternative_title":"Proving Method of Termination/Non-Termination for Functional Programs with Exception Handling","subitem_alternative_title_language":"en"}]},"item_10_biblio_info_6":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2011-03","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"2","bibliographicPageEnd":"30","bibliographicPageStart":"13","bibliographicVolumeNumber":"4","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌, プログラミング","bibliographic_titleLang":"ja"}]}]},"item_10_description_4":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"本論文では,例外処理を持つ先行評価に基づく関数型プログラムの停止性・非停止性証明法を提案する.停止性と非停止性を保存する関数型プログラムの文脈依存項書き換え系 (CS-TRS) への変換法を与える.これにより,近年開発が進んでいる既存の CS-TRS の停止性証明ツールを用いることが可能になる.先行評価での実行においては,関数の引数を先頭から順に評価してから関数の値を計算するため,生成される書き換え系においては,この評価は基本的には最内評価に対応する.しかし,停止性を持たない引数と例外を発生させる引数の順序によって停止性に影響を与えるため,引数の評価順を厳密に考慮する必要がある.そのため,文脈依存の機能を用いて引数の評価順を制御する.また,例外が発生した場合には,それ以降の評価を止めて,例外が処理されるまで例外値を戻す必要がある.これを行えるように書き換え規則を生成する.また,この変換の健全性,すなわち変換後の CS-TRS が最内停止性を持てばプログラムも停止性を持つことと,完全性,すなわちプログラムが停止性を持つならば変換後の CS-TRS も最内停止性を持つことを示す.これにより,変換後の CS-TRS の最内 (非) 停止性が示すことができれば,プログラムの (非) 停止性が証明されることが保証される. ","subitem_description_language":"ja","subitem_description_type":"Abstract"},{"subitem_description":"We present a proving method of termination/non-termination for functional programs based on eager-evaluation with exception handling. We give a transformation of functional programs into Context-Sensitive Term Rewriting Systems (CS-TRSs). This enables us to use recent-developed termination provers for CS-TRSs as termination provers for functional programs. Since eager-evaluation computes a return value of a function after all values of its arguments are computed in right-to-left order, this evaluation corresponds to the innermost reduction on generated TRSs. The termination property is affected by the occurrences of non-terminating argument and exception-raising argument. This means that we have to handle the evaluation order strictly. Thus we used context sensitiveness for this purpose and design the transformation producing rewrite rules, that repeatedly pass back an exception to the caller until it is handled when exception occurs. We prove the soundness and completeness of the transformation, that is, the innermost termination of the CS-TRS implies the termination of the program and vise versa. This allows us to prove (non-)termination of programs by proving (non-)termination of CS-TRSs.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_10_identifier_60":{"attribute_name":"URI","attribute_value_mlt":[{"subitem_identifier_type":"URI","subitem_identifier_uri":"http://id.nii.ac.jp/1001/00073761/"},{"subitem_identifier_type":"HDL","subitem_identifier_uri":"http://hdl.handle.net/2237/21165"}]},"item_10_publisher_32":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"一般社団法人情報処理学会","subitem_publisher_language":"ja"}]},"item_10_relation_43":{"attribute_name":"関連情報","attribute_value_mlt":[{"subitem_relation_type":"isVersionOf","subitem_relation_type_id":{"subitem_relation_type_id_text":"http://id.nii.ac.jp/1001/00073761/","subitem_relation_type_select":"URI"}}]},"item_10_rights_12":{"attribute_name":"権利","attribute_value_mlt":[{"subitem_rights":"ここに掲載した著作物の利用に関する注意 本著作物の著作権は情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。Notice for the use of this material The copyright of this material is retained by the Information Processing Society of Japan (IPSJ). This material is published on this web site with the agreement of the author (s) and the IPSJ. Please be complied with Copyright Law of Japan and the Code of Ethics of the IPSJ if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof. All Rights Reserved, Copyright (C) Information Processing Society of Japan. Comments are welcome. Mail to address editj＠ipsj.or.jp, please.","subitem_rights_language":"ja"}]},"item_10_select_15":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_select_item":"publisher"}]},"item_10_source_id_7":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"0387-5806","subitem_source_identifier_type":"PISSN"}]},"item_1615787544753":{"attribute_name":"出版タイプ","attribute_value_mlt":[{"subitem_version_resource":"http://purl.org/coar/version/c_970fb48d4fbd8a85","subitem_version_type":"VoR"}]},"item_access_right":{"attribute_name":"アクセス権","attribute_value_mlt":[{"subitem_access_right":"open access","subitem_access_right_uri":"http://purl.org/coar/access_right/c_abf2"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"濱口, 毅","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55669","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"酒井, 正彦","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55670","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"馬場, 正貴","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55671","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"阿草, 清滋","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55672","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Hamaguchi, Takeshi","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55673","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Sakai, Masahiko","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55674","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Baba, Masataka","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55675","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Agusa, Kiyoshi","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55676","nameIdentifierScheme":"WEKO"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2018-02-21"}],"displaytype":"detail","filename":"IPSJ-TPRO0402003.pdf","filesize":[{"value":"414.8 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"IPSJ-TPRO0402003.pdf","objectType":"fulltext","url":"https://nagoya.repo.nii.ac.jp/record/19059/files/IPSJ-TPRO0402003.pdf"},"version_id":"82eb096e-ba7b-41c9-ab42-03dd786e021c"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"journal article","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"例外処理を持つ関数型プログラムの停止性・非停止性証明法","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"例外処理を持つ関数型プログラムの停止性・非停止性証明法","subitem_title_language":"ja"}]},"item_type_id":"10","owner":"1","path":["314"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2015-01-30"},"publish_date":"2015-01-30","publish_status":"0","recid":"19059","relation_version_is_last":true,"title":["例外処理を持つ関数型プログラムの停止性・非停止性証明法"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-16T04:32:27.873982+00:00"}