[002T] 自然数

今までに導入した型だけでは何も面白い数学はできない。数学を面白くするには自然数の概念は必須であろう。自然数の型は帰納的型の例として定義される。

-自然数型(type of natural numbers) $\mathbb {N}:\mathcal {U}(0)$ を構成できる。 $\mathbb {N}$ の要素を自然数(natural number)と呼ぶ。
-要素 $0:\mathbb {N}$ を構成できる。
-要素 $n:\mathbb {N}$ に対して、要素 $\mathord {\textnormal {\textsf {succ}}}(n):\mathbb {N}$ を構成できる。
- $n:\mathbb {N}$ を要素、 $$i$$ を階数、 $A:\mathbb {N}\to \mathcal {U}(i)$ を型の族、 $$a:A(0)$$ を要素、 $f:\prod _{\lbrace x:\mathbb {N}\rbrace }A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))$ を関数とすると、要素 $\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(n,A,a,f):A(n)$ を構成できる。
- $$i$$ を階数、 $A:\mathbb {N}\to \mathcal {U}(i)$ を型の族、 $$a:A(0)$$ を要素、 $f:\prod _{\lbrace x:\mathbb {N}\rbrace }A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))$ を関数とすると、 $\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(0,A,a,f)\equiv a$ と定義される。
- $n:\mathbb {N}$ を要素、 $$i$$ を階数、 $A:\mathbb {N}\to \mathcal {U}(i)$ を型の族、 $$a:A(0)$$ を要素、 $f:\prod _{\lbrace x:\mathbb {N}\rbrace }A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))$ を関数とすると、 $\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(\mathord {\textnormal {\textsf {succ}}}(n),A,a,f)\equiv f(\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(n,A,a,f))$ と定義される。

一般に帰納的型はいくつかの構成子(constructor)によって定められる。 $\mathbb {N}$ の場合、 $$0$$ と $\mathord {\textnormal {\textsf {succ}}}$ が構成子である。これらは $\mathbb {N}$ の要素を構成する方法を与える。任意の $\mathbb {N}$ の要素がこれらの構成子のみを使って構成されることを表すために、帰納法原理(induction principle)を規則として認める。 $\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}$ に関する規則は、自然数 $$n$$ を使ってなんらかを構成するには、 $$0$$ の場合の構成( $$a:A(0)$$ )と $\mathord {\textnormal {\textsf {succ}}}(x)$ の場合の構成( $f:\prod _{\lbrace x:\mathbb {N}\rbrace }A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))$ )を与えれば十分であることを意味する。つまり、型理論の中の人にとっては自然数とは $$0$$ と $\mathord {\textnormal {\textsf {succ}}}$ のみを使って構成されたものである。さらに、 $\mathord {\textnormal {\textsf {succ}}}$ の場合の構成においては、 $$x$$ の場合の構成( $$f$$ の引数 $$y:A(x)$$ )は既に定義されたと仮定してよい。これは再帰的定義(recursive definition)を可能にする。

自然数型からの関数を定義するにはパターンマッチが便利である。

[008E] 記法

$\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}$ を使って関数を定義するには次のいずれかのような言い回しをする。

-関数 $h:\prod _{x:\mathbb {N}}A(x)$ を $\lambda x.\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(x,A,a,f)$ と定義する。
-関数 $h:\prod _{x:\mathbb {N}}A(x)$ を $h(0)\equiv a$ と $h(\mathord {\textnormal {\textsf {succ}}}(x))\equiv f(h(x))$ で定義する。
- $x:\mathbb {N}$ を要素とする。要素 $$h(x):A(x)$$ を $h(0)\equiv a$ と $h(\mathord {\textnormal {\textsf {succ}}}(x))\equiv f(h(x))$ で定義する。

現実では多変数の関数の引数の一つにパターンマッチを使う場合がある。自然数のパターンマッチの $\mathord {\textnormal {\textsf {succ}}}$ の場合 $h(\mathord {\textnormal {\textsf {succ}}}(x))\equiv f(h(x))$ では右辺に $$h(x)$$ のパターンを見出すのに慣れが要ることもある。

[002W] 例

$n_{1},n_{2}:\mathbb {N}$ を要素とする。要素 $\mathord {\textnormal {\textsf {plus}}}(n_{1},n_{2}):\mathbb {N}$ を構成する。自然数の帰納法を使い、 $\mathord {\textnormal {\textsf {plus}}}(0,n_{2})\equiv n_{2}$ と $\mathord {\textnormal {\textsf {plus}}}(\mathord {\textnormal {\textsf {succ}}}(n_{1}),n_{2})\equiv \mathord {\textnormal {\textsf {succ}}}(\mathord {\textnormal {\textsf {plus}}}(n_{1},n_{2}))$ と定義する。形式的には $\mathord {\textnormal {\textsf {plus}}}(n_{1},n_{2})\equiv \mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(n_{1},\lambda x.\mathbb {N},n_{2},\lambda (x,y).\mathord {\textnormal {\textsf {succ}}}(y))$ と定義できる。

[002X] 例

$n:\mathbb {N}$ を要素、 $f:\mathbb {N}\to \mathbb {N}\to \mathbb {N}$ を関数とする。原始再帰(primitive recursion)による関数 $\mathord {\textnormal {\textsf {prim-rec}}}(n,f):\mathbb {N}\to \mathbb {N}$ が $\mathord {\textnormal {\textsf {prim-rec}}}(n,f,0)\equiv n$ と $\mathord {\textnormal {\textsf {prim-rec}}}(n,f,\mathord {\textnormal {\textsf {succ}}}(m))\equiv f(m,\mathord {\textnormal {\textsf {prim-rec}}}(n,f,m))$ で定義される。形式的には $\mathord {\textnormal {\textsf {prim-rec}}}(n,f)\equiv \lambda m.\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(m,\lambda x.\mathbb {N},n,\lambda (x,y).f(x,y))$ である。よって、いわゆる原始再帰的関数はすべて構成できる。

[002Y] 演習

Ackermann関数は二変数の関数 $\mathord {\textnormal {\textsf {ack}}}:\mathbb {N}\to \mathbb {N}\to \mathbb {N}$ で、次のように定義される。

- $\mathord {\textnormal {\textsf {ack}}}(0,n)\equiv \mathord {\textnormal {\textsf {succ}}}(n)$
- $\mathord {\textnormal {\textsf {ack}}}(\mathord {\textnormal {\textsf {succ}}}(m),0)\equiv \mathord {\textnormal {\textsf {ack}}}(m,\mathord {\textnormal {\textsf {succ}}}(0))$
- $\mathord {\textnormal {\textsf {ack}}}(\mathord {\textnormal {\textsf {succ}}}(m),\mathord {\textnormal {\textsf {succ}}}(n))\equiv \mathord {\textnormal {\textsf {ack}}}(m,\mathord {\textnormal {\textsf {ack}}}(\mathord {\textnormal {\textsf {succ}}}(m),n))$

Ackermann関数の構成を[002V]に基づいて正当化せよ。ちなみに、Ackermann関数は原始再帰的でないことが知られているので、[002X]の特別な場合としては定義できない。関数型を使えることに注意するとよい。