CafeOBJ入門(3) : 等式推論と項書換システム Introducing CafeOBJ (3) : Equational Reasoning and Term Rewriting Systems

この論文にアクセスする

この論文をさがす

著者

抄録

等式推論は代数仕様言語CafeOBJの最重要の推論機構である.等式推論の効率的な実行を可能とする項書換システムについて,CafeOBJ仕様の作成の助けとなる知識に焦点を当てて解説する.項書換システムの停止性,合流性,十分完全性などの基本的性質を満たす仕様作成の指針を示し,AC演算子属性,条件付き等式などを含む仕様への適用を議論する.Equational inference is the most fundamental inference mechanism for CafeOBJ algebraic specification language. Term rewriting system can realize equational inference in an efficient way. Several pieces of fundamental knowledge on term rewriting systems, which are valuable for CafeOBJ specification development, are described. We present the ways to describe specifications which satisfies fundamental properties of term rewriting systems: termination, confluence and sufficient completeness properties, and also discuss about applications to specifications including associative and/or commutative operators, conditional equations, and so on.

Equational inference is the most fundamental inference mechanism for CafeOBJ algebraic specification language. Term rewriting system can realize equational inference in an efficient way. Several pieces of fundamental knowledge on term rewriting systems, which are valuable for CafeOBJ specification development, are described. We present the ways to describe specifications which satisfies fundamental properties of term rewriting systems: termination, confluence and sufficient completeness properties, and also discuss about applications to specifications including associative and/or commutative operators, conditional equations, and so on.

収録刊行物

  • コンピュータソフトウェア = Computer software

    コンピュータソフトウェア = Computer software 25(3), 69-80, 2008-07-25

    日本ソフトウェア科学会

参考文献:  7件中 1-7件 を表示

各種コード

  • NII論文ID(NAID)
    110006840405
  • NII書誌ID(NCID)
    AN10075819
  • 本文言語コード
    JPN
  • 資料種別
    Journal Article
  • ISSN
    02896540
  • NDL 記事登録ID
    9599985
  • NDL 雑誌分類
    ZM13(科学技術--科学技術一般--データ処理・計算機)
  • NDL 請求記号
    Z14-1033
  • データ提供元
    CJP書誌  NDL  NII-ELS  IR  J-STAGE 
ページトップへ