左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン

IR HANDLE Web Site 11 References Open Access

Bibliographic Information

Other Title
  • サセンケイナ テイコウ ジョウケンツキ コウ カキカエケイ ニ オケル トウタツ カノウナ コウ シュウゴウ ノ キンジ シュウゴウ オ ニンシキスル キ オートマトン
  • Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems

Search this article

Abstract

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

References(11)*help

See more

Keywords

Details 詳細情報について

Report a problem

Back to top