関数 f と値 n が与えられたとき、f(m)=n を満たす m の集合を n の f に関する逆像という。これを計算することは、プログラムとして与えられた方程式を解くとき、あるいはプログラム変換を行なうときに非常に有効な手段となる。西田らは、関数が項書換え系によって定義される場合に、逆像の一つの要素を計算することのできる項書換え系を生成する手法を提案した。
本研究では、西田の変換をMLを用いて実装し、さらに逆像の要素をすべて求める手法を考え、実装した。西田の手法で生成される項書換え系は一般的に停止性が保証されないため、すべての要素をできるだけ求められるよう工夫を加えた。