はじめに
ペアノの公理は自然数の定義する公理ですが、自然数上の多くの関数は再帰関数または漸化式を用いて定義されていたりします。
そこで本記事ではペアノの公理から再帰呼び出し関数、特に多くの関数型言語や証明支援系において関数定義として使えるFixpoint関数が定義できることを証明していきます。
まずはペアノの公理を見ていきましょう。
ペアノの公理
以下の公理を満たす集合$N$を自然数全体の集合と呼び、その要素を自然数と呼ぶ。
- $0 \in N$が存在する
- 関数$S : N \to N$が存在する
- [単射性]$S$は単射
- [一意性]任意の$n \in N$に対し、$S\,n \neq 0$
- [帰納原理]任意の$P: N \to 2$つまり$P \in 2^N$に対し、$P\,0$かつ、(任意の$n \in N$に対し$P\,n$ならば$P\,(S\,n)$)を満たすとき、任意の$n \in N$に対し$P\,n$
ここでポイントになるのは最後の帰納原理です。
これよりペアノの公理を満たす集合はFixpoint関数つまり関数の再帰的な定義ができることを示します。
ペアノの公理からFixpoint関数の存在性を示す
ペアノの公理を満たす集合$(N,0,S)$に対し、以下を満たす$F:\forall A, A \to (A \to N \to A) \to N \to A$すなわちFixpoint関数が存在することを示します。
Fixpoint関数の性質
・任意の集合$A$, $x_0 \in A$, $f_S:A \to N \to A$に対し、以下を満たす。
F\,x_0\,f_S\,0 = x_0
\forall n \in N, F\,x_0\,f_S\,(S\,n) = f_S\,(F\,x_0\,f_S\,n)\,n
分かりづらいので、関数$f := F\,x_0\,f_S : N \to A$と置くことにします。
すると上の性質は以下のように書き表せます。
f\,0 = x_0
\forall n \in N, f\,(S\,n) = f_S\,(f\,n)\,n
この時$f$はFixpoint関数で定義される関数を表していて
$f\,n$は
$n=0$のとき、初期値$x_0$を返し、
$n=S\,n'$のとき、再帰呼び出しした値$f\,n'\in A$と引数$n' \in N$の値から$f_S : A \to N \to A$を用いて返り値が作れることを表しています。
つまり$f\,n$は$n=0$の時の初期値$x_0$と、$n=S\,n'$の時の値を再帰呼び出しを行なって得られる値$f\,n'$と$n'$から関数$f_S$を用いて作られる値によって定義できる関数だということです。
実はこの関数の定義や性質は数学的帰納法から示すことができます。
Fixpoint関数の存在性
まず、任意の集合$A$, $x_0 \in A$, $f_S:A \to N \to A$つまりFixpoint関数の引数に対し、以下を満たす関係$R:N \to A \to 2$を考えます。
R\,0\,x_0
\forall n \in N,\forall a \in A, R\,n\,a \to R\,(S\,n)\,(f_S\,a\,n)
この関係$R$の意味するところは、関数$f := F\,x_0\,f_S$の引数と返り値の関係です。
これを満たす$R$は存在し、実際に全関係、すなわち任意の$n \in N$と$a \in A$に対し、$R\,n\,a$が成り立つ時、上の性質を満たします。
つまり、これを満たす最小の関係$R_\min$
R_\min\,n\,a := \forall R \in \{R : N \to A \to 2 \mid R\,0\,x_0 \wedge \forall n \in N,\forall a \in A, R\,n\,a \to R\,(S\,n)\,(f_S\,a\,n)\},
R\,n\,a
が存在することが分かります。
ちなみに$R_\min$自身も上の性質が成り立つこと、つまり
R_\min \in \{R : N \to A \to 2 \mid R\,0\,x_0 \wedge \forall n \in N,\forall a \in A, R\,n\,a \to R\,(S\,n)\,(f_S\,a\,n)\}
であることも簡単に示せます。そこでこの$R_\min$が関数的関係、すなわち任意の$n \in N$に対し、$R_\min\,n\,a$を満たす$a \in A$が一意に存在することを示します。
ここで$N$の帰納原理を使うので、ペアノの公理の帰納原理を再掲します。
- [帰納原理]任意の$P: N \to 2$つまり$P \in 2^N$に対し、$P\,0$かつ、(任意の$n \in N$に対し$P\,n$ならば$P\,(S\,n)$)を満たすとき、任意の$n \in N$に対し$P\,n$
存在性
ここで$P\,n := \exists a\in A, R_\min\,n\,a$と定義して帰納原理を使います。
$n=0$のときは$R\,0\,x_0$が成り立つので$a:=x_0$とおけば$P\,0$が成り立つことがわかる。
$n=S\,n'$のとき、帰納法の仮定より$R_\min\,n'\,x$となる$x \in A$が存在する。そこで$R_\min$の性質により$R_\min\,(S\,n')\,(f_S\,x\,n')$が成り立つので$a := f_S\,x\,n'$とおけばいい。
以上から任意の$n \in N$に対して$R_\min\,n\,a$となる$a \in A$の存在性を示せます。
一意性
次に任意の$n \in N$に対し、$R_\min\,n\,a$となる$a \in A$が一意に定まることを帰納原理を使って示します。
$n=0$の時、$R:N \to A \to 2$を以下に定義する。
R\,n\,a := R_\min\,n\,a \wedge (n \neq 0 \vee a = x_0)
このとき
R \in \{R : N \to A \to 2 \mid R\,0\,x_0 \wedge \forall n \in N,\forall a \in A, R\,n\,a \to R\,(S\,n)\,(f_S\,a\,n)\}
であることが分かる。
$R_\min$の定義より任意の$n \in N$と$a \in A$に対し、$R_\min\,n\,a \to R\,n\,a$が成り立つ。
定義より$R\,0\,a$となるのは$a = x_0$の時だけなので$R_\min\,0\,a$を満たす$a \in A$は$a = x_0$のときだけである。
$n=S\,n'$のとき、帰納法の仮定より$R_\min\,n'\,x$となる$x \in A$が一意に定まる。
そこで、$R:N \to A \to 2$を以下に定義する。
R\,m\,a := R_\min\,m\,a \wedge (m \neq S\,n' \vee a = f_S\,x\,n')
この時、
R \in \{R : N \to A \to 2 \mid R\,0\,x_0 \wedge \forall n \in N,\forall a \in A, R\,n\,a \to R\,(S\,n)\,(f_S\,a\,n)\}
を示す。
$R\,0\,x_0$は明らか。
任意の$m \in N$と$a \in A$に対し、$R\,m\,a$とする。この時$R\,(S\,m)\,(f_S\,a\,m)$を示す。
$m \neq n'$の時は$R_\min$の性質から明らか。
$m = n'$の時、$R_\min\,n'\,a$と帰納法の仮定より$a = x$が成り立ち、
$R_\min$の性質から$R_\min\,(S\,m)\,(f_S\,a\,m)$が言えるが$m = n'$と$a = x$から$R\,(S\,m)\,(f_S\,a\,m)$が言える。
すなわち$R \in \{R : N \to A \to 2 \mid R\,0\,x_0 \wedge \forall n \in N,\forall a \in A, R\,n\,a \to R\,(S\,n)\,(f_S\,a\,n)\}$を満たす。
このことから$R_\min$の定義より
任意の$n \in N$と$a \in A$に対し、$R_\min\,n\,a \to R\,n\,a$が成り立つので、特に$R_\min\,(S\,n')\,a$ならば$R\,(S\,n')\,a$が言える。
この時、$R$の定義より$a = f_S\,x\,n'$が言えるので$n = S\,n'$の時の$R_\min\,n\,a$を満たす$a \in A$の一意性が言える。
以上から、任意の$n \in N$に対して$R_\min\,n\,a$を満たす$a \in A$の一意性が成り立つ。
Fixpoint関数の存在性
上の２つの性質より、$R_\min$は関数的関係なので、選択公理より以下を満たす$f : N \to A$が存在する。
\forall n \in N, R_\min\,n\,(f\,n)
実際に、任意の$n \in N$に対し$R_\min\,n := \{a \in A \mid R_\min\,n\,a\}$は空でないので、選択公理より以下を満たす$f' : N \to \bigcup_{n \in N} R_\min\,n$が存在する。
\forall n \in N, f'\,n \in R_\min\,n
今、$\bigcup_{n \in N} R_\min\,n \subset A$であり、自然な単射$\operatorname{id} : \bigcup_{n \in N} R_\min\,n \to A$を用いて
$f := id \circ f' : N \to A$と定義すればいい。
この関数$f$は任意の$n \in N$に対して$R_\min\,n\,(f\,n)$を満たすので、$R_\min$の一意性から最初に欲しかった以下の性質を満たすことが示せる。
f\,0 = x_0
\forall n \in N, f\,(S\,n) = f_S\,(f\,n)\,n
実際に$R_\min\,0\,x_0$と$R_\min\,0\,(f\,0)$より$R_\min\,0$の一意性から$f\,0=x_0$であり
任意の$n \in N$に対し$R_\min\,n(f\,n)$が成り立つことから$R_\min\,(S\,n)\,(f_S\,(f\,n)\,n)$がいえて、$R_\min\,(S\,n)\,(f\,(S\,n))$と$R_\min\,(S\,n)$の一意性から$f\,(S\,n) = f_S\,(f\,n)\,n$が言える。
あとはここからFixpoint関数$F$を定義するだけです。
気持ちとしては$F\,x_0\,f_S := f$と定義したいのですが、正確に定義するには選択公理を使って以下のように存在性を示します。
具体的には、任意の$A$と$x_0 \in A$、$f_S : A \to N \to A$に対して上記の性質を満たす$f$の存在性が言えるので、特に任意の$x_0 \in A$, $f_S : A \to N \to A$に対して以下の集合は空ではないです。
\{f : N \to A \mid f\,0 = x_0 \wedge \forall n \in N, f\,(S\,n) = f_S\,(f\,n)\,n\}
よって選択公理によって、以下を満たす関数$F':A * (A \to N \to A) \to \bigcup_{(x_0,f_S) \in A * (A \to N \to A)} \{f : N \to A \mid f\,0 = x_0 \wedge \forall n \in N, f\,(S\,n) = f_S\,(f\,n)\,n\}$が存在します。
F'\,(x_0,f_S) \in \{f : N \to A \mid f\,0 = x_0 \wedge \forall n \in N, f\,(S\,n) = f_S\,(f\,n)\,n\}
この$F'$をCurry化して、以下の自然な単射$\operatorname{id}$を使ってFixpoint関数$F:\forall A, A \to (A \to N \to A) \to N \to A$が定義できる。
\operatorname{id}:\bigcup_{(x_0,f_S) \in A * (A \to N \to A)} \{f : N \to A \mid f\,0 = x_0 \wedge \forall n \in N, f\,(S\,n) = f_S\,(f\,n)\,n\} \to N \to A
F\,x_0\,f_S := \operatorname{id}\,(F'\,(x_0,f_S))
この時、関数$F$はFixpoint関数になる。
Fixpoint関数の一意性
$N$の帰納原理を使えば簡単に示せます。
もし$f,g:N \to A$が共にFixpoint関数の性質を満たしたとすると
$n=0$の時は$f\,0 = g\,0 = x_0$を満たし
$n=S\,n'$のとき、帰納法の仮定より$f\,n' = g\,n'$であるため
$f\,(S\,n') = f_S\,(f\,n') = f_S\,(g\,n') = g\,(S\,n')$を満たす。
すなわち、任意の$n \in N$に対し、$f\,n= g\,n$が成り立つ。
まとめ
ペアノの公理から自然数上の関数の再帰的な定義ができることを示しました。