一般マグマの多項式の単一化アルゴリズム(2)
この項目の内容は「一階の項」の理論と内容は同じものになると思われます。書き方を変えることで極限や普遍性について考えるときに多項式の考え方が使えると思うのですが、今のところどうなるかわかりません。
前回の の定義は、 を固定しても、変化させても定義できるのですが、両方が混じっていたので変化させるように書き直します。また、記述が複雑になってしまったので を として書き直します。
の という形の元の全体を とします。すると、 となります。 とします。
を置換全体の集合とします。 を の部分項として現れる の元全体の集合とします。
、 ( は失敗を表す)を(場合分け(*)) \begin{cases}
(1) & α \in M, & β \in M, & α = β & のとき & σ \\
(2) & α \in M, & β \in M, & α \ne β & のとき & F \\
(3) & α \in X, & β \in X, & α = β & のとき & σ \\
(4) & α \in X, & β \in X, & α \ne β & のとき & σ \succ (α \mapsto β) \\
(5) & α \in X, & β \in T_+, & α \notin v(β) & のとき & σ \succ (α \mapsto β) \\
(6) & α \in X, & β \in T_+, & α \in v(β) & のとき & F \\
(7) & α \in T_+, & β \in X , & β \notin v(α) & のとき & σ \succ (β \mapsto α) \\
(8) & α \in T_+, & β \in X , & β \in v(α) & のとき & F \\
(9) & α \in T_f, & β \in T_g , & f = g & のとき & 以下を参照 \\
(10) & α \in T_f, & β \in T_g , & f \ne g & のとき & F \\
\end{cases} と定義します(定義できるかどうかは以下で検討)。(9)は \begin{cases}
σ \in Σ & のとき & σ \triangleright u(s, t) = u(s[σ], t[σ]) \\
F & のとき & F \triangleright u(s, t) = F \\
\end{cases} としたとき \begin{eqnarray*}
(9) & & u(f(s_1, s_2, \cdots, s_n), f(t_1, t_2, \cdots, t_n)) \\
& = & 1 \triangleright u(s_1, t_1) \triangleright u(s_2, t_2) \triangleright \cdots \triangleright u(s_n, t_n) \\
\end{eqnarray*} と定義します( は左から順に適用)。このとき \begin{cases}
u(α, β) = σ \in Σ & のとき & σ \ は \ α, β \ の最汎単一化子 \\
u(α, β) = F & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立ちます。
単一化アルゴリズムの定義
が を変化させても定義できるならば、 は写像として定義できます。場合分け(*)の(1)から(10)の場合分けを1段階として、上位の部分項から順に実行することはアルゴリズムということができます。(9)の項は左から順に実行するとします。
の部分項 があるとき とします。 個の部分項が という関係のとき とします。 の部分項で となる最大の を 、 とします。
を の元の個数とします。
のとき、 を 段階実行すると、ある または の結果を得ることができます。
とし、 を段階的に実行して結果が得られるとき、その段階数を とします。結果が得られないとき、 とします。
、 のとき、 の最大値があれば とします。最大値がなければ とします。
のとき となります。
と仮定します。
を 段階実行すると、 または の部分項に の元が出現します。最初に現れた の元に対応する項を代入したものを とします。すると 、 となります。
帰納法の仮定より \begin{eqnarray*}
& & t(r(α', β'), k(α', β')) \\
& \le & r + (2^{k(α', β')+1}-1)r(α', β') \\
& \le & r + (2^{ (k - 1 ) + 1 }- 1) \cdot 2r \\
& = & (2^{k+1}-1)r
\end{eqnarray*} となって、任意の に対して が成り立ちます。
よって となります。 は を変化させても定義できるので写像となり、上位の部分項から順に実行する手順はアルゴリズムということができます。