Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
スポンサーリンク
概要
- 論文の詳細を見る
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.
論文 | ランダム
- 地盤・基礎・建物連成系の地震応答(その3・隣接建物の影響)
- 地盤・基礎・建物連成系の地震応答(その2・表層地形の影響)
- 地盤・基礎・建物連成系の地震応答(その1・成層地盤の影響)
- 地震時における地盤-建物相互作用に関する二,三の考察(その1・直接基礎を有するRC-中層建物について)
- 建物-地盤系のモデル化に関する研究(その1・東松山地震の解析)