WEKO3
アイテム
{"_buckets": {"deposit": "a0153ea0-a9c6-4a41-a093-99aa88a969d0"}, "_deposit": {"id": "9338", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "9338"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00009338", "sets": ["314"]}, "author_link": ["26678", "26679", "26680", "26681"], "item_10_biblio_info_6": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2007", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "5", "bibliographicPageEnd": "431", "bibliographicPageStart": "407", "bibliographicVolumeNumber": "18", "bibliographic_titles": [{"bibliographic_title": "Applicable Algebra in Engineering, Communication and Computing", "bibliographic_titleLang": "en"}]}]}, "item_10_description_4": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "We enhance the dependency pair method in order to prove termination using recursive structure analysis in simply-typed term rewriting systems, which is one of the computational models of functional programs. The primary advantage of our method is that one can exclude higher-order variables which are difficult to analyze theoretically, from recursive structure analysis. The key idea of our method is to analyze recursive structure from the viewpoint of strong computability. This property was introduced for proving termination in typed λ-calculus, and is a stronger condition than the property of termination. The difficulty in incorporating this concept into recursive structure analysis is that because it is defined inductively over type structure, it is not closed under the subterm relation. This breaks the correspondence between strong computability and recursive structure. In order to guarantee the correspondence, we propose plain function-passing as a restriction, which is satisfied by many non-artificial functional programs.", "subitem_description_language": "en", "subitem_description_type": "Abstract"}]}, "item_10_identifier_60": {"attribute_name": "URI", "attribute_value_mlt": [{"subitem_identifier_type": "HDL", "subitem_identifier_uri": "http://hdl.handle.net/2237/11112"}]}, "item_10_publisher_32": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "Springer-International", "subitem_publisher_language": "en"}]}, "item_10_select_15": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_select_item": "author"}]}, "item_10_source_id_7": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "09381279", "subitem_source_identifier_type": "PISSN"}]}, "item_10_text_14": {"attribute_name": "フォーマット", "attribute_value_mlt": [{"subitem_text_value": "application/pdf"}]}, "item_1615787544753": {"attribute_name": "出版タイプ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_ab4af688f83e57aa", "subitem_version_type": "AM"}]}, "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": "26678", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Kusakari, Keiichirou", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "26679", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "酒井, 正彦", "creatorNameLang": "ja"}], "nameIdentifiers": [{"nameIdentifier": "26680", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Sakai, Masahiko", "creatorNameLang": "en"}], "nameIdentifiers": [{"nameIdentifier": "26681", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-02-20"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "aaecc07.pdf", "filesize": [{"value": "164.0 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_note", "mimetype": "application/pdf", "size": 164000.0, "url": {"label": "aaecc07.pdf", "objectType": "fulltext", "url": "https://nagoya.repo.nii.ac.jp/record/9338/files/aaecc07.pdf"}, "version_id": "3ea5fd5f-2f4c-49c1-b208-7e67f0050050"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "Termination", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Simply-Typed Term Rewriting System", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Plain Function-Passing", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Dependency Pair", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Strong Computability", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting", "subitem_title_language": "en"}]}, "item_type_id": "10", "owner": "1", "path": ["314"], "permalink_uri": "http://hdl.handle.net/2237/11112", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2009-02-13"}, "publish_date": "2009-02-13", "publish_status": "0", "recid": "9338", "relation": {}, "relation_version_is_last": true, "title": ["Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting"], "weko_shared_id": -1}
Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting
http://hdl.handle.net/2237/11112
http://hdl.handle.net/2237/11112dcc62b8a-c6ec-4119-aceb-ebfd0e704b8e
名前 / ファイル | ライセンス | アクション |
---|---|---|
aaecc07.pdf (164.0 kB)
|
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2009-02-13 | |||||
タイトル | ||||||
タイトル | Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting | |||||
言語 | en | |||||
著者 |
草刈, 圭一朗
× 草刈, 圭一朗× Kusakari, Keiichirou× 酒井, 正彦× Sakai, Masahiko |
|||||
アクセス権 | ||||||
アクセス権 | open access | |||||
アクセス権URI | http://purl.org/coar/access_right/c_abf2 | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Termination | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Simply-Typed Term Rewriting System | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Plain Function-Passing | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Dependency Pair | |||||
キーワード | ||||||
主題Scheme | Other | |||||
主題 | Strong Computability | |||||
抄録 | ||||||
内容記述 | We enhance the dependency pair method in order to prove termination using recursive structure analysis in simply-typed term rewriting systems, which is one of the computational models of functional programs. The primary advantage of our method is that one can exclude higher-order variables which are difficult to analyze theoretically, from recursive structure analysis. The key idea of our method is to analyze recursive structure from the viewpoint of strong computability. This property was introduced for proving termination in typed λ-calculus, and is a stronger condition than the property of termination. The difficulty in incorporating this concept into recursive structure analysis is that because it is defined inductively over type structure, it is not closed under the subterm relation. This breaks the correspondence between strong computability and recursive structure. In order to guarantee the correspondence, we propose plain function-passing as a restriction, which is satisfied by many non-artificial functional programs. | |||||
言語 | en | |||||
内容記述タイプ | Abstract | |||||
出版者 | ||||||
言語 | en | |||||
出版者 | Springer-International | |||||
言語 | ||||||
言語 | eng | |||||
資源タイプ | ||||||
資源タイプresource | http://purl.org/coar/resource_type/c_6501 | |||||
タイプ | journal article | |||||
出版タイプ | ||||||
出版タイプ | AM | |||||
出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
ISSN | ||||||
収録物識別子タイプ | PISSN | |||||
収録物識別子 | 09381279 | |||||
書誌情報 |
en : Applicable Algebra in Engineering, Communication and Computing 巻 18, 号 5, p. 407-431, 発行日 2007 |
|||||
フォーマット | ||||||
application/pdf | ||||||
著者版フラグ | ||||||
値 | author | |||||
URI | ||||||
識別子 | http://hdl.handle.net/2237/11112 | |||||
識別子タイプ | HDL |