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


# 自然数の定義

以下の5条件を満たす集合 N を **自然数** と呼びます：

1. 0 ∈ N が存在する
2. 任意の a ∈ N にはその「次」 a+ が存在する
3. a+ = 0 なる a は存在しない（N は 0 から始まる）
4. a ≠ b ならば a+ ≠ b+ （a+ は単射）
5. N では数学的帰納法が成立する

我々のよく知っている自然数 N = {0,1,2,...} が上の5条件を満たすことは明らかですが、ではこの「0」や「1」などの「数」はどこから出てきたのか？これらの数をちゃんと定義するには「自然数は何をもって自然数なのか」が定まってないといけない、ということでこの [ペアノの公理](http://ja.wikipedia.org/wiki/ペアノの公理) があります。

実際にこの公理を満たすような集合は構成できます。その代表が [ジョン・フォン・ノイマン](http://ja.wikipedia.org/wiki/ジョン・フォン・ノイマン) による構成法で、自然数一個一個を「集合」として作っていくのです。

## フォン・ノイマンの構成法

まず始まりである 0 は空集合 {} として、そこから、

* a+ = a ∪ {a} 

として、自然数を次々と定義していきます。

* 0 = {}
* 1 = 0+ = 0 ∪ {0} = {0}
* 2 = 1+ = 1 ∪ {1} = {0} ∪ {1} = {0, 1}
* 3 = 2+ = 2 ∪ {2} = {0, 1} ∪ {2} = {0, 1, 2}
* ...

という具合に。中身をバラして書けば、

* 0 = {}
* 1 = {0} = {{}}
* 2 = {0, 1} = {{}, {{}}}
* 3 = {0, 1, 2} = {{}, {{}}, {{}, {{}}}}
* ...

と、それぞれの数は「空集合の集合の集合…とかの集合」になってるわけです（こんなものを思いつくなんて変態だ）。

a+ の定義より、

* a ⊂ a+

なので、包含関係 ⊂ を ≦ と書くことにすれば 0 < 1 < 2 < ... となって N は全順序集合となるのです。

## 和・積の定義

自然数の和 a + b を：

* a + 0 = a
* a + b+ = (a + b)+

によって定義します。2つめの式は「0 でない数は b+ と書ける」ことに依っています。+ して b になる数を b- と書くことにすれば：

* a + b = (a + b-)+

と書けます。こうして + を掃き出しながら b を 0 まで下げていくことができるので、任意の数の組に対して和が定義できるのです。例えば：

```
3 + 2 = (3 + 1)+
      = ((3 + 0)+ )+
      = (3+ )+
      = 4+
      = 5
```

という具合に。

同様に自然数の積 a x b を：

* a x 0 = 0
* a x b+ = (a x b) + a

と定義します。すると、

```
3 x 2 = (3 x 1) + 3
      = ((3 x 0) + 3) + 3
      = (0 + 3) + 3
      = 3 + 3
      = 6
```

と、積もちゃんと定義できます。このように**何の実体の存在も仮定せず**、**空集合と集合演算**だけから自然数が作れちゃうというところが変態的にストイックで良いですよね。

# では、実装しましょう！

早速 Swift で **Array** だけを使ってフォン・ノイマン型の自然数を構成してみましょう。まずは箱として：

```swift
struct N: Printable {
    private let val: [Any]
    
    private init(_ val: [Any]) {
        self.val = val
    }
    
    static var zero: N {
        return N([])
    }
    
    var description: String {
        return "\(val)" // for debug
    }
}
```

`val` に実体としての配列が入ります。外から勝手に変な配列を入れられては困るので init は private にした上で、空配列を持つ定数 `zero` を置いています。次に 1, 2, ... を作っていけるように、後置単項演算子 `+` を定義します：

```swift
postfix operator + {}
postfix func +(n: N) -> N {
    return N(n.val + [n.val]) // この + は配列の結合
}
```

そして実際にやってみると…

```swift
let n0 = N.zero
let n1 = n0+
let n2 = n1+
let n3 = n2+

println("n0: \(n0)")
println("n1: \(n1)")
println("n2: \(n2)")
println("n3: \(n3)")
```

```console
n0: []
n1: [[]]
n2: [[], [[]]]
n3: [[], [[]], [[], [[]]]]
```

おー、ちゃんとできていますね。いい感じに変態的です。

### 和・積の定義

次に和を定義したいのですが、先に `a-` を定義しておきます：

```swift
postfix operator - {}
postfix func -(n: N) -> N {
    if n.val.isEmpty {
        assertionFailure("0- doesn't exist.")
    }
    return N(n.val.last as [Any])
}
```

`last` を使っているのが若干ずるい感じがしますが（最後の要素が一個前の数になっていることを使っています）、そこは勘弁してください。それでは和を定義します：

```
func +(n: N, m: N) -> N {
    if m.val.isEmpty {
        return n
    } else {
        return (n + m-)+
    }
}
```

`m` を `0` まで減らしていく再帰的な定義になっています。そして、


```swift
let n5 = n3 + n2
println("n5: \(n5)")
```

実行してみると…

```console
n5: [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]
```

おっとこれは…早くも人智を超えてしまいました。仕方ないので **デバッグ用** に、その自然数と配列の個数が一致していることを使って、

```swift
    var description: String {
        return "\(val.count)" // for debug
    }
```

としておきましょう。あくまでデバッグ用です。自然数が定義できてない世界に `count` などあり得ないのですから。そうすると、

```console
n5: 5
```

となり、ちゃんと計算できてそうなことがわかりました。

積も定義通り：

```swift
func *(n: N, m: N) -> N {
    if m.val.isEmpty {
        return N.zero
    } else {
        return (n * m-) + n
    }
}
```

とすると、

```swift
let n6 = n3 * n2
println("n6: \(n6)") // n6: 6
```

となり、ちゃんと計算できていそうです！
和と積の組み合わせでも、

```swift
let m = (n2 + n3) * n6
println("m: \(m)") // m: 30
```

でちゃんとできています！ちなみに 30 の中身を見てみようとしたら、シミュレータがフリーズしてしまいました。`[]` の数は指数関数的に増えるので仕方ないです。

### イコールの定義

`n.val == m.val` としてイコールを定義したいのですが、配列の要素が `Any` 型となっているためできませんでした（`val: [Equatable]` と書くことも許されない…Swiftは厳しい）

仕方がないので、イコールも再帰的に定義することにしましょう。

```swift
struct N: Equatable, Printable {
    ...
}

func ==(n: N, m: N) -> Bool {
    if (n.val.isEmpty && m.val.isEmpty) {
        return true
    } else if (n.val.isEmpty || m.val.isEmpty) {
        return false
    } else {
        return (n- == m-)
    }
}
```

共にゼロなら真、一方がゼロなら偽、そうでなければ共に1ずつ減らして再確認、という感じです。これでちゃんとイコールが定義できるのは、公理(4)が保証しています。

という訳で、 **自然数が実装できました！**

### 整数リテラルにも対応しておく

無事実装もできたことですし、毎回 `(((N.zero)+)+...` と書かなきゃいけないのは面倒なので、整数リテラルからも生成できるようにしておきましょう。 Swift では `IntegerLiteralConvertible` プロトコルを実装することで対応できます。

```swift
struct N: Equatable, Printable, IntegerLiteralConvertible {
    ...
    
    init(integerLiteral value: IntegerLiteralType) {
        var n = N.zero
        for i in 0..<value {
            n = n+
        }
        self.val = n.val
    }
}
```

そうすると、

```swift
let a: N = 4
let b: N = 6
println("a + b: \(a + b)") // a + b: 10
```

おー、とても自然数っぽくなりました！
でも、中身を覗いてみると…

```swift
a + b: 10 = [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]]]]]]
```

どうもありがとうございました。

---

ソースコードはこちら： [PeanoNatural.swift](https://gist.github.com/taketo1024/d60e0b8ba479921f7b16)
宣伝：数学ブログ書いてます：[Imaginary, Imaginative](http://taketo1024.hateblo.jp)