数の型を作る(自然数編)

— 数の型を作る(自然数編) —

最終更新日:2025-10-31

local_offer数の型を作るlocal_offer型local_offerHaskell

この記事の目標は、Haskellで自然数の型を構成することである。その為、プログラムの意図が伝わることを意識し、形式的で厳密な議論は避けた部分がある。その詳細についてはいつか(自分が生きている間とは限らないが)記事にしようと思う。

なお、この記事ではHaskellの基本的な文法は仮定した。(Haskellの文法が分からないと記事が読めないのならば、プログラムの意図も伝わらないのでは？と指摘されれば、返す言葉がない🥲)

Peanoの公理

自然数を構成する前に、自然数とは何かをはっきりさせておく必要がある。数学に於いて何かを定義する際に重要となるのは、その定義が、定義する対象の本質的な性質を捉えているかどうかということである。自然数とは何かということを考えたとき、自然数の持つ豊かな構造と性質—順序、加法、乗法、数学的帰納法など—を思い浮かべるだろう。しかし、本質的に重要な性質のみを整理するのは、そう簡単なことではない。

自然数を自然数たらしめる本質的な性質を見事に捉え、公理化したのが次に述べるPeanoの公理である。

▷定義 (Peano系)

集合 $N$ に対し、三つ組 $(N,s,0)$ が以下の条件を満たすとき、これをPeano系という。

(P1). $0\in N$ である。
(P2). $s$ は $N$ から $N$ への写像である。
(P3). $s$ は単射である。
(P4). 全ての $n\in N$ に対し、 $s(n)\neq 0$ である。
(P5). $N$ の部分集合 $S$ が

0\in S\wedge (n\in S \Rightarrow s(n)\in S)

を満たすとき、 $S=N$ となる。

この(P1)から(P5)の条件をPeanoの公理という。Peano系 $(N,s,0)$ を自然数と呼ぶことにする。

□

例えば、我々がよく知っている自然数全体の集合

\mathbb{N}

に対し、写像

s:\mathbb{N}\to \mathbb{N}

を

s(n)=n+1

と定めれば、三つ組

(\mathbb{N},s,0)

はPeano系である。ただし、自然数を定義しようという流れの中では、まだ

\mathbb{N}

を使うことはできないので、これは実際にはPeano系を構成しているわけではないことに注意する。

この記事ではPeano系についての詳細は述べないが、とりあえずこの5つの条件でもって自然数を特徴付けるのだということを頭に入れておこう。

Peano系を型で実装する

では、ここから(P1)から(P5)の条件を満たすような型を実装していく。まずは型Natを定義しよう。

・Nat型を定義する

気持ち的に、Nat型はZeroを含んでおり、その他の元は再帰的にSucc Natのような形をしていて欲しい。したがって、Nat型を次のように定めることにする：

つまりNat型とは、ZeroかSucc Natの形をしたものの集まりである。例えば、Succ ZeroやSucc (Succ Zero)などはNat型の値になる。この段階で、SuccというNatからNatへの関数が定まっており、Natの元としてZeroを定義している。つまり、三つ組(Nat,Succ,Zero)はPeano公理系の(P1)と(P2)そして(P5)を満たしている。実際、(P1)と(P2)に関してはそのまま成り立ち、Natの定義から、Natの値の集まりSがZeroを含み、そしてmがSの値であればSucc mもSの値となれば、Sは当然Zero,Succ (Zero), Succ (Succ Zero),...も全て含むことになり、これはNatに他ならない。

今回、Natを再帰的に定義したので、Natが(P5)を満たすのは当たり前になっているが、一般にはPeano系に対して再帰的な関数を定義する際、再帰定理を使うことになる。再帰定理についてはwikipediaを参照。

・等号を定める

あとはNat型が(P3)と(P4)を満たすことを示せば良い。しかし、このままでは(P3)と(P4)の条件以前に、そもそもNatに於ける等しさが定義されていない。まずは、Nat型に等しさの概念を導入しよう。すなわちこれは、NatをEq型クラスのインスタンスにするということである。

Haskellで定義した型を型クラスのインスタンスにするには、再帰的な定義を用いる。このとき、再帰的な定義の基本となるのは、その定義のスタート地点である。Nat型のスタート地点はZeroであり、まずはこれに関する定義から記述してみる：

これで等号==の右辺か左辺のどちらかがZeroの場合は定義できた。一般的な(Succ m) == (Succ n)という形の場合には対応できていない。そこで、一般的な形の定義式を追加することで、晴れてNatをEq型クラスのインスタンスにすることができる。

これでNatに等号が定義できたことを確認してみよう。最後に追加した(Succ m) == (Succ n) = m == nの部分は、数学的には後者関数

s

に対し、

s(m)=s(n)

を

m=n

として定める。ということであるが、そもそもNatの定義を思い返すと、Natの値は必ずZeroかSucc Natの形をしているので、Succ mをmに置き換えることで、Succ mの一つ前の値mを評価するということになり、これを繰り返すといづれZeroを含む場合の等号に話が置き換わるのである。

を判定したかったとする。このとき、==の定義から、これは両辺から外側のSuccを省いたSucc (Succ Zero) == Succ Zeroと同値である。また同様に、これはSucc Zero == Zeroと同値になる。これはFalseであると定義したので、元の式Succ (Succ (Succ Zero)) == Succ (Succ Zero)もFalseになる。

もうこの段階で、(Nat,Succ,Zero)が(P3)と(P4)の条件を満たし、したがってこれがPeano系になることが示せる。実際、(P3)は等号の定義(Succ _) == Zero = FalseとZero == (Succ _) = Falseから示せるし、また、(P4)は等号の定義(Succ m) == (Succ n) = m == nから示せる。

・順序を入れる

さて、次はNatに順序を入れる、即ちNatをOrd型クラスのインスタンスにしよう。Ord型クラスのインスタンスにするには、Natに対してcompare関数を定めればよい。Nat上の順序は、二つのNatの値Succ (Succ (Succ ...))とSucc (Succ (Succ ...))があったとき、外側のSuccの個数が多ければそちらが値として大きいと考えるのが自然である。では、これも等号の時と同じようにZeroを含む式から始めて実装する。

もちろんZeroはNatの中で最も小さいものとしたいので、Zeroと(Succ _)では必ず(Succ _)の方が大きいとした。最後に一般的な形について定義し、順序が完成する：

ghciで試してみると、次のようにきちんと動作することがわかる：

・加法と乗法を定める

加法についてだが、まずはZeroは何と足しても値が変わらないようにする。一般の形の場合は、通常の自然数で

m+(n+1)=(m+n)+1

つまり

m+s(n)=s(m+n)

が成り立つことを用いて再帰的に定義する。したがって、プログラムは次のようになる：

例えば、ghciで実験してみると、次のような出力が得られる：

次に乗法を定めよう。こちらも加法の時と同じ様に定めれば良い。まずはZeroに何をかけてもZeroとなるようにし、通常の自然数においては

m\times (n+1)=m\times n + m

即ち

m\times s(n)=m\times n+m

が成り立つことを用いると、プログラムは次の様になる：

最後に

以上でHaskellの型システムを用いて自然数を定義することができた。プログラムの全体を以下に記す：

この記事で解説を省いたもの—再帰定理やPeano算術、そして自然数全体の一意性など—はwikipediaやTAIKEI-BOOKなどを適宜参照されたい。

Peanoの公理

Peano系を型で実装する

・Nat型を定義する

・等号を定める

・順序を入れる

・加法と乗法を定める

最後に

・`Nat`型を定義する