前置き

この記事シリーズの目的は、

数学やプログラムを知ったかぶる著者が、『習うより慣れろ』の精神で、Haskellを使って計算論を学び、アウトプットしているうちに、いつの間にか計算論を理解しHaskell使いになっていることを目指す

ことで、
Haskellの実行環境構築や基本的な文法について詳細に解説すること、ではありません。

著者はHaskellや計算論のお勉強中なので、誤りなど、なんかよくないことを書いちゃっていたらご指摘いただけると幸いです。

今回の目的

Haskellで、シンプルな自然数の型を定義し、自然数の加算関数を帰納的に記述してみること。

自然数ざっくりメモ

自然数の定義

自然数を以下のように帰納的に定義します。

0は自然数である
nが自然数ならば、succ n は自然数である

ここで、succ n は n の次の自然数を表します。
つまり、succは、自然数を与えると自然数を返す関数です。
succはsuccessorの略で、英語で「後継」という意味です。

例えば、1 は succ 0 として定義します。
自然数は0から始まり、次々とsuccを適用していくことで、$1,2,3\cdots$という馴染み深い自然数を定義できます。

こう考えると自然数は

0
後継関数 succ

から構成されていると言ってよいのかな。
例えば、5 は

5 = succ 4
  = succ (succ 3)
  ・・・
  = succ (succ (succ (succ (succ 0))))

で、succ と 0 で表現し定義できます。

自然数の加算

日常で加算(足し算)って、 + を使いますよね。

例えば、
$2+1=3$
とか。

今回の目的で書いた通り、Haskellで足し算を表す関数を帰納的に定義してみます。
Haskellではもちろん「+」は用意されており、あまり意味ないかもしれませんが、帰納的定義に慣れることが目的です。
ちなみに、Haskellでは、数値型の値を引数にとる「succ」も用意されています。
ですが、今回Haskellで実装する加算関数では、自然数の型を自分で定義して自然数のみを対象としたいので、succは使いません。

加算を帰納的に定義してみる

$1 + 2 = 3$

って、 1 と 2 を「+」に与えることで 3 を得ているように見えるかもしれません。

もっと一般的に、

$x + y = z$

という式を考えると、「＋」は自然数の組 ( x , y ) を引数にとって、自然数 z を返す関数に見えるかもしれません。

+ (x,y) = z

のような感じで。
（こんな書き方しないと思いますが、例えです。）

ここでは、自然数の加算を「+」ではなくて、関数 myAdd を用いて次のように帰納的に定義することを考えてみます。

myAddの定義

x = 0 の場合

myAdd x y = y

それ以外の場合、ある自然数 x' を用いて、x = succ x' と書けて、

myAdd succ(x') y  = succ myAdd x' y

myAddは自身を再帰呼び出ししています。

また、myAddは自然数の組(x,y)を受け取っているというよりは、
まず、myAddがxを受け取り、次にyを受け取る、と考えます。(カリー化)
myAddはxを受け取り、「1つの自然数を引数として自然数を返す関数」を返すと言えばいいのかな。
(その返ってきた関数にyを与えることで、結果として自然数(つまり $x+y$ の結果)を得るイメージ。)

例えば、myAdd 2 1 を計算すると、

myAdd 2 1 = myAdd succ(1) 1
          = succ (myAdd 1 1)
          = succ (myAdd succ(0) 1)
          = succ (succ (myAdd 0 1))
          = succ (succ 1)
          = succ 2
          = 3

となり、 myadd 2 1 は、 $2+1=3$ と同じ結果になります。
$2+1=3$ と計算するとき無意識に行っていると思います。
計算の理屈としては、加算は後継関数 succ を繰り返し適用することで行っています。

HaskellでmyAddを実装

まず、Haskellで自然数の型を定義してみましょう。
型の名前をMyNaturalとでもしましょうか。

data MyNatural = Zero | Successor MyNatural deriving Show

これだけの簡単なモデルですけど、MyNatural型は、「Zero もしくは Succerssor MyNatural」のみとすることで、自然数の定義で述べたことを表現しようとしています。

ここで、ZeroはHaskellの数値型で出てくる「0」とは、今のところ全く関係がないことに注意してください。
Zeroと書くと「0」を連想しやすいかなー、と思ってそうしてます。
Successorは今まで述べてきたsuccのことだと思ってください。

myAddの定義を確認すると、myAddは次のように書けます。

myAdd :: MyNatural -> MyNatural -> MyNatural
myAdd Zero y = y
myAdd (Successor x) y = Successor (myAdd x y)

1 を Successor Zero
2 を Successor ( Successor Zero )
のことだと考えると、上で例としたmyAdd 2 1 は

myAdd (Successor ( Successor Zero )) ( Successor Zero )

と書けます。

確認のために、以下のようにコーディングして実行してみましょう。

main :: IO ()
main = do
  print $ myAdd (Successor (Successor Zero)) (Successor Zero)

data MyNatural = Zero | Successor MyNatural deriving Show

myAdd :: MyNatural -> MyNatural -> MyNatural
myAdd Zero y = y
myAdd (Successor x) y = Successor (myAdd x y)

結果は、

Successor (Successor (Successor Zero))

となってSuccessorが３つあるので、0の次の次の次、つまり3を表す値となりました。

今回は以上です。
最後までご覧いただきありがとうございました。
<(_ _)>

Haskellを使いながら計算論 【1】自作自然数型を定義し、加算関数をHaskellで帰納的に定義する

前置き