WEKO3
アイテム
項書き換えシステムにおける生成性と局所十分完全性について
https://ipsj.ixsq.nii.ac.jp/records/233818
https://ipsj.ixsq.nii.ac.jp/records/233818f3a496c0-9f17-4282-9a45-f9961b01c2f6
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO1702005.pdf (107.8 kB)
2026年4月22日からダウンロード可能です。
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| 非会員：¥0, IPSJ:学会員：¥0, PRO:会員：¥0, DLIB:会員：¥0 | ||
| Item type | Trans(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-04-22 | |||||||||
| タイトル | ||||||||||
| タイトル | 項書き換えシステムにおける生成性と局所十分完全性について | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | On Productivity and Local Sufficient Completeness of Term Rewriting Systems | |||||||||
| 言語 | ||||||||||
| 言語 | jpn | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | [発表概要, Unrefereed Presentatin Abstract] | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者所属 | ||||||||||
| 新潟大学大学院自然科学研究科 | ||||||||||
| 著者所属 | ||||||||||
| 新潟大学大学院自然科学研究科 | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Science and Technology, Niigata University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Science and Technology, Niigata University | ||||||||||
| 著者名 |
櫻井, 爽一
× 櫻井, 爽一
× 青戸, 等人
|
|||||||||
| 著者名(英) |
Soichi, Sakurai
× Soichi, Sakurai
× Takahito, Aoto
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | 関数型プログラムでは，関数に値を入力して呼び出すことで計算を行う．そのため，関数呼び出しに対して，つねに計算が終了するという性質は重要なものである．十分完全性は，計算モデルの1つである項書き換えシステムにおいてそのような性質をモデル化したものである．項書換えシステムでは，十分完全性は，書き換えによって基底項を必ず基底構成子項に書き換えることができることをいう性質をいう．また，特定の関数呼び出しについてはつねに構成子項に書き換えられることをいう性質を，局所十分完全性と呼ぶ(Shiraishi et al., 2021)．一方，ストリームのような，要素を無限個含むようなものを対象とした計算は一般に終了することはないが，ストリームの先頭から任意個の要素を取り出しても，その次の要素を適切な値として求められることがあり，そのようなことを保証する性質を生成性と呼ぶ．生成性についても，項書き換えシステムに基づく形式化や検証方法が提案されている(Endrullis and Hendriks, 2011)．局所十分完全性と生成性の間には，計算が終了しないことがあるシステムを対象とし，値の取り出しを保証する点が共通している．しかし，従来，この2つの性質の関連性などについてはあまり報告されていない．そこで本発表では，項書き換えシステムに基づく形式化における，両者の性質の関連について報告する．そして，その関連性に基づく，生成性の検証手法を用いた局所十分完全性の検証手法を提案する． | |||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | Computations in functional programs are performed by applying functions to values. Thus, it is important to ensure calculations for function calls always terminate. Using term rewriting systems (TRSs), a computational model based on equational logic, this property is modeled as sufficient completeness. A TRS is sufficiently complete if any ground terms can be rewritten into ground constructor terms. A property that ensure particular function calls can be rewritten into constructor terms is called local sufficient completeness. There is a property known as productivity which concerns computations of infinite stream of elements. A system is called productive when one can obtain the next value after comsuming finite number of first parts of the stream. A formalization of the notion of productivity based on TRSs and its verification method are proposed in Endrullis and Hendriks (2011). Local sufficient completeness and productivity share a feature that it deals with systems that may not terminating and that ensures possibility of getting some values. However, it seems that relations of these two properties have not been investigated. In this presentation, we will report a relation of two properties based on formalization using TRSs. We also propose a verification method for local sufficient completeness using the one for productivity. | |||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AA11464814 | |||||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 17, 号 2, p. 1-1, 発行日 2024-04-22 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 1882-7802 | |||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
