項書換え系の決定問題の解法として最近 GTT(Ground Tree Transducer)が注目さ れている。GTT とは同一のアルファベット上で動く木オートマトンの組で、項間の関 係を表 現できる。本研究では、2 つの項が GTT によって認識されるかどうかを調べる GTT のシミュレータ、ならびに、GTT が表す関係 R の推移的閉包 R* を表す GTT を生 成するシステムをプログラミング言語 ML を用いて実現した。実現したプログラム は、Comon らの手法に基づき、GTT の 2 つの木オートマトンの積オートマトンが遷 移す る可能性のある状態を調べることで構成されている。この実装により、右辺と左辺 に共通変数を持たない項書換え系の 1 ステップの書き換えを GTT で表現し、そ の推移的閉包を生成することができる。すなわち、項の到達可能性を判定するこ とが出来る。