※現在、ブログ記事を移行中のため一部表示が崩れる場合がございます。
順次修正対応にあたっておりますので何卒ご了承いただけますよう、お願い致します。

Haskellで自然数を定義してみる


2012年 11月 07日

Haskells.jpg

第3章は数値である。
ちゃんと、自然数を扱ってみようというわけだ。
それで、次のように加算(+)を本に従って定義してみた。

data Nat = Zero | Succ Nat
     deriving (Eq,Ord,Show)

(+)  :: Nat -> Nat -> Nat
m + Zero    = m
m + Succ n  = Succ ( m + n )

しかし、これではエラーになってしまった。

*Main> :l 3.1_1
[1 of 1] Compiling Main             ( 3.1_1.hs, interpreted )

3.1_1.hs:6:24:
    Ambiguous occurrence `+'
    It could refer to either `Main.+', defined at 3.1_1.hs:5:3
                          or `Prelude.+',
                             imported from `Prelude' at 3.1_1.hs:1:1
                             (and originally defined in `GHC.Num')

Prelude+ なのか、ここで定義した + なのか分からないと言われている訳だ。
仕方がないので、必要な演算には全部 Main.+ をつけてみた。
そして、乗算、べき乗も加えてみた。

data Nat = Zero | Succ Nat
     deriving (Eq,Ord,Show)

(+)  :: Nat -> Nat -> Nat
m + Zero    = m
m + Succ n  = Succ ( m Main.+ n )

(*)  :: Nat -> Nat -> Nat
m * Zero    = Zero
m * Succ n  = (m Main.* n) Main.+ m

(**) :: Nat -> Nat -> Nat
m ** Zero   = Succ Zero
m ** Succ n = (m Main.** n) Main.* m

すると、これは受け付けられたので、ちょっと計算してみよう。

Prelude> :l 3.1_2.hs
[1 of 1] Compiling Main             ( 3.1_2.hs, interpreted )
Ok, modules loaded: Main.
*Main> Zero Main.+ Zero
Zero
*Main> (Succ (Succ (Succ Zero))) Main.+ (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ Zero))))
*Main> (Succ (Succ (Succ Zero))) Main.* (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ (Succ Zero)))))
*Main> (Succ (Succ (Succ Zero))) Main.** (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))
*Main> 

それぞれ、 0+0, 3+2, 3*2, 3**2 を計算したものだ。
自然数の定義まで立ち戻って、つまり数論として書くとこんな感じになるわけだ。

ところで、今のHaskell(GHC)では、漢字も使えるとあった。
単に、中がUnicodeも通るようになっただけかも知れないのだが、利用できるものは利用してみよう。
ということで、Main.をつけて元からある演算と区別していたウザイ個所を、漢字の演算子に変えてみた。

data Nat = Zero | Succ Nat
     deriving (Eq,Ord,Show)

(+)  :: Nat -> Nat -> Nat
m + Zero    = m
m + Succ n  = Succ ( m + n )

(×)  :: Nat -> Nat -> Nat
m × Zero    = Zero
m × Succ n  = (m × n) + m

(↑) :: Nat -> Nat -> Nat
m ↑ Zero   = Succ Zero
m ↑ Succ n = (m ↑ n) × m

ずいぶんすっきりした。

*Main> :l 3.1_3.hs 
[1 of 1] Compiling Main             ( 3.1_3.hs, interpreted )
Ok, modules loaded: Main.
*Main> Zero + Zero
Zero
*Main> (Succ (Succ (Succ Zero))) + (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ Zero))))
*Main> (Succ (Succ (Succ Zero))) × (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ (Succ Zero)))))
*Main> (Succ (Succ (Succ Zero))) ↑ (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))
*Main> 

ということで、ちゃんと同じ結果が得られて、めでたしめでたし。