素因数分解の一般化
で生成された自由モノイド
の有限部分集合全体を
とおきます。モノイドの演算子を
、和集合の演算子を
とすると、
は
を積、
を和とする半環となります。積の単位元を
、和の単位元を
と書きます。
の元
は
と表すことができます(この を
と書くことにします)。
を
と定義することにより に拡張することができます。
素因数分解の部分写像
- (1)
のとき
- (2)
のとき
と定義します。これは を
- (k1)
のとき
- (k2)
のとき
と定義し、 を合成したものを表すとします。
に対して
が(k2)にならない
が存在すれば
を
(恒等写像)で置き換え、各
は
を呼び出すように置き換えた
を合成した「部分写像」を
としたとき
であるとします。
この を
とおきます。
順序
は順序
を持つとします。
、
に対して、任意の
に対して
であるとき
とします。
任意の に対して
であるとします。(*)
が順序
に関して降鎖条件を満たすならば、すなわち任意の
の元の列
に対して、ある自然数 が存在して、
が成り立つとします。(**)
このとき は
から
への写像となります。
項の素因数分解
(演算子は
または省略します)
とおきます。
を
とおきます。ここで 、
は
で、各
は単位元ではない
のすべての組についての和を表します。
項の長さの順序を順序とすると条件(*)、(**)が成り立ち、 は写像となります。
単一化アルゴリズム
(「単一化アルゴリズム(3) - エレファント・ビジュアライザー調査記録」参照)
項全体 の空ではない有限部分集合全体を
、代入全体を
とします。
とおきます。
を元の個数が
以上の
の部分集合
で、不一致集合が単一化代入
によって単一化可能であるもの全体とします。
とします。
を
と定義します。
に現れる変数の個数の順序を順序とすると条件(*)、(**)が成り立ち、
は写像となります。
を単一化代入を取得できるように変更すると、単一化アルゴリズムとなります。




