{"created":"2021-03-01T06:29:04.403854+00:00","id":21404,"links":{},"metadata":{"_buckets":{"deposit":"ac62191f-1b55-48e5-9b0b-d3f24567d8ac"},"_deposit":{"id":"21404","owners":[],"pid":{"revision_id":0,"type":"depid","value":"21404"},"status":"published"},"_oai":{"id":"oai:nagoya.repo.nii.ac.jp:00021404","sets":["312:313:314"]},"author_link":["62025","62026","62027","62028","62029","62030","62031","62032","62033","62034"],"item_10_alternative_title_19":{"attribute_name":"その他のタイトル","attribute_value_mlt":[{"subitem_alternative_title":"On Usable Rules under Argument Filterings in Higher-Order Rewrite Systems","subitem_alternative_title_language":"en"}]},"item_10_biblio_info_6":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2012-01","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"406","bibliographicPageEnd":"62","bibliographicPageStart":"57","bibliographicVolumeNumber":"111","bibliographic_titles":[{"bibliographic_title":"電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス","bibliographic_titleLang":"ja"}]}]},"item_10_description_4":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"高階書換え系(HRS)での強力な停止性証明手法として静的依存対法が知られている.この手法は静的な再帰構造解析を行い,静的再帰成分と呼ばれる解析結果の非循環性を示すことで証明を行う.この際に,非循環性を示すために考慮すべき規則を絞り込む実効規則と呼ばれる概念が提案されているが,高階変数を介した依存解析が困難であるため規則を絞り込めない場合がある.一方,一階の書換え系ではより考慮すべき規則を絞り込む,引数切り落とし関数の下での実効規則が提案されている.本研究ではこの成果をHRS上に拡張する.高階変数から始まる部分項を切り落とすことにより高階変数を介した依存解析を考慮せずにすむため,証明力を飛躍的に向上させることができる. ","subitem_description_language":"ja","subitem_description_type":"Abstract"},{"subitem_description":"The static dependency pair method is known as a powerful method for proving termination of higher-order rewrite systems (HRSs). The method proves the termination by showing the non-loopingness of all the static recursion components respectively that are obtained by some static recursion analysis. The notion of usable rules has been proposed to reduce the number of rewrite rules considered in showing the non-loogingness. However, we sometimes fail to reduce rewrite rules by reason of some dependency analysis through higher-order variables. In first-order term rewriting, the notion of usable rules under argument filterings has also been proposed, which can reduce more rewrite rules in general. In this paper, we extend the notion to HRSs. By filtering subterms rooted by a higher-order variable, we can avoid analyzing dependencies through higher-order variables.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_10_description_5":{"attribute_name":"内容記述","attribute_value_mlt":[{"subitem_description":"IEICE Technical Report;MSS2011-64,IEICE Technical Report;SS2011-49","subitem_description_language":"en","subitem_description_type":"Other"}]},"item_10_identifier_60":{"attribute_name":"URI","attribute_value_mlt":[{"subitem_identifier_type":"URI","subitem_identifier_uri":"http://ci.nii.ac.jp/naid/110009482063/"},{"subitem_identifier_type":"HDL","subitem_identifier_uri":"http://hdl.handle.net/2237/23548"}]},"item_10_publisher_32":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"一般社団法人電子情報通信学会","subitem_publisher_language":"ja"}]},"item_10_relation_40":{"attribute_name":"シリーズ","attribute_value_mlt":[{"subitem_relation_name":[{"subitem_relation_name_text":"IEICE Technical Report;MSS2011-64"}]},{"subitem_relation_name":[{"subitem_relation_name_text":"IEICE Technical Report;SS2011-49"}]}]},"item_10_relation_43":{"attribute_name":"関連情報","attribute_value_mlt":[{"subitem_relation_type":"isVersionOf","subitem_relation_type_id":{"subitem_relation_type_id_text":"http://ci.nii.ac.jp/naid/110009482063/","subitem_relation_type_select":"URI"}}]},"item_10_rights_12":{"attribute_name":"権利","attribute_value_mlt":[{"subitem_rights":"(c)一般社団法人電子情報通信学会 本文データは学協会の許諾に基づきCiNiiから複製したものである","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":"0913-5685","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":"62025","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"草刈, 圭一朗","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"62026","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"酒井, 正彦","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"62027","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"坂部, 俊樹","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"62028","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"西田, 直樹","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"62029","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"OOI, Kazuhiro","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"62030","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"KUSAKARI, Keiichirou","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"62031","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"SAKAI, Masahiko","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"62032","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"SAKABE, Toshiki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"62033","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"NISHIDA, Naoki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"62034","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":"110009482063.pdf","filesize":[{"value":"869.4 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"110009482063.pdf","objectType":"fulltext","url":"https://nagoya.repo.nii.ac.jp/record/21404/files/110009482063.pdf"},"version_id":"3c91881b-ad74-4f47-b278-7a16e92807e6"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"高階書換え系","subitem_subject_scheme":"Other"},{"subitem_subject":"停止性","subitem_subject_scheme":"Other"},{"subitem_subject":"静的依存対法","subitem_subject_scheme":"Other"},{"subitem_subject":"引数切り落とし法","subitem_subject_scheme":"Other"},{"subitem_subject":"実効規則","subitem_subject_scheme":"Other"},{"subitem_subject":"higher−order rewrite system","subitem_subject_scheme":"Other"},{"subitem_subject":"termination","subitem_subject_scheme":"Other"},{"subitem_subject":"static dependency pair method","subitem_subject_scheme":"Other"},{"subitem_subject":"argument filtering","subitem_subject_scheme":"Other"},{"subitem_subject":"usable rule","subitem_subject_scheme":"Other"}]},"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":"2016-02-23"},"publish_date":"2016-02-23","publish_status":"0","recid":"21404","relation_version_is_last":true,"title":["高階書換え系における引数切り落とし関数の下での実効規則について"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-16T04:10:26.591957+00:00"}