hello worldはもう古い！自然数の定義からだろ！

●はじめに

二番煎じです。

関数型言語を学び始めたなら、hello worldより先に自然数の定義をするのが定石です。本稿では、最近私が学んだ言語での自然数の定義を紹介しようと思います。

●ペアノ自然数

ペアノの公理という以下の条件を満たすデータ型を定義します。学校で習う自然数とは異なり０も含むので、厳密にはペアノ自然数と呼ばれるものです。

1. 自然数 0 が存在する。

2. 任意の自然数 a にはその後者が存在する。

3. 0 はいかなる自然数の後者でもない。

4. 異なる自然数は異なる後者を持つ。

5. 0 がある性質を満たし、a がある性質を満たせばその後者 もその性質を満たすとき、すべての自然数はその性質を満たす。

１と２と３が分かれば問題ないです。要は、ゼロを表すデータと、引数の次の数字を返す関数を定義すれば終わりです。

●haskellの場合

data Nat = Zero | Suc Nat

ZeroとSuc Natという値を取るNat型を定義しています。Zeroは、それ自体をゼロを表す値として扱います。Sucは値コンストラクタという関数で、引数として与えられたNat型の値の次の数字を表します。具体的にどうやって数字を表すかを見たほうが理解が早いと思います。

Zero                 　が数字の０

Suc Zero          　が数字の１

Suc (Suc Zero) 　が数字の２

といった具合に、帰納的に全ての自然数を表現できる事がわかると思います。

●Agdaの場合

data ℕ : Set where

 zero : ℕ

 suc : ℕ → ℕ

haskellの場合と構造は同じですが、表記が若干異なります。data ℕ : Setはℕが型である事を宣言し、where以降で値を定義しています。zero : ℕはzero自体がℕ型である事を表しています。suc  : ℕ → ℕは、ℕ型を引数に取ってℕ型を返す関数である事を意味しています。

●Coqの場合

Inductive nat : Set :=  O : nat | S : nat -> nat

Agdaとほとんど同じです。

●最後に

説明を色々すっとばしてるので、まったくもって分かり難いとは思いますが、関数型言語の雰囲気だけでも分かってもらえれば幸いです。

かしこ。