Haskellで自然数から整数を構成する - 置き去りになったメモ

こんにちは、やきつか(@sy_t_)です。
最近はとても暑いですね。僕は研究室の冷房強くしすぎてよくお腹を壊してるんですけど。

目次
はじめに
自然数ってなんぞや (ペアノの公理)
Haskellで自然数を実装する
自然数に二項演算を用意する
自然数が正しく動作していることを確認
整数ってなんぞや
Haskellで整数を実装する
整数に二項演算を用意する
整数が正しく動作していることを確認
まとめ

はじめに

さて、今回は、純粋関数型言語であるHaskellを使って自然数を実装して、その自然数から整数を構成する、ということをやります。いきなりコードを貼り付けるのもアレなんで、自然数と整数の簡単な説明を通してから実装していきます。「それぐらいわかるわボケ」って人はその単元は飛ばしてください。

自然数ってなんぞや (ペアノの公理)

自然数ってなんでしょうかね。人に説明する時は「1,2,3,...って続く数字のことだよ」とか「0以上の全ての整数だよ」とかって言うんですかね。僕もそう言うと思います、めんどくさいし。
しかし、数学は厳密な学問なので、しっかりした定義が欲しくなります。そこで、ペアノさんが、次のような性質(ペアノの公理)を満たすものを自然数と呼ぶことにしようと決めました。自然数全体の集合をℕと表すことにします。

$0∈ℕである0が存在する。$
$任意にa∈ℕをとっても、その後者suc(a)∈ℕが存在する。$
$異なる自然数は異なる後者を持つ。つまり、∀a,b∈ℕ[a≠b→suc(a)≠suc(b)]が常に成立する。$
$0はいかなる数の後者でもない。∀a∈ℕ[0≠suc(a)$ ]
$自然数を引数にとる命題Pがあり、P(0)が成立し、\\ P(a)が成立する時P(suc(a))が成立するならば任意の自然数xに対してP(x)が成立する。$

sucは後者関数と呼ばれる単射な写像で、"1を足す"ことに相当します。
ℕを外延的記法で書けば、 $ℕ=\{0,suc(0),suc(suc(0)),suc(suc(suc(0))),...\}$ という感じになります。
ここで、次のように各要素に名前をつけていきます。
$1 := suc(0) \\ 2 :=suc(suc(0)) \\ 3 := suc(suc(suc(0))) \\ \qquad \vdots$
このようにすると、我々がよくみる $ℕ=\{0,1,2,...\}$ になりますね！

Haskellで自然数を実装する

自然数の定義はある程度理解できた(とする)ので、Haskellで自然数を実装してみましょう!
Haskellで自然数を定義するには、次のように書けばいいです。

data N = Zero | Suc N deriving (Eq, Ord, Show)

この文は、=の左辺と右辺に分けて読みます。dataは代数的データ型とよばれる、列挙型・構造体・共用体のようなものを生成するキーワードです、Cのstructのような使い方ですね。
=は代入だと思う人もいそうですが、「=の左辺っていうのは=の右辺に書いてあるもののことやで」の意味です。
右辺にあるZeroはコンストラクタとか構築子と呼ばれるやつで、列挙型の要素に相当します。
次にある|の記号は、「もしくは」と読みます。Suc NのSucは構築子なのですが、Nはフィールドとよばれるもので、なんらかの値(ここではN自身)にSucを適用したものです。
全体としては、「代数的データ型Nは、Zeroもしくは自身にSucを適用したもののことを言うんだな、うんうん」ぐらいの感じです。
代数的データ型に関しては、Haskell データ型・型クラス・型族 | Netsphere Laboratoriesあたりを読むといいと思います。
つまり、NというのはZeroもしくはSuc ZeroもしくはSuc (Suc Zero)もしくは...と無限の値を持つ代数的データ型です。
これは、Zeroを0、Sucを後者関数だとすると自然数そのものだと考えることができます。
「derivingってなんや?Eq,Ord,Show?」となっている人がいると思います、これは「代数的データ型Nの値は値同士で同値(Eq)であることを確かめられるし、比較(Ord)することもできるし、画面上に表示(Show)することができるんやで!!」というぐらいの意味です。詳しくは型クラス - ウォークスルー Haskellあたりを読んで下さい。(言い訳: Haskellの文法を解説する目的ではないので...)

自然数に二項演算を用意する

さて、Haskellで自然数を実装することができたので、足し算とか掛け算のような二項演算を作りましょう。
足し算は次のように定義します。

(+.) :: N -> N -> N
Zero +. n = n
n +. Zero = n
n +. Suc m = Suc (n +. m)

これは、ペアノさんによる再帰的な加法の定義をそのままHaskellで書き下ろしただけです、これでちゃんと動きます。詳しくは加法 - Wikipediaを参考に。

同じ感じで、掛け算も実装していきます!

(*.) :: N -> N -> N
Zero *. _ = Zero
_ *. Zero = Zero
n *. Suc m = n +. (n *. m )

+とか*に.(ドット)が付いてるのはHaskellの標準関数として+と*が定義されてしまっているからです、許して。

自然数が正しく動作していることを確認

全体のソースコードとしてはこんな感じ。

--いい感じに自然数を定義する
data N = Zero | Suc N deriving (Eq, Ord, Show)

--足し算を定義
Zero +. n = n
n +. Zero = n
n +. Suc m = Suc (n +. m)

--掛け算を定義
Zero *. _ = Zero
_ *. Zero = Zero
n *. Suc m = n +. (n *. m )

ghciの対話形式で実行します。

同値性・順序性の確認

f:id:yakituka:20190813223917p:plain

足し算の確認

f:id:yakituka:20190813224549p:plain
Suc (Suc (Suc Zero))は3, Suc (Suc Zero)は2にあたるので、
Suc (Suc (Suc (Suc (Suc Zero))))が5=3+2という結果に一致していますね。

掛け算の確認

f:id:yakituka:20190813224815p:plain
3*3=9になっていることを確認してください。(疲れた)

整数ってなんぞや

Haskellで自然数は実装できたので、一旦話を戻して、整数を数学的にどうやって作るのか説明したいと思います。
まず、自然数全体 $ℕ$ の2つの直積
$ℕ×ℕ$
を考えます。この $ℕ×ℕ$ を次のような同値関係 $\sim$ で割ってあげます。これが整数です。
$∀(n,m),(n',m')∈ℕ×ℕ[(n,m)〜(n',m')⇔n+m'=m+n']$
$ℤ := ℕ×ℕ/\sim$
$ℤ$ の要素としては、 $\{(0,0),(1,1),(2,2)...\}$ や $\{(1,0),(2,1),(3,2),...\}$ 、 $\{(0,1),(1,2),(2,3),...\}$ などが考えられると思います。これらの要素としての集合を、商写像 $[]$ を用いて、 $ℤ=\{...,[(0,2)],[(0,1)],[(0,0)],[(1,0)],[(2,0)],...\}$ と表します。
さらに、 $[(n,0)]$ を $n$ 、 $[(0,n)]$ を $-n$ と置くと、僕たちのよく知る整数 $ℤ=\{\dots,-2,-1,0,1,2,\dots\}$ を垣間見ることができます!(何故このようにできるかは足し算や掛け算の実装でわかると思います。)

Haskellで整数を実装する

整数については理解できた(はず)なので、Haskellで実装していきましょう。といっても、そのまま書くだけなんですけど。
整数の元は2つの自然数全体の直積でした、これをHaskellで表現するには次のように書きます。

data Z = Z N N

「えっ、これだけ?」と思うかもしれません、これだけです。
「代数的データ型ZはNとNの2つの値を持つんだよ～」ぐらいのテンションです。(なげやり)
流石にこれだけでは、整数とは言えないので同値関係を定めておきます。これは、次のようにかけばOKです。

instance Eq Z where
    (Z n m) == (Z n' m') = n +. m' == m +. n'

「2つの自然数n,mを持つ整数と、2つの自然数n',m'を持つ整数が等しいとは、n+m'=m+n'が成立することである。」と読みます。
このように、ZをEq型クラスのインスタンスとして実装することで、いとも簡単に同値関係で割ることができます。やっぱりHaskellってすげぇよ。

整数を表示する時に、一意的に表示できるようにZをShow型クラスのインスタンスにします。

instance Show Z where
    show (Z n m) = show $ f (Z n m)
        where
            f :: Z -> Int
            f (Z Zero Zero) = 0
            f (Z Zero (Suc m')) = (-1) + f (Z Zero m')
            f (Z (Suc n') Zero) = 1 + f (Z n' Zero)
            f (Z (Suc n') (Suc m')) | n' >= m' = 1 + f (Z n' (Suc m'))
                                    | n' < m' = (-1) + f (Z (Suc n') m')

これによって、例えばZ (Suc Zero) (Zero)もZ (Suc (Suc Zero)) (Suc Zero)も両方とも1と表示されます。(負の数ももちろん表示できる。)

整数に二項演算を用意する

整数 $\mathbb{Z} = \mathbb{N}×\mathbb{N}/\sim$ において、足し算+は次のように定義されます。
$(+): \mathbb{Z}×\mathbb{Z} \to \mathbb{Z} \\ [(n,m)] + [(n',m')] \longmapsto [(n+n',m+m')]$

また、掛け算は次のように定義されます。
$(*): \mathbb{Z}×\mathbb{Z} \to \mathbb{Z} \\ [(n,m)] * [(n',m')] \longmapsto [(n*n'+m*m',n*m'+m*n')]$

なぜこのように定義すればうまくいくかは、実装のあと確認します。
Haskellで、上記の定義をそのまま書いてやります。

(Z n m) +.. (Z n' m') = Z (n +. n') (m +. m')
(Z n m) *.. (Z n' m') = Z ( (n *. n') +. (m *. m') ) ( (n *. m') +. (n' *. m) )

+や*に.(ドット)が2つ付いてるのは、標準関数と上で自然数に対する演算で定義しているからです。(Num型クラスのインスタンスとして実装すればよかったのですが、+と*以外別にいらなかったので、このようにしました。)

整数が正しく動作していることを確認

ソースコード全体はこんな感じになりました。

--いい感じに自然数を定義して、演算も準備しておく
data N = Zero | Suc N deriving (Eq, Ord, Show)

Zero +. n = n
n +. Zero = n
n +. Suc m = Suc (n +. m)

Zero *. _ = Zero
_ *. Zero = Zero
n *. Suc m = n +. (n *. m )

--整数はN×Nを適当な同値関係で割って構成する
data Z = Z N N
instance Eq Z where
    (Z n m) == (Z n' m') = n +. m' == m +. n'

instance Show Z where
    show (Z n m) = show $ f (Z n m)
        where
            f :: Z -> Int
            f (Z Zero Zero) = 0
            f (Z Zero (Suc m')) = (-1) + f (Z Zero m')
            f (Z (Suc n') Zero) = 1 + f (Z n' Zero)
            f (Z (Suc n') (Suc m')) | n' >= m' = 1 + f (Z n' (Suc m'))
                                    | n' < m' = (-1) + f (Z (Suc n') m')

(Z n m) +.. (Z n' m') = Z (n +. n') (m +. m')
(Z n m) *.. (Z n' m') = Z ( (n *. n') +. (m *. m') ) ( (n *. m') +. (n' *. m) )

それでは、確認していきます。

同値性の確認

f:id:yakituka:20190813233929p:plain

表示の一意性

f:id:yakituka:20190813234140p:plain

足し算

f:id:yakituka:20190813234345p:plain
2-3=-1や2+3=5がうまく計算できていますね。

掛け算

f:id:yakituka:20190813234609p:plain
2*3=6が計算できています。すごい。

あっ(-1)*(-1)ってどうなるんだろう

f:id:yakituka:20190813235300p:plain
ちゃんと1になってくれましたね、めでたしめでたし。

まとめ

今回は、Haskellの代数的データ型や型クラスの機能を用いて自然数や、自然数から整数を定義しました。
このように、Haskellは代数にめっぽう強く、とてもカッコいい言語なので、みなさんも使いましょう。
次は「Haskellで整数と自然数から有理数を構成する」みたいなのを書くと思います、多分。
もし、ここまで読んでいただいた人がいたら、ご清覧ありがとうございました。

目次