Go to Qiita Advent Calendar 2024 Top
LoginSignup
4
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 3 years have passed since last update.

プロデルAdvent Calendar 2019

Day 24
@Mopepe51(雪下)

自然数を作る in 日本語プログラミング言語「プロデル」

Last updated at Posted at 2019-12-24

自然数

みなさん、自然数ってご存知でしょうか？
そう、0, 1, 2, 3,……というあれです。0は自然数です。いいですね？
（どうしても0が自然数では嫌だと言う方は1から始まる自然数について後半でお話するので我慢してください。）

しかし、「……」ってなんだよ、と思いませんか？ 3の次は実は௵かもしれないですよね？
いや、別に3の次の数が௵と書かれていても構わないのですが、どんなものが「……」に入るのか、はっきり書く方法を考えてみましょう。

ペアノの公理

上記の「自然数の定義」を数学的に規定したものの一つに「ペアノの公理」というものがあります

  1. 自然数 0 が存在する。
  2. 任意の自然数 a にはその後者 (successor)、suc(a) が存在する（suc(a) は a + 1 の "意味"）。
  3. 0 はいかなる自然数の後者でもない（0 より前の自然数は存在しない）。
  4. 異なる自然数は異なる後者を持つ：a ≠ b のとき suc(a) ≠ suc(b) となる。
  5. 0 がある性質を満たし、a がある性質を満たせばその後者 suc(a) もその性質を満たすとき、すべての自然数はその性質を満たす。

－ーWikipedia ペアノの公理より

「後者」、すなわち次の数を次々に「自然数」としていくこと、0からの分岐・合流・終端のないシリーズ1本だけを自然数とすることを規定しています。

ジョン・フォン・ノイマンの構成法

「0が存在する」と言われても、その「0」って何なんだ、という気持ちになりますね。
実のところ何でも良いのですが、ここは我々のよく知る（本当によく知っているのかどうかについてはさておき）「集合」で構成してみましょう。

  1. 0 := {}
  2. $suc(x)$ := $x$$\cup${$x$}

0は{}＝∅（空集合）に対応します。ゼロのイメージとも合致してわかりやすいですね。
1, 2, 3, ……はそれぞれ{{}}={0}、{{}, {{}}}={0, 1}、{{}, {{}}, {{}, {{}}}={0, 1, 2}、……のようにそれ未満の自然数をすべて含むという形になります。

これ以外にも様々な構成法が存在しますが、上記のペアノの公理を満たして構成された「自然数」はすべて同型（一対一の対応を作れる） ことがわかっています。1

自然数を作る

さて、上記で定義した「自然数」をプロデルで作ってみましょう。

まず、自然数という種類(クラス)にデータとしてノイマンの構成法に従い実体という配列を持たせます。
次の数はｘ＋{ｘ}という配列を実体に持つ自然数を生成して返します。

自然数
自然数とは
  【実体：配列】を持つ
  はじめ(実体)の手順
    自分の実体は、実体
  終わり
  [自分]の、次の数を求める手順
    【甲】は、自分の実体のクローン
    甲へ、自分の実体のクローンを、追加する
    自然数(甲)を作ったものを返す
  終わり

2

ここまでで上記の「自然数」は完成です。ゼロを零として3 1,2,3を計算してみましょう。

零という自然数({})を作る
零の実体を表示
//=> {}
零の次の数の実体を表示
//=> {{}}
零の次の数の次の数の実体を表示
//=> {{}, {{}}}
零の次の数の次の数の次の数の実体を表示
//=> {{}, {{}}, {{}, {{}}}

加算・乗算

さて、「自然数」というからには足し算・掛け算くらいはできてほしいものです。
(引き算・割り算は自然数に関して閉じていない(計算結果が自然数であるとは限らない)ため今回は省きます。)

足し算は

  1. $x+0=x$
  2. $x+suc(y)=suc(x+y)$

のように書けます。
第2オペランドが0になるまで$y$回繰り返して2.を使うので、$x+y=x +1…(y回)…+1$という計算になりますね。

掛け算は、

  1. $x\times 0=0$
  2. $x\times suc(y)=x\times y +x$

となります。こちらは$x\times y=x+…(y回)…+x$という計算になります。4

さて、これをプロデルで実装する……前に、加積の計算では$suc$を外すという操作が必要になるので前の数の手順と、ついでに等しいを判定する手順を定義しておきましょう。

0の前の数は存在しないのでエラーを投げます。
それ以外では$suc(x)=${1,2,……,$x$}の最後の要素$x$を返すようにします。自然数の実体は配列で実装されているので末尾で最後の要素を取得できます。
等しいの判定はどちらかが0になるまで前の数をさかのぼり、判定を行います。

「自然数」続き
  [自分]の、前の数を求める手順
    例外監視
      もし自分の実体＝{}ならば
        「０の前の自然数はありません」というエラーを発生させる
      そうでなければ
        自然数(自分の実体の末尾)を作ったものを返す
      もし終わり
    発生した場合
      エラーのメッセージを警告アイコンで表示する
    監視終わり
  終わり
  [自分]と、[他の数]が、等しいかどうかを判定する手順
    もし自分の実体＝{}かつ他の数の実体＝{}ならば
      ○を返す
    他でもし自分の実体＝{}かつ他の数の実体≠{}
        または自分の実体≠{}かつ他の数の実体＝{}ならば
      ×を返す
    そうでなければ
      自分の前の数と、他の数の前の数が等しいかどうかを返す
    もし終わり
  終わり

それでは改めて足し算・掛け算を実装します。

「自然数」続き
  [自分]と、[他の数]を、足す手順
    もし他の数の実体＝{}ならば
      自分を返す
    そうでなければ
      自分と、(他の数の前の数)を、足して【和】とする
      和は、和の次の数
      和を返す
    もし終わり
  終わり
  [自分]と、[他の数]を、掛ける手順
    もし他の数の実体＝{}ならば
      自然数({})を作ったものを返す
    そうでなければ
      自分と、(他の数の前の数)を、掛けて【積】とする
      積は、積と、自分を足したもの
      積を返す
    もし終わり
  終わり
終わり

それではまずかの有名な「1+1=2」が正しいかどうか計算してみましょう。

零という自然数({})を作る
壱は、零の次の数
弐は、壱の次の数
壱と壱を足したものと、弐が等しいかどうかを表示
//=> ○

無事正解となりました！
同様に色々な計算ができます。

参は、弐の次の数
肆は、参の次の数
参と壱を足したものと、(弐と弐を足したもの)が、等しいかどうかを表示
//=> ○
弐と弐を掛けたものと、肆が、等しいかどうかを表示
//=> ○

「１から始まる自然数」

さて、自然数が作れてめでたしめでたしといったところですが、やはり自然数は１から始まるものだと考える人も多いでしょう5。
0を含まない流儀での自然数も定義してみましょう。

  1. 自然数 1 が存在する。
  2. 任意の自然数 a にはその後者、suc(a) が存在する
  3. 1 はいかなる自然数の後者でもない。
  4. 異なる自然数は異なる後者を持つ：a ≠ b のとき suc(a) ≠ suc(b) となる。
  5. 1 がある性質を満たし、a がある性質を満たせばその後者 suc(a) もその性質を満たすとき、すべての自然数はその性質を満たす。

自然数そのものの定義は前述の定義で0を1に換えるだけでOKです。また、具体的構成もノイマンのものの「1」をそのまま使って大丈夫でしょう。

  1. 1 := {{}}
  2. $suc(x)$ := $x$$\cup${$x$}

一方計算については定義で0の性質を組み込んでしまっているため代わりに1を使った定義が必要です。
足し算：

  1. $x+1=suc(x)$
  2. $x+suc(y)=suc(x+y)$

掛け算：

  1. $x\times 1=x$
  2. $x\times suc(y)=x\times y +x$

としてみました。
これをプロデルで実装すると以下のようになります。(上の自然数との区別のため便宜上「正整数」という名前になっています)

正整数とは
 【実体：配列】を持つ
  はじめ(実体)の手順
    自分の実体は、実体
  終わり
  [自分]の、次の数を求める手順
    【甲】は、自分の実体のクローン
    甲へ、自分の実体のクローンを、追加する
    正整数(甲)を作ったものを返す
  終わり
  [自分]の、前の数を求める手順
    例外監視
      もし自分の実体＝{{}}ならば
        「１の前の正整数はありません」というエラーを発生させる
      そうでなければ
        正整数(自分の実体の末尾)を作ったものを返す
      もし終わり
    発生した場合
      エラーのメッセージを警告アイコンで表示する
    監視終わり
  終わり
  [自分]と、[他の数]が、等しいかどうかを判定する手順
    もし自分の実体＝{{}}かつ他の数の実体＝{{}}ならば
      ○を返す
    他でもし自分の実体＝{{}}かつ他の数の実体≠{{}}
        または自分の実体≠{{}}かつ他の数の実体＝{{}}ならば
      ×を返す
    そうでなければ
      自分の前の数と、他の数の前の数が等しいかどうかを返す
    もし終わり
  終わり
  [自分]と、[他の数]を、足す手順
    もし他の数の実体＝{{}}ならば
      自分の次の数を返す
    そうでなければ
      自分と、(他の数の前の数)を、足して【和】とする
      和は、和の次の数
      和を返す
    もし終わり
  終わり
  [自分]と、[他の数]を、掛ける手順
    もし他の数の実体＝{{}}ならば
      自分を返す
    そうでなければ
      自分と、(他の数の前の数)を、掛けて【積】とする
      積は、積と、自分を足したもの
      積を返す
    もし終わり
  終わり
終わり

壱という正整数({{}})を作る
弐は、壱の次の数
参は、弐の次の数
肆は、参の次の数

壱と壱を足したものと、弐が等しいかどうかを表示
//=> ○
弐と弐を掛けたものと、肆が等しいかどうかを表示
//=> ○

$\mathbb{N}:=\mathbb{Z}_{>0}$バージョンも計算ができました。
今度こそめでたしめでたし。

参考：
Swiftで自然数を作ってみた（ペアノの公理）
Wikipedia ペアノの公理

2019/12/24：記事公開
2019/12/24：参考文献を追記
2019/12/24：次の数、前の数手順を「名詞型手順」として自然な活用形に変更
2020/10/17:「1から始まる自然数」乗法の定義修正

  1. Wikipedia ペアノの公理#存在と一意性 ↩

  2. 「名詞型手順」：式で戻り値を返す手順では～～する手順のような動詞型の定義の代わりに～～の手順、～～を求める手順のような形で定義し、～～と呼び出すことが可能です。ver1.7からの機能ということですが動いたので良しとします。流石に「次の数手順」では日本語として不自然なので……。参考：動詞型手順と名詞型手順―プロデルブログ ↩

  3. ところでプロデルでは〇(漢数字ゼロ)は真偽値のtrueリテラル○(まる)と同一視されています。開発者様の記事マイナスと丸の全角文字の話では「数字をわざわざ漢数字で入れることは考えにくいので漢数字は無視しても困らないでしょう...」とありましたがこれが数少ない漢数字ゼロの使用場面となりました。（結局零で良かったですが……） ↩

  4. 何とは言いませんがこの定義でははっきりとxとyに順序があるわけですね。もちろん交換法則は証明できますがそこそこ大変です。ほぼ同じ証明を https://ykst51.blogspot.com/2019/12/blog-post.html に示してあります。何とは言いませんが。 ↩

  5. 実際、「ペアノの公理」の原型を作ったペアノ本人も、原論文では「１」を始点として定義していたようです。Wikipedia ペアノの公理#ペアノ自身による記述 ↩

4
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
4
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?