条件付き項書換え系の紐解き変換の模倣完全性について On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems

Search this Article

Author(s)

Abstract

条件付き項書換え系(CTRS)から項書換え系(TRS)への変換は紐解き変換(unraveling)と呼ばれる.紐解き変換は与えられたCTRSに対して一般には模倣完全ではない,すなわち,変換により得られたTRSの書換え系列のうち,初期項と最終項が元のCTRSの関数記号上の項であるものが元のCTRSの書換え系列で模倣できるとは眠らない.一方,我々は決定的CTRSの紐解き変換を提案し,その変換が生成したTRSが左線形,右線形,変数非消去(non-erasing)の性質を持つための元のCTRSの構文条件をそれぞれ示した.本稿では,その紐解き変換が模倣完全性を持つための2つの条件を示す.1つは生成したTRSが右線形かつ変数非消去であること,もう1つは生成したTRSが左線形であることである.ただし,左線形の場合には右辺のみに現れる変数に代入されて現れた項の部分項は書き換えられていないとする.

Transformations from conditional term rewriting systems (CTRSs) over (original) signatures into term rewriting systems (TRSs) over the exteded signatures, are called unravelings. They are not always simulation-complete for any input CTRS. Here simulation-completeness means that every rewrite sequence of the unraveled CTRSs (the output TRSs), whose initial and final terms are over the original signatures, can be simulated by a rewrite sequence of the original CTRSs. We have proposed an unraveling which generates left-linear, right-linear and non-erasing TRSs from CTRSs satisfying some syntactic conditions, respectively. In this paper, we show two conditions that the unraveling is simulation-complete for CTRSs. One is that the unraveled CTRSs are right-linear and non-erasing, and the other is that they are left-linear. Under the latter condition, we assume that any redex introduced by extra variables is not reduced anywhere in the rewrite sequences of the unraveled CTRSs.

Journal

  • Technical report of IEICE. SS

    Technical report of IEICE. SS 104(243), 25-30, 2004-07-27

    The Institute of Electronics, Information and Communication Engineers

References:  9

Codes

  • NII Article ID (NAID)
    110003276724
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    ENG
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    7090666
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top