Haskell でラムダ式を簡約させてみる - 1

ラムダ式について勉強する機会があったのでメモ。

ラムダ計算について前々から興味はあったのだが、残念ながら日本語による良質な書籍を私は知らない。ので勉強した内容をまとめてみました。
ラムダ計算の名を冠した本に高橋正子先生の本がある。

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)

しかし合流性に関する議論が多く、例えばラムダ式で自然数を表現するとか、ラムダ式で足し算を実装するとか、ラムダ式で再帰式を記述する、というようなトピックは無い。
この記事では、ラムダ式を独自に定義した型で表現し、簡約（インタプリタによる実行）するエンジンを Haskell で実装する。

準備

ghc をインストールする。
https://www.haskell.org/ghc/download
current stable をクリックし、バイナリをダウンロードして適当なディレクトリに解凍、パスを通せば良い。
Windows の場合は DOS 窓で

C:\Users\hal>ghci
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
Prelude> 

となればインストールは成功である。
Cygwin でも使えないことはないが、矢印キーによる履歴の呼び出しやタブ補完が利かないので、Dos 窓で実行するほうが良い。

自然数の表現

Haskell で簡約エンジンを実装する前に、自然数についての簡単な例を挙げておく。
自然数にはれっきとした定義があり、古くは1900年代のペアノ、デーデキント等の著書にその定義が見受けられる。ペアノによる著書では、自然数の公理として5つが挙げられており、そのうちの2つを引用すると：

• ゼロは自然数である。( = Z とする )
• ある自然数の、次の数 が存在する。( = 次の数を表す関数 successor を S とする )

アラビア数字とペアノの定義による自然数は、以下のように対応可能である：

0 : Z
1 : S(Z)
2 : S(S(Z))
3 : S(S(S(Z)))
...

これを Haskell で実装してみる。まず、自然数 N の定義は以下となる：

Prelude> data N = Z | S N deriving Show

この式は、
自然数 N とは、「ゼロである(=Z)」または「自然数 N の次の数( = S )である」
という意味である。
S N という記述に注目すると、これはデータが再帰的になっていることを示す。
この型 N を定義すると、以下のように上で挙げたペアノの定義による自然数を表現可能となる。

Prelude> Z
Z
Prelude> S(Z)
S Z
Prelude> S(S(Z))
S (S Z)
Prelude> S(S(S(Z)))
S (S (S Z))

足し算

これからは、peano.hs というファイルに Haskell のプログラムを書いて実行してみる。
ghc を

Prelude> :quit
Leaving GHCi.

で抜け、適当なエディタで peano.hs を作る。

peano.hs :

data N = Z | S N deriving Show

add Z     y = y
add (S x) y = S (add x y)

この定義はデーデキントの著作より拝借した。

数とは何かそして何であるべきか (ちくま学芸文庫)

最初の式は、ゼロに y を足しても、答えは y であることを定義している。
（定義というか、置き換え可能、と考えたほうが分かりやすいかも）
次の式はゼロ以外の数字を y を足した定義である。
例として、2 + 1 を考える。
2 = S (S Z)
1 = S Z
であるので、2 + 1 は以下のように置き換え可能である：

  add (S (S Z)) (S Z)
= S ( add (S Z) (S Z))
= S ( S ( add Z (S Z)))
= S ( S ( S Z ) )

答えは S (S (S Z)) つまり 3 である。

Haskell で実行してみる。
DOS 窓からファイルを指定して ghci を起動する。

C:\Users\hal>ghci -i peano.hs

実際に足し算させてみると、

> add (S (S Z)) (S Z)
S (S (S Z))
> add (Z) (S Z)
S Z
> add (S Z) (S(S Z))
S (S (S Z))
> add (S(S Z)) Z
S (S Z)

ちゃんと計算されている。

後々の記事では、λ式で自然数を表現し、足し算や引き算等を実装する予定である。