項の集合Tが正則であるとは, Tを受理する木オートマトンが存在することである. 項の集合を木言語ともいう. 項書換え系Rが構成的正則保存であるとは, 任意の正則木言語Lに対して, LからRによって 書換えて得られる項全体からなる木言語が正則であり, それを受理する木オートマトンを構成できることをいう.
構成的正則保存項書換え系においては, 到達可能性や会同性,局所合流性などの重要な性質が 決定可能になることが知られている. しかしながら,与えられた項書換え系が構成的正則保存であるかどうかは 決定不能である.
これまでにいくつかの決定可能な部分クラスが提案されてきたが, それらは書換え規則の右辺に強い制約を課している. 本研究で提案する多層変換項書換え系のクラスは { f(x) -> f(g(x)) } のような, 既知の部分クラス には属さない正則保存項書換え系を含んでいる. また,木言語理論における代表的な計算モデルである 線形ボトムアップ型木変換器は多層変換項書換え系の特別な場合である.
本研究では,多層変換項書換え系が正則保存になるための 2つの十分条件を与える.
A set of ground terms (tree language) T is recognizable if there exists a tree automaton which accepts T. A TRS R effectively preserves recognizability (EPR) if for any recognizable tree language L, the set of terms obtained by rewriting terms in L by R is also recognizable and a tree automaton which accepts it can be effectively constructed.
EPR-TRS has good mathematical properties, e.g., reachability, joinability and local confluence are decidable for EPR-TRSs. Unfortunately it is undecidable whether a given TRS belongs to EPR-TRS or not.
Therefore decidable subclasses of EPR-TRS have been proposed. These subclasses put a rather strong constraint on the syntax of the right-hand side of a rewrite rule. The class of LT-TRSs contains some EPR-TRSs, e.g., { f(x) -> f(g(x)) } which do not belong to any of the known decidable subclasses of EPR-TRSs. Bottom-up linear tree transducer, which is a well-known computation model in the tree language theory, is a special case of LT-TRS.
In this thesis, two sufficient conditions for an LT-TRS to be an EPR-TRS are presented.