{"created":"2021-03-01T06:26:27.304543+00:00","id":19000,"links":{},"metadata":{"_buckets":{"deposit":"7e70cc73-e83f-45b8-8e76-2e8c754f358c"},"_deposit":{"id":"19000","owners":[],"pid":{"revision_id":0,"type":"depid","value":"19000"},"status":"published"},"_oai":{"id":"oai:nagoya.repo.nii.ac.jp:00019000","sets":["312:313:314"]},"author_link":["55388","55389","55390","55391","55392","55393","55394","55395","55396","55397"],"item_10_alternative_title_19":{"attribute_name":"その他のタイトル","attribute_value_mlt":[{"subitem_alternative_title":"Argument Filtering and Usable Rules in Higher-Order Rewrite Systems","subitem_alternative_title_language":"en"}]},"item_10_biblio_info_6":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2009-12","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"343","bibliographicPageEnd":"30","bibliographicPageStart":"25","bibliographicVolumeNumber":"109","bibliographic_titles":[{"bibliographic_title":"電子情報通信学会技術研究報告SS, ソフトウェアサイエンス","bibliographic_titleLang":"ja"}]}]},"item_10_description_4":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"項書換え系(TRS)の拡張として高階関数を直接扱える単純型付き項書換え系(STRS)やさらにλ抽象も扱える高階書換え系(HRS)が提案されている.静的依存対法はこれら高階の系における非常に強力な停止性証明法である.静的依存対法で停止性を証明する際には引数切り落とし法や実効規則の概念が重要となる.これらはTRS上で提案されSTRS上に拡張されているが, HRS上では知られていない.本論文ではHRS上の引数切り落とし法と実効規則の概念を与える.さらに我々の成果は単なる拡張ではなく,引数切り落とし法で要求されていた適用条件を取り除き,実効規則の定義から高階変数を介した依存性を取り除くという改良も伴っている. ","subitem_description_language":"ja","subitem_description_type":"Abstract"},{"subitem_description":"Simply-typed term rewriting systems (STRSs) and higher-order rewrite systems (HRSs) have been proposed to extend term rewriting systems (TRSs). These systems can handle higher-order functions directly, and moreover HRSs are allowed to have a A-abstraction syntax. Static dependency pair methods are very powerful methods for proving termination of these higher-order systems. Notions of argument filtering and usable rules play important roles in proving termination by the static dependency pair method. These notions are proposed on TRSs, and extended to STRSs. However, we have not known these notions on HRSs. In this paper, we extend notions of argument filtering and usable rules onto HRSs. In addition, these extensions include some enhancements : removing an applicable condition demanded by existing argument filtering methods on STRSs, and removing a dependency through higher-order variables from the definition of usable rule.","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://ci.nii.ac.jp/naid/110008001253"},{"subitem_identifier_type":"HDL","subitem_identifier_uri":"http://hdl.handle.net/2237/21104"}]},"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://ci.nii.ac.jp/naid/110008001253","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":"55388","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"草刈, 圭一朗","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55389","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"坂部, 俊樹","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55390","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"酒井, 正彦","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55391","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"西田, 直樹","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55392","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"SUZUKI, Sho","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55393","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"KUSAKARI, Keiichirou","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55394","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"SAKABE, Toshiki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55395","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"SAKAI, Masahiro","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55396","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"NISHIDA, Naoki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55397","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":"110008001253.pdf","filesize":[{"value":"931.4 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"110008001253.pdf","objectType":"fulltext","url":"https://nagoya.repo.nii.ac.jp/record/19000/files/110008001253.pdf"},"version_id":"49709686-468d-4580-a485-1040da4b01dc"}]},"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"}]},"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-20"},"publish_date":"2015-01-20","publish_status":"0","recid":"19000","relation_version_is_last":true,"title":["高階書換え系における引数切り落とし法と実効規則"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-16T04:07:15.255642+00:00"}