自然数にコード化するpair関数
書籍『C言語による計算の理論』固有の概念
自然数のペア
(x,y) をコード化する\mathrm{pair}(x,y)=(\sum^{x+y}_{n=0}n)+x+1
\mathbb{N}^2\to\mathbb{N}の全域関数
「任意の自然数のペア」と「正の自然数」を一対一に対応付けるのが特徴
hspair :: 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)を示せばいい
x+y\gt w+zとしたときも同様
よってx+y=w+z
よってfは単射
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は全射
よってfは全単射