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

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

多重集合・自由可換モノイド(1)

エレファントな整数論では、素因数分解の一意性のわかりやすい記法を考えていたのですが、良い方法ができず止まっていました。ここでは、数式ではなくプログラミング言語を使って書くとどうなるか考えていきたいと思います。まず、エレファントな整数論(18)、(19)で書いた内容を書いておきます。

整数の素因数分解の多重集合としての一意性

重複度を含めた集合を多重集合(wikipedia:多重集合参照)と呼びます。多重集合  \{| x_1, x_2, \cdots , x_m |\} とは、通常の集合とは異なり、 x_1, x_2, \cdots , x_m の中に重複するものがあったとき、その出現する回数が異なれば多重集合としては異なるものとするものです。

多重集合  \{| x_1, x_2, \cdots , x_m |\} \{| y_1, y_2, \cdots , y_n |\}全単射  g: \{1, 2, \cdots, m\} \to \{1, 2, \cdots, n\} が存在して任意の  i \in \{1, 2, \cdots, m\} に対して  x_i = y_{g(i)} であるとき  \{| x_1, x_2, \cdots , x_m |\} = \{| y_1, y_2, \cdots , y_n |\} とします。

多重集合  \mathcal{X} = \{| x_1, x_2, \cdots , x_m |\} \mathcal{Y} = \{| y_1, y_2, \cdots , y_n |\} に対して

  •  \{| x_1, x_2, \cdots , x_m, y_1, y_2, \cdots , y_n |\} \mathcal{X} + \mathcal{Y} と書くことにします。
  •  \mathcal{X} + \mathcal{Z} = \mathcal{Y} となる多重集合  \mathcal{Z} が存在するとき  \mathcal{X} \le \mathcal{Y} \mathcal{Z} = \mathcal{Y} - \mathcal{X} と書くことにします。
  •  m \# \mathcal{X}と書くことにします。
  •  \displaystyle \prod_{i=1}^m x_i \displaystyle \prod \mathcal{X} と書くことにします。 \# \mathcal{X} = 0 のときは  \displaystyle \prod \mathcal{X} = 1 とします。

 \mathcal{Y} \le \mathcal{X} のとき  (\mathcal{X} - \mathcal{Y}) + \mathcal{Y} = \mathcal{X} となります。

 e: S \to \mathbb{N} に対して  \mathrm{supp}(e) \mathrm{supp}(e) = \{ x \in S \mid e(x) \ne 0 \} とおきます。

集合  S に対して  \mathrm{Bag}(S) \mathrm{Bag}(S) = \{ e: S \to \mathbb{N} \mid \mathrm{supp}(e) \ は有限集合 \} とおきます。

 e \in \mathrm{Bag}(S) \mathrm{supp}(e) = \{ x_1, \cdots, x_n \} のとき、 e は多重集合  \mathcal{X} = \{| \underbrace{x_1, \cdots, x_1}_{e(x_1)個}, \cdots, \underbrace{x_n, \cdots, x_n}_{e(x_n)個} |\} と同一視することができます。

 S \subseteq \mathbb{N} のとき  \displaystyle \prod \mathcal{X} = \prod_{x \in \mathrm{supp}(f)} x^{e(x)} が成り立ちます。

整数  a の倍数全体の集合を  (a) とします。
 \begin{eqnarray*}
P & = & \{ p \in \mathbb{N} \setminus \{0, 1\} \mid (x)(y) \subseteq (p) \implies (x) \subseteq (p) \lor (y) \subseteq (p) \} \\
 & = & \{ p \in \mathbb{N} \setminus \{0, 1\} \mid p \mid xy \implies p \mid x \lor p \mid y \}
\end{eqnarray*}
とおくとエレファントな整数論での議論より  P素数全体の集合となります( a \mid b b a で割り切れること、 \land は「かつ」、 \lor は「または」を表します)。

 \mathcal{P}, \mathcal{Q} \in \mathrm{Bag}(P) のとき、 \prod \mathcal{P} = \prod \mathcal{Q} ならば  \mathcal{P} = \mathcal{Q}

[証明]  \{| p |\} \le \mathcal{P} となる  p が存在しないとすると  \prod \mathcal{P} = 1 となります。 \prod \mathcal{P} = \prod \mathcal{Q} ならば  \prod \mathcal{Q} = 1 となって  \# \mathcal{Q} = 0 となるので  \mathcal{P} = \mathcal{Q} となります。

 \{| p |\} \le \mathcal{P} となる  p が存在するならば、 P の定義より  \{| p |\} \le \mathcal{Q} となります。 \mathcal{P}' = \mathcal{P} - \{| p |\} \mathcal{Q}' = \mathcal{Q} - \{| p |\} とおくと  \prod \mathcal{P} = \prod \mathcal{Q} より  \prod \mathcal{P}' = \prod \mathcal{Q}' となります。このとき  \mathcal{P}' = \mathcal{Q}' と仮定すると、 \mathcal{P} = \mathcal{P}' + \{| p |\} = \mathcal{Q}' + \{| p |\} = \mathcal{Q} となります。

よって  \# \mathcal{P} に関する機能法により主張が成り立ちます。[証明終わり]

これを数式の変形で書きます。
 \# \mathcal{P} = m とすると
 \begin{eqnarray*}
 &  & \left[ \ \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 & \Longleftarrow & \left[ \ \# \mathcal{P} = 0 \land \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 &  & \land \left[ \ \# \mathcal{P} \ne 0 \land \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 & \Longleftarrow & \left[ \ \# \mathcal{P} \ne 0 \land \prod \mathcal{P} = \prod \mathcal{Q} \implies \mathcal{P} = \mathcal{Q} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_1 + \{| p_1 |\} \land \prod \mathcal{P}_1 = \prod ( \mathcal{Q} - \{| p_1 |\} ) \implies \mathcal{P}_1 = \mathcal{Q} - \{| p_1 |\} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_2 + \{| p_1, p_2 |\} \land \prod \mathcal{P}_2 = \prod ( \mathcal{Q} - \{| p_1, p_2 |\} ) \implies \mathcal{P}_2 = \mathcal{Q} - \{| p_1, p_2 |\} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_3 + \{| p_1, p_2, p_3 |\} \land \prod \mathcal{P}_3 = \prod ( \mathcal{Q} - \{| p_1, p_2, p_3 |\} ) \right. \\
 & & \left. \implies \mathcal{P}_3 = \mathcal{Q} - \{| p_1, p_2, p_3 |\} \ \right] \\
 & \Longleftarrow & \\
 & \vdots & \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_m + \{| p_1, \cdots, p_m |\} \land \prod \mathcal{P}_m = \prod ( \mathcal{Q} - \{| p_1, \cdots, p_m |\} ) \right. \\
 & & \left. \implies \mathcal{P}_m = \mathcal{Q} - \{| p_1, \cdots, p_m |\} \ \right] \\
 & \Longleftarrow & \left[ \ \mathcal{P} =_\exists \mathcal{P}_m + \{| p_1, \cdots, p_m |\} \land \prod \mathcal{P}_m = \prod ( \mathcal{Q} - \{| p_1, \cdots, p_m |\} ) \right. \\
 & & \implies \left. \mathcal{P}_m = \mathcal{Q} - \{| p_1, \cdots, p_m |\} \ \right] \\
\end{eqnarray*}
となります。ここで  \mathcal{X} =_\exists \mathcal{Y} + \mathcal{Z} \mathcal{X} = \mathcal{Y} + \mathcal{Z} となる  \mathcal{Y} \mathcal{Z} が存在することを表すとします。最後の項は  \# \mathcal{P}_m = 0 なので成り立ちます。よって  \prod \mathcal{P} = \prod \mathcal{Q} ならば  \mathcal{P} = \mathcal{Q} となります。