項書き換えシステムにおける可簡約演算子とその応用  [in Japanese] Reducible Operation Symbols for the Term Rewriting System and Their Applications  [in Japanese]

Search this Article

Author(s)

Abstract

項書き換えシステムでは, 書き換え規則の適用によって簡約できる項は可約項と呼ばれる.本研究では, この可簡約の概念を演算子に適用し, 可簡約演算子の性質を明らかにする.可簡約演算子とは, その演算子を含む項が可簡約であることと定義する.項は演算子をノードに持つ木構造であり, 項の簡約のしくみには演算子間の区別はない.しかし通常, システムの記述者はモデル上の要素を構成する構成子とその上の関数を表す演算子を区別して考える.可簡約演算子とは, 後者の関数としての演算子が持つべき性質である.本研究では, (1)通常の項, (2)基底項(変数を含まない), (3)あるソートに属する項を簡約対象とした場合に, 演算子が可簡約であるための必要十分条件を示す.直接の成果として, 文脈依存書き換えの正当性の十分条件を得ることができる.文脈依存書き換えは, 書き換えポジションが制限された書き換え関係であり, 正当性は, 書き換え結果が必ず正規形であるという性質である.正当性の十分条件は, 無駄な書き換えや停止しない簡約を避けて正規形を得るための方法を与える.応用として, 隠蔽代数に基づく振舞い仕様に対する可簡約演算子の定義を与える.隠蔽代数における可簡約演算子が, 隠蔽代数において重要な性質であるコヒーレント性の十分条件を与えることを示す.

In term rewriting, a term to which some rewrite rule can be applied is called a reducible term. We apply the notion of reducibility to an operation symbol. A reducible operation symbol is defined as follows: a term having a reducible operation symbol is reducible. A term is a tree-structure whose nodes are operation symbols, and there is no difference between them for mechanism of reduction of terms by rewrite rules. However, when describing a system, the designer should divide them into ones denoting constructors of elements in the model and others denoting functions on the set of the elements. The latter should be given as reducible operation symbols. In this study we give a definition of reducible operation symbols for each of (1) ordinary terms, (2) ground (variable-free) terms, and (3) terms of some sorts. Reducible operation symbols give us a sufficient condition for the correctness of context-sensitive rewriting. This gives us a method to reduce terms into normal form with no waste or non-terminating reduction. As another application of reducibility we also a sufficient condition for behavioral coherence of the hidden algebra.

Journal

  • 情報処理学会論文誌. プログラミング

    情報処理学会論文誌. プログラミング 46(25), 69, 2005-04-15

    Information Processing Society of Japan (IPSJ)

Codes

  • NII Article ID (NAID)
    110002769559
  • NII NACSIS-CAT ID (NCID)
    AA11464814
  • Text Lang
    JPN
  • Article Type
    SHO
  • ISSN
    03875806
  • Data Source
    CJP  NII-ELS 
Page Top