1. Home
  2. 技術者ブログ
  3. Haskellで自然数を定義してみる

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>

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

< 前の記事へ 次の記事へ >

＃人気の記事

＃タグ

＃アーカイブ