ログイン
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

{"_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}
  1. A500 情報学部/情報学研究科・情報文化学部・情報科学研究科
  2. A500a 雑誌掲載論文
  3. 学術雑誌

Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting

http://hdl.handle.net/2237/11112
http://hdl.handle.net/2237/11112
dcc62b8a-c6ec-4119-aceb-ebfd0e704b8e
名前 / ファイル ライセンス アクション
aaecc07.pdf 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
著者 草刈, 圭一朗

× 草刈, 圭一朗

WEKO 26678

ja 草刈, 圭一朗

Search repository
Kusakari, Keiichirou

× Kusakari, Keiichirou

WEKO 26679

en Kusakari, Keiichirou

Search repository
酒井, 正彦

× 酒井, 正彦

WEKO 26680

ja 酒井, 正彦

Search repository
Sakai, Masahiko

× Sakai, Masahiko

WEKO 26681

en Sakai, Masahiko

Search repository
アクセス権
アクセス権 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
戻る
0
views
See details
Views

Versions

Ver.1 2021-03-01 12:00:36.295511
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3