Word problem

記号 0, x, y, z, ... から次のように作られたものを項とします。 (1) 項 X から ( - X ) を作る。 (2) 項 X, Y から ( X + Y ) を作る。 (かっこは省略することもあります。) こうしてできた項の集合を T とします。 T の元に対して、次の関係をみたす同値関係 = が成り立っているとします。

0 + x = x

- x + x = 0

( x + y ) + z = x + ( y + z )

ここで、上の x, y, z に T のどんな元で置き換えても成り立っているとします。このとき、T の元 X, Y に対して X = Y が成り立っているかどうかを判定する方法を考えます。ある変形規則の集合によって X, Y を標準形 X', Y' に変形したとき、X' と Y' が項として一致しているかどうかで判定することができます。変形規則の集合は、次のようになります。

0 + x → x

- x + x → 0

( x + y ) + z → x + ( y + z )

- x + ( x + y ) → y

x + 0 → x

- - x → x

x + - x → 0

- 0 → 0

x + ( - x + y ) → y

- ( x + y ) → - y + - x

変形規則を求める方法は、次のようになります。 (Knuth-Bendix完備化手続き, [1, p.180])

	function KB( E: 等式の集合 ) return 書換え規則の集合
		var R, R_new: 書換え規則の集合
		R := 空集合
		while E != 空集合
			E から等式 l=r を選択する
			if l>>R = r>>R then
				E := E - {l=r}
			else
				case l>>R > r>>R then R_new := {l>>R->r>>R}
				case l>>R < r>>R then R_new := {r>>R->l>>R}
				otherwise 「失敗」を表示して停止する
				while Rの中にR_newでリダクション可能な規則s->tが存在
					R := R - {s->t}
					E := E + {s=t}
				end
				R := R + R_new
				E := E - {l=r} + {u=v: <u,v>はR_newとRの各規則間の危険対}
			end
		end
		return R
	end

l>>R, r>>R は、l,r をRの規則で変形して最終的にできる項を表す。 l>>R = r>>R は項が等しいことを表す。 l>>R > r>>R, l>>R < r>>R は項に入っている順序を表す。