はじめに

「そういえば第1章の1.1のペアノ自然数の加算乗算の推論規則、Swiftのenumで楽に再現できそうだなー」

とふと思いました。

そこでやってみたら案外楽しかったので、Advent Calendarの記事として残しておくことにしました。

環境

Swift5.1で動作確認していますが、多分Swift4くらいまで動くと思います。

ペアノ自然数って？

私達は日常生活では通常アラビア文字を利用しています。

ペアノ自然数¹とは、これをSとZと(と)で表現したものです。

Z          => 0
S(Z)       => 1
S(S(Z))    => 2
S(S(S(Z))) => 3

Sは successor(次に来るもの)の頭文字を取ったものです。
簡単に言えばInt型で使える++と似ているようなものと考えてください。²

Zは0とすると、S(Z)はZの次なので1ですね。

では、Swiftのenumでそれっぽいものを作ってみましょう。

// ペアノ自然数
indirect enum N {
    // N + 1
    case S(N)
    // 0
    case Z
}

はい、Associated Valuesを使えば簡単にできますね。
Sでは再帰的にまた列挙型Nを利用するので、enumの宣言の先頭にindirectが必要です。

加算はどうやるの？

加算/乗算は以下の推論規則で証明することができます。(N1, N2, N3にはペアノ数が入ります。)

Z + N1 = N1
N1 + N2 = N3 ならば S(N1) + n2 = S(N3)

これらの推論規則³を利用して、ペアノ数での加算の結果を算出したいと思います。
では、実装するとどうなるでしょうか？

// 足し算の推論規則
// lhs + rhsの結果を出している
func +(lhs: N, rhs: N) -> N {
    switch lhs {
    case .Z:
        // 0 + N1 = N1
        return rhs
    case .S(let value):
        // N1 + N2 = N3 -> S(N1) + N2 = S(N3)
        return .S(value + rhs)
    }
}

これが正しいかを検証するために、ペアノ数をアラビア数に変換する関数を定義します。

indirect enum N {

    ... // さっきのコードと同じなので省略

    // デバッグ用、ペアノ自然数 -> アラビア数字
    func print() -> Int {
        var selfValue: N = self
        var i: Int = 0

        while true {
            if case .S(let value) = selfValue {
                selfValue = value
                i += 1
            } else {
                return i
            }
        }
    }
}

では、試してみるとあら不思議、ちゃんと正しく計算されています。

(.S(.S(.Z)) + .S(.S(.Z))).print()          // 4
(.S(.S(.Z)) + .S(.Z)).print()              // 3
(.Z + .Z).print()                          // 0

実装の考え方

詳しい実装の考え方について、フォーカスします。

`Z + N1 = N1` について

まず、Z + N1 = N1に関しては、片方がゼロ(Z)であれば、N1の値をそのまま返せば良いことになります。これは簡単。

case .Z:
   // 0 + N1 = N1
   return rhs

`N1 + N2 = N3 -> S(N1) + N2 = S(N3)` について

N1 + N2 = N3 -> S(N1) + N2 = S(N3) が曲者ですが、次のように考えると簡単に実装できます。

この規則は言い換えれば

N1 + N2さえ求めることできれば、N1 + N2の結果をSでくるむとS(N3)も求まる

という意味です。

一歩進んで考えると、

N1 + N2の証明がいまは無理なら、N1 - 1 + N2⁴を導き出してみる
その結果をSでくるめば(+ 1 すること)、N1 + N2が導き出せる
N1 + N2の結果をSでくるむとS(N3)も求まる（再掲）

と考えればよいです。

そうなると次はN1 - 1 + N2の証明に移ればいいですが、N1 - 1 をやっていけば、いずれかはゼロ(Z)に到達するし、その時の規則はすでに以下のように証明されているので、一番目のcaseの実装に行くということになります。

Z + X = X (上のN1と混同するのでXに置換)

まとめると、

N1 + N2の証明がいまは無理なら、N1 - 1 + N2⁴を導き出してみる（再掲）
N1 - 1 + N2⁴を導き出していこうとすると、１番目の Z + X = X の推論規則になる（再掲）

その結果をSでくるめば(+ 1 すること)、N1 + N2が導き出せる（再掲）

例）2 + 1

S(S(Z)) + S(Z)   // 2 + 1
S((S(Z)) + S(Z)) // (1 + 1) + 1
S(S(Z + S(Z)))   // (0 + 1) + 1 + 1
// Z + S(Z) = S(Z) に置換できる
S(S(S(Z)))

N1 + N2の結果をSでくるむとS(N3)も求まる（再掲）

// value は N1 - 1
case .S(let value):
   // N1 + N2 = N3 -> S(N1) + N2 = S(N3)
   // 結局はS(N1 - 1 + N2) をしている
   return .S(value + rhs)

おまけ

https://gist.github.com/freddi-kit/248ce9f1cb33510a7067f94b440c51b6 にソースをまとめていますが、掛け算もあるので見てみてください。
もし、自分の力でチャレンジしたければ以下に推論規則を書いておきます。これはそれなりに難しいと思います。

0 * N = 0
N1 * N2 = N3 かつ N2 + N3 = N4 ならば S(N1) * N2 = N4

余談

C++だとこうなるらしい。

ペアノはジュゼッペ・ペアノさんの名前からとったもの ↩
あくまで、「似ているよねー」くらいの話で性質は全然違います。++は「対象の値をインクリメントする演算子」ですが、S(N)は「Nの次の数の表現」であることは念頭に入れてください。 ↩
こんな短い注釈で推論規則を解説するのは難しいですが、例えば文中のN1 + N2 = N3やS(N1) + n2 = S(N3)はそれぞれ一つのルールになっていて、そのいくつかのルールから生み出されたルール(規則)を指します。「N1 + N2 = N3ということがなら、そこからS(N1) + n2 = S(N3)が導き出せる」というルールができていますね。興味があれば論理学の大学の資料を見ると良いかも。 ↩
わかりやすく- 1という記法を使っていますが、ペアノ数での定義上この書き方は間違いなので注意。エラーで言うとシンタックスエラーです。 ↩

ペアノ自然数とペアノ自然数での加算の推論規則をSwiftで表現してみる