ウォンツテック

そでやまのーと

x \div yが原始的関数である事を示すのに以下の補題が必要なんだけどその証明が4行しかなくて一読しただけでは分からなかったので論理的に細かく追ってみた。

前提
真偽の定まる関数pを述語と呼ぶ。
述語pに対してC_pを特徴関数とよび、その定義は
述語pが真の時0、偽の時1となる関数である。

補題 1.3.12

述語  p:N^{n+1} \to \left\{ \text{true, false}\right\}
が原始的ならば、
\mu_{z < y}p(\vec{x},z):N^{n+1} \to N
は原始的関数である。
ただし、\mu_{z < y}p(\vec{x},z) = min(\left\{ z \in N \mid z < y \wedge p(\vec{x},z)\right\}) \cup \left\{ y \right\})
証明
p(\vec{x},z)の特徴関数をC_p(\vec{x},z)とすると
(\exists z \leq v)p(\vec{x},z)
の特徴関数は
\prod_{z \leq v}C_p(\vec{x},z)
となる。
何故ならばz \leq vなるzが存在する時、特徴関数C_pは0となるが、
存在しなければ1である。
すなわちz \leq vを満たすz全てにおいて
C_pを満たすzが存在しなければ1、
一つでも存在すれば0なのでその特徴関数は上記のように置ける。
ここで
\prod_{z \leq v}C_p(\vec{x},z)g(\vec{x},v)とおく。
\vec{x}を固定したときg(\vec{x},v)の値は、
はじめてp(\vec{x},v) = trueとなるv以後は0、
それ以外は1である。
その値を特別にz_0とすると
g(\vec{x},1) + g(\vec{x},2) + \cdots g(\vec{x},z_0)
この式の各項は全て1なのでその和はz_0となる。
また
g(\vec{x},z_0+1) + \cdots + g(\vec{x}, y-1)
は各項全て0であるので和も0である。
以上より
g(\vec{x},1) + \cdots g(\vec{x},y-1) = \sum_{v < y}g(\vec{x},v) = z_0
となる。
ところでz_0p(\vec{x},v)が真となる境界値なので
\mu_{z < y}p(\vec{x},z) = min(\left\{ z \in N \mid z < y \wedge p(\vec{x},z)\right\}) \cup \left\{ y \right\}
その物である。ただし、p(\vec{x},v)が真とならない場合は
g(\vec{x},v)は全て1なのでそのv < yに関する和はyその物である。
以上より、
\mu_{z < y}p(\vec{x},z) =  \sum_{v < y}g(\vec{x},v)
と表す事ができ、原始的述語の特徴関数が原始的関数である事と、
以前の補題によりその積、和が原始的関数である事により命題の関数は
原始的関数である。

ここまで細かく論理の飛躍を追ってようやく理解出来た。数学の本ってのはえてして飛躍が多すぎるんだよなぁ。

さて、ここで

 x \div y = \mu_{z < x}(x < y \times (z+1))
とおけるんだけど、何でおけるかっていうと
z > x \div y -1
を満たす最小のzx \div yだから。

これよりx \div yも原始的関数である事がわかったよ。
x+y, x-y, x \times yが原始的関数である事は既に証明されてるので四則演算が原始的関数である事が証明され模様。
そんで原始的関数はNプログラムという抽象化されたプログラムで計算出来る事が証明される。
この後に有名なAckermann関数という関数が原始的関数でない事が証明されるのでこれはまずいという事でそれを拡張した帰納的関数が登場。