左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン  [in Japanese] Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems  [in Japanese]

Access this Article

Abstract

項書換え系(TRS)の到達可能性問題とは,与えられた2つの項の一方からもう一方にTRSでの書換えにより到達できるか否かという問題であり,一般には決定不能である.そこで,到達可能な項集合(の近似集合)を認識する木オートマトンの生成法が広く研究されている.条件付きTRS(CTRS)に関しては,左線形な結合CTRSについて生成手続きが提案されているが,木オートマトンの自動生成の基準となる近似関数はCTRSについて提案されていない.本稿では,結合CTRSを含むクラスである定向CTRSに着目し,左線形な定向CTRSで到達可能な項集合の近似集合を認識する木オートマトンの生成手続きを提案する.さらに,結合CTRSと定向CTRSのための近似関数,結合CTRSを定向CTRSで表現する方法を提案し,結合CTRSについての生成手続きと比較する.The reachability problem for term rewriting systems (TRSs) is to decide whether one of two given terms is reachable to the other with respect to rewriting by a given TRS. Unfortunately, this problem is undecidable in general. Hence, several methods have been widely studied in order to construct a tree automaton that accepts all terms reachable from terms in a given recognizable set. In conditional rewriting, such methods have been proposed only for left-linear join conditional TRSs. However, the techniques of approximation functions used in automatically constructing tree automata have not been formalized. In this paper, we focus on oriented conditional TRSs since every join conditional TRS can be simulated completely by an oriented one. We first propose a method that, given a left-linear oriented conditional TRS and a recognizable set of terms, constructs a tree automaton recognizing an over-approximated set of reachable terms. Then, we formalize approximation functions for join conditional TRSs and oriented ones, respectively, and compare the constructions for join and oriented systems.

Journal

  • 電子情報通信学会技術研究報告SS, ソフトウェアサイエンス

    電子情報通信学会技術研究報告SS, ソフトウェアサイエンス 107(176), 1-6, 2007-07

    一般社団法人電子情報通信学会

Codes

  • NII Article ID (NAID)
    120005526506
  • Text Lang
    JPN
  • Article Type
    journal article
  • ISSN
    0913-5685
  • Data Source
    IR 
Page Top