自然数にコード化するpair関数

自然数のペア(x,y)をコード化する

$ \mathrm{pair}(x,y)=(\sum^{x+y}_{n=0}n)+x+1

$ \mathbb{N}^2\to\mathbb{N}の全域関数

「任意の自然数のペア」と「正の自然数」を一対一に対応付けるのが特徴

code:hs

pair :: Int -> Int -> Int

pair x y = sum 0..x+y + x + 1

便利関数を用意しておく

left, rightはpairの逆の変換をしてその片方を返す

hoge z = (left, right)のイメージ

$ \mathbb{N}\to\mathbb{N}^2であり、そのタプルの片方を返す

$ \mathrm{left}(\mathrm{pair}(x,y))=x

$ \mathrm{right}(\mathrm{pair}(x,y))=y

重要なのは、left, right,pairは計算可能である、ということ

ジャンププログラムで記述できる

leftやrightは、プログラム内部でで引数zの二重ループを行う

つまり最悪でも$ z\times z回のループで得られる

leftは元の数列に対するhead

rightは元の数列に対するtail

$ \mathrm{pair}(x,y)=(\sum^{x+y}_{n=0}n)+x+1が全単射になることを証明する ref

やりづらいので$ f(x,y)=\frac{1}{2}(x+y)(x+y-1)+x+1という関数$ fを考える

$ fが単射であることを示す

$ x,y,w,z\in\mathbb{N}に対して、$ f(x,y)=f(w,z)\Rightarrow(x,y)=(w,z)を示せばいい

https://gyazo.com/9f50d09ae09694d5c1dacd6c2e60f770

https://gyazo.com/8b0d8c7ad32461be2e00e5004194fcf8

$ x+y\gt w+zとしたときも同様

よって$ x+y=w+z

よって$ fは単射

https://gyazo.com/eb48456eec1f0c3a1d4db66ce132bdfb

https://gyazo.com/8f37f5f9cf7c600751e909ee1c13c735

https://gyazo.com/5a9da08dcc6f5d7b79dd1e703aceea69

$ fが全射であることを示す

$ \forall n\in \mathbb{N}に対して、$ \frac{k(k-1)}{2}\le n\le\frac{(k+1)k}{2}+1(①とする)を満たす$ k\in\mathbb{N}を取ると

$ n=\frac{k(k-1)}{2}+m+1と書ける

ここで$ m=n-\frac{k(k-1)}{2}-1\le \frac{(k+1)k}{2}+1-\frac{k(k-1)}{2}-1=k

①より。

よって$ m\le k

$ m=n-\frac{k(k-1)}{2}-1\ge0でもあるので、$ 0\le m\le k

よって$ x=m, y=k-m \in \mathbb{N}ととると

$ n=\frac{k(k-1)}{2}+m+1=\frac{1}{2}(x+y)(x+y-1)+x+1となる

つまり任意の$ n\in\mathbb{N}にたいして、$ f(x,y)=nを満たす$ x,y\in\mathbb{N}が存在する

よって、$ fは全射

https://gyazo.com/20330e326ccdd23c2be711101b548bf1

よって$ fは全単射