WEKO3
インデックスリンク
アイテム
Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
http://hdl.handle.net/2297/22582
http://hdl.handle.net/2297/2258261d0265e-4d3d-4bed-ad19-123b2f68ce4a
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
TE-PR-NAKAMURA-M-551.pdf (232.5 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2017-10-03 | |||||
| タイトル | ||||||
| タイトル | Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | journal article | |||||
| 著者 |
Nakamura, Masaki
× Nakamura, Masaki× Ogata, Kazuhiro× Futatsugi, Kokichi |
|||||
| 提供者所属 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 金沢大学理工研究域電子情報学系 | |||||
| 書誌情報 |
Journal of Symbolic Computation 巻 45, 号 5, p. 551-573, 発行日 2010-01-01 |
|||||
| ISSN | ||||||
| 収録物識別子タイプ | ISSN | |||||
| 収録物識別子 | 0747-7171 | |||||
| NCID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AA10460294 | |||||
| DOI | ||||||
| 関連タイプ | isVersionOf | |||||
| 識別子タイプ | DOI | |||||
| 関連識別子 | 10.1016/j.jsc.2010.01.008 | |||||
| 出版者 | ||||||
| 出版者 | Elsevier | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | In this paper, we propose the notion of reducibility of symbols in term rewriting systems (TRSs). For a given algebraic specification, operation symbols can be classified on the basis of their denotations: the operation symbols for functions and those for constructors. In a model, each term constructed by using only constructors should denote an element, and functions are defined on sets formed by these elements. A term rewriting system provides operational semantics to an algebraic specification. Given a TRS, a term is called reducible if some rewrite rule can be applied to it. An irreducible term can be regarded as an answer in a sense. In this paper, we define the reducibility of operation symbols as follows: an operation symbol is reducible if any term containing the operation symbol is reducible. Non-trivial properties of context-sensitive rewriting, which is a simple restriction of rewriting, can be obtained by restricting the terms on the basis of variable occurrences, its sort, etc. We confirm the usefulness of the reducibility of operation symbols by applying them to behavioral specifications for proving the behavioral coherence property. © 2010 Elsevier Ltd. All rights reserved. | |||||
| 著者版フラグ | ||||||
| 出版タイプ | AM | |||||
| 出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
