ウォンツテック

そでやまのーと

帰納的関数の主要定理は大体理解したので一つ問題を解いてみる。

問題 1.4.9

問題
述語 p:N^{n+1} \to \lbrace true, false \rbrace の特徴関数 c_p:N^{n+1} \to N帰納的関数のときpを帰納的述語という。
帰納的述語の最小関数 \mu_y(p(\vec{x}, y)) は
(定義域が\lbrace\vec{x}|\exist y(p(\vec{x}, y)\rbrace)の帰納的関数である事を示せ。
証明
帰納的述語の最小解関数 \mu_y(p(\vec{x}, y)) に最小値が存在するとしその値を y_0とする。
特徴関数の定義により \vec{x}を固定したとき、
y_0 未満の y について特徴関数 c_p(\vec{x}, y) の値は1であり
 y_0 以上の y での値は0である。
よって
c_p(\vec{x}, 0) + c_p(\vec{x}, 1) \cdots c_p(\vec{x}, y_0 - 1) = \overbrace{1 + 1 + \cdots + 1}^{y_0} = y_0
となるので
\mu_y(p(\vec{x}, y)) = \sum_y c_p(\vec{x}, y)
と表せる。
ところで、仮定より c_p(\vec{x}, y)帰納的関数であるのでKleeneの標準形定理により 
適当な原始的関数fと原始的述語p^{\prime}を使って
c_p(\vec{x}, y) = f(\vec{x}, \mu_y(p^{\prime}(\vec{x}, y)))
と表す事が出来る。
※pp^{\prime}は別の述語である。
すなわち
\mu_y(p(\vec{x}, y)) = \sum_y f(\vec{x}, \mu_y(p^{\prime}(\vec{x}, y)))
となり、右辺は原始的述語p^{\prime}の最小解関数と原始的関数の合成関数の和で表され、
これは帰納的関数の定義により帰納的関数である。
また、定義域はp(\vec{x}, y)が真となるyが存在する領域なので \lbrace \vec{x}|\exist y(p(\vec{x}, y)) \rbraceとなる。