Haskellの自然数が自然数じゃないという話(?)

12/26 追記

断定で書くほど、よくわかってる話でもないので、タイトルに疑問符追加

Haskellで、自然数の集合に対応する型は、以下のように定義できるように思えます (ここでの自然数は、0を含んでいるとします)。

自然数(?)Natの定義

data Nat = O | S Nat

以下のように、0,1,2に対応するNat型の値を定義することが出来ます。

zero :: Nat
zero = O

one :: Nat
one = S O

two :: Nat
two = S (S O)

問題点

しかし問題は、以下の様な定義もできてしまうことです。

omega :: Nat
omega = S omega

omegaは、どのように評価されるのでしょうか?

omega
~> S omega
~> S (S omega)
~> S (S (S omega))
.
.
.
~> S (S (S (S (S ....

ということで、無限に対応するような値が、Nat型の中に入り込んでしまいました。

イメージ図

自然数って、以下の様な構造を持っているイメージですよね。

しかしHaskellのNatには、omegaが混じってしまっているので、以下の様なイメージです。

図がきたねぇ。

他にも色々不純物

omega以外にも、Natには以下の様なものも混じっています。

omega1 :: Nat
omega1 = S omega2

omega2 :: Nat
omega2 = S omega1

omega' :: Nat
omega' = omega'

なんとなく、omegaとomega1,omega2は結局同じもの、という気がしますが。

Nat型と数学的帰納法

上の図を見ていただけばなんとなく納得できると思うのですが、Nat型に関する性質を証明したいときには、普通の数学的帰納法では不十分です。

表示的意味論やらなんやらでがんばらないといけません。といっても、実際そんなに難しい手法になるわけではないようですが。

参考資料

関数プログラミング入門 ―Haskellで学ぶ原理と技法―

元ネタはこの本です。

数学ガール ゲーデルの不完全性定理 (数学ガールシリーズ 3)

とても丁寧な「ペアノの公理」の説明がのってます。