WEKO3
アイテム
項書き換えシステムにおける可簡約演算子とその応用
https://ipsj.ixsq.nii.ac.jp/records/16626
https://ipsj.ixsq.nii.ac.jp/records/166265884ddf7-a3e5-4906-9b4a-024083ce8d17
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO4606005.pdf (227.6 kB)
|
Copyright (c) 2005 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2005-04-15 | |||||||
| タイトル | ||||||||
| タイトル | 項書き換えシステムにおける可簡約演算子とその応用 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Reducible Operation Symbols for the Term Rewriting System and Their Applications | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 通常論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 北陸先端科学技術大学院大学 | ||||||||
| 著者所属 | ||||||||
| 北陸先端科学技術大学院大学 NEC ソフトウェア北陸 | ||||||||
| 著者所属 | ||||||||
| 北陸先端科学技術大学院大学 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Japan Advanced Institute of Science and Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Japan Advanced Institute of Science and Technology,NEC Software Hokuriku, Ltd. | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Japan Advanced Institute of Science and Technology | ||||||||
| 著者名 |
中村, 正樹
緒方, 和博
二木, 厚吉
× 中村, 正樹 緒方, 和博 二木, 厚吉
|
|||||||
| 著者名(英) |
Masaki, Nakamura
Kazuhiro, Ogata
Kokichi, Futatsugi
× Masaki, Nakamura Kazuhiro, Ogata Kokichi, Futatsugi
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 項書き換えシステムにおける演算子は，その意味から関数としての役割を持つ演算子と台集合の要素を構成する構成子としての演算子の2 つに分けられる．このとき項書き換えシステムには，任意の正規形が構成子からのみなるという性質が期待される．我々はそのような性質を持つ演算子として可簡約演算子の概念を提案する．すなわち可簡約演算子を含む任意の項は正規形ではない．通常の項，基底項（変数を含まない項），あるソートに属する項をそれぞれ簡約対象とした場合の可簡約演算子の定義を与え，その性質を示す．これらの可簡約演算子は，単に演算子が正規形に現れないという性質を持つのみでなく，効率的な書き換え関係を得る助けにもなる．また代数仕様への応用として，振舞仕様における重要な性質であるコヒーレント性の十分条件を与える． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | In a term rewriting system, operation symbols can be classified into two divisions from its denotational semantics: the operation symbols as functions and the operation symbols as constructors. Each term constructed by constructors corresponds to an element of the carrier set. Then the term rewriting system is expected to have the property that each normal form is constructed by only constructors. We propose the notion of the reducible operation symbols as any term having a reducible function symbol is not a normalform. We discuss about reducible operation symbols for ordinary terms, ground terms and terms of some sorts. Not only the reducible operation symbol has the property that it does not appear in each normal form but also it gives us an efficient rewrite relation. Moreover as an application to algebraic specifications we show a sufficient condition for the behavioral coherence, which is one of the most important properties of the behavioral specification. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 46, 号 SIG6(PRO25), p. 47-59, 発行日 2005-04-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
