Haskellでラムダ計算：算術編１

Haskellで算術のラムダ計算を行いますが、今回はRojas2015 A Tutorial Introduction to the Lambda Calculus を参考にします。

自然数の定義

自然数は以下のように定義します。
$\textbf{0}\equiv \lambda s z.s$
$\textbf{1}\equiv \lambda s z.s(z)$
$\textbf{2}\equiv \lambda s z.s(s(z))$
$\textbf{3}\equiv \lambda s z.s(s(s(z)))$

関数$\textbf{3}$を変数$f$と$a$に適用すると、
$$\textbf{3}f a \rightarrow (\lambda s z.s(s(sｚ)))f a\rightarrow f(f(fa))$$

これを見るとプログラミング言語のFOR i=1 TO 3を表していて、３回繰り返しの抽象的な形式になっている。我々は自然数を何か物のように考えているが、ラムダ形式や関数型プログラミングの世界では、何らかの操作を$n$回繰り返すという風に抽象化されていて、面白い。
ゼロ回の場合は、$\textbf{0}f a \equiv(\lambda s z.s)fa\rightarrow a$と記述され、これは何もしなかったことになっています。つまり、無（ない）のではなく、操作しなかった（動詞）という意味です。物（名詞）的表現ではなく、操作（動詞）的表現になっている。これはまるで哲学のようです。
インドの哲学で有とか無とか言うけれども、これはむしろ、無為や有為と解釈する方がよいのかもしれません。老子の思想に近いのかもしれないです。３回為すことを老子的に言うと、"為為為"とかなるのでしょうか。

Haskellで書けば、以下の通り：$f a$は値が必要なので、とりあえず、add1 0を入れて評価しました。

zero s z = z
one s z = s(z)
two s z = s(s(z))
three s z = s(s(s(z)))
add1 n = n + 1

main = do print $ three add1 0
ghci> mian
3

successor関数S

successor関数を定義します。
$$\textbf{S}\equiv\lambda n a b.a(nab)$$

$\textbf{S}$に$\textbf{0}$を適用すると、

$\textbf{S}\textbf{0}
\equiv(\lambda n a b.a(nab))\textbf{0}
\rightarrow\lambda a b.a(\textbf{0}ab)
\rightarrow\lambda a b.a((\lambda sz.z)ab)
\rightarrow\lambda a b.a(b)\equiv\textbf{1}$
$\textbf{S}\textbf{1}
\equiv(\lambda n a b.a(nab))\textbf{1}
\rightarrow\lambda a b.a(\textbf{1}ab)
\rightarrow\lambda a b.a((\lambda sz.s(z))ab)$
$\rightarrow\lambda a b.a(a(b))\equiv\textbf{2}$
$\textbf{S}\textbf{2}
\equiv(\lambda n a b.a(nab))\textbf{2}
\rightarrow\lambda a b.a(\textbf{2}ab)
\rightarrow\lambda a b.a((\lambda sz.s(s(z)))ab)$
$\rightarrow\lambda a b.a(a(a(b)))\equiv\textbf{3}$

zero s z = z
one s z = s(z)
two s z = s(s(z))
three s z = s(s(s(z)))

succ' n a b = a (n a b)
add1 n = n + 1

main = do
    print $ succ' zero add1 0
    print $ succ' one add1 0
    print $ succ' two add1 0
ghci> main
1
2
3

succは既に定義されているので、succ'と名前を変えました。

加算

加算については、例えば$2+3$は以下のように記述できます。

$$2\textbf{S}3\equiv(\lambda s z.s(s(z)))\textbf{S}\textbf{3}\rightarrow\textbf{S}(\textbf{S}\textbf{3})\rightarrow\textbf{S}\textbf{4}\rightarrow\textbf{5}$$

一般に、$m+n$は$m\textbf{S}n$となります。こんな風に加算を定義できるのは面白いですね。

main = do
    print $ two succ' three add1 0
ghci> main
5

コードは下記のところ：