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」などの「数」はどこから出てきたのか？これらの数をちゃんと定義するには「自然数は何をもって自然数なのか」が定まってないといけない、ということでこの ペアノの公理 があります。

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

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

まず始まりである 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 だけを使ってフォン・ノイマン型の自然数を構成してみましょう。まずは箱として：

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, ... を作っていけるように、後置単項演算子 + を定義します：

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

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

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)")

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

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

和・積の定義

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

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 まで減らしていく再帰的な定義になっています。そして、

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

実行してみると…

n5: [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]], [[], [[]], [[], [[]]], [[], [[]], [[], [[]]]]]]

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

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

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

n5: 5

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

積も定義通り：

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

とすると、

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

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

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

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

イコールの定義

n.val == m.val としてイコールを定義したいのですが、配列の要素が Any 型となっているためできませんでした（val: [Equatable] と書くことも許されない…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 プロトコルを実装することで対応できます。

struct N: Equatable, Printable, IntegerLiteralConvertible {
    ...

    init(integerLiteral value: IntegerLiteralType) {
        var n = N.zero
        for i in 0..<value {
            n = n+
        }
        self.val = n.val
    }
}

そうすると、

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

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

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

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

---

ソースコードはこちら： PeanoNatural.swift
宣伝：数学ブログ書いてます：Imaginary, Imaginative