エレファントな整数論では、素因数分解の一意性のわかりやすい記法を考えていたのですが、良い方法ができず止まっていました。ここでは、数式ではなくプログラミング言語を使って書くとどうなるか考えていきたいと思います。まず、エレファントな整数論(18)、(19)で書いた内容を書いておきます。
整数の素因数分解の多重集合としての一意性
重複度を含めた集合を多重集合(wikipedia:多重集合参照)と呼びます。多重集合 とは、通常の集合とは異なり、 の中に重複するものがあったとき、その出現する回数が異なれば多重集合としては異なるものとするものです。
多重集合 と は全単射 が存在して任意の に対して であるとき とします。
多重集合 と に対して
- を と書くことにします。
- となる多重集合 が存在するとき 、 と書くことにします。
- を と書くことにします。
- を と書くことにします。 のときは とします。
のとき となります。
に対して を とおきます。
集合 に対して を とおきます。
、 のとき、 は多重集合 と同一視することができます。
のとき が成り立ちます。
整数 の倍数全体の集合を とします。
とおくとエレファントな整数論での議論より は素数全体の集合となります( は が で割り切れること、 は「かつ」、 は「または」を表します)。
のとき、 ならば
[証明] となる が存在しないとすると となります。 ならば となって となるので となります。
となる が存在するならば、 の定義より となります。、 とおくと より となります。このとき と仮定すると、 となります。
よって に関する機能法により主張が成り立ちます。[証明終わり]
これを数式の変形で書きます。
とすると
となります。ここで は となる と が存在することを表すとします。最後の項は なので成り立ちます。よって ならば となります。