エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

エレファントな群とリー代数(10)

一般マグマの多項式の単一化アルゴリズム(2)

この項目の内容は「一階の項」の理論と内容は同じものになると思われます。書き方を変えることで極限や普遍性について考えるときに多項式の考え方が使えると思うのですが、今のところどうなるかわかりません。

前回の  u(\alpha, \beta, \sigma) の定義は、 \alpha, \beta を固定しても、変化させても定義できるのですが、両方が混じっていたので変化させるように書き直します。また、記述が複雑になってしまったので  M[X] T として書き直します。

 T f_i(t_1, t_2, \cdots, t_n) という形の元の全体を  T_{f_i}、 T_{f_0} = M とします。すると、 T = X \cup T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} となります。 T_+ = T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} とします。

 \Sigma を置換全体の集合とします。 v(\alpha) \alpha の部分項として現れる  X の元全体の集合とします。

 u(\alpha, \beta) u: T \times T \to \Sigma \sqcup \{F\} ( F は失敗を表す)を(場合分け(*)) \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*} と定義します( \triangleright は左から順に適用)。このとき \begin{cases}
u(α, β) = σ \in Σ & のとき & σ \ は \ α, β \ の最汎単一化子 \\
u(α, β) = F & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立ちます。

単一化アルゴリズムの定義

 u(\alpha, \beta) \alpha, \beta を変化させても定義できるならば、 u写像として定義できます。場合分け(*)の(1)から(10)の場合分けを1段階として、上位の部分項から順に実行することはアルゴリズムということができます。(9)の項は左から順に実行するとします。

 \alpha の部分項  f_i(t_1, t_2, \cdots, t_n) があるとき  f_i(t_1, t_2, \cdots, t_n) > t_j とします。 r+1 個の部分項が  t_0 > t_1 > \cdots > t_r という関係のとき  t_0 >^r t_r とします。 \alpha の部分項で  t >^r t' となる最大の  r r(\alpha) r(\alpha, \beta) = \max(r(\alpha), r(\beta)) とします。

 k(\alpha, \beta) v(\alpha) \cup v(\beta) の元の個数とします。

 k(\alpha, \beta) = 0 のとき、 u(\alpha, \beta) r(\alpha, \beta) 段階実行すると、ある  \sigma \in \Sigma または  F の結果を得ることができます。

 k= k(\alpha, \beta) とし、 u(\alpha, \beta) を段階的に実行して結果が得られるとき、その段階数を  s(\alpha, \beta) とします。結果が得られないとき、 s(\alpha, \beta) = \infty とします。

 r= r(\alpha, \beta) k= k(\alpha, \beta) のとき、 s(\alpha, \beta) の最大値があれば  t(r, k) とします。最大値がなければ  t(r, k) = \infty とします。

 k = 0 のとき  r = s(\alpha, \beta) = t(r, 0) となります。

 t(r, k) \le (2^{k+1}-1)r と仮定します。

 u(\alpha, \beta) r(\alpha, \beta) 段階実行すると、 \alpha または  \beta の部分項に  X の元が出現します。最初に現れた  X の元に対応する項を代入したものを  \alpha', \beta' とします。すると  r(\alpha', \beta') \le 2r(\alpha, \beta) k(\alpha', \beta') = k-1 となります。

帰納法の仮定より \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*} となって、任意の  \alpha, \beta に対して  t(r(\alpha, \beta), k(\alpha, \beta)) \le (2^{k(\alpha, \beta)+1}-1)r(\alpha, \beta) が成り立ちます。

よって  s(\alpha, \beta) \le t(r, k) \le (2^{k+1}-1)r となります。 u(\alpha, \beta) \alpha, \beta を変化させても定義できるので写像となり、上位の部分項から順に実行する手順はアルゴリズムということができます。