再帰的部分関数、帰納的部分関数、部分帰納関数などと揺れる

帰納的関数の部分関数版

「計算可能な関数」と同値になる(後述)

簡潔な定義

原始帰納的関数から、

合成、原始帰納、最小化

の組み合わせで得られるものが帰納的部分関数

定義

①3つの原始帰納的関数は全て帰納的部分関数である

②帰納的部分関数から、関数合成で得られるものは帰納的部分関数である

合成は部分関数の合成による

③帰納的部分関数から原始帰納で得られるものは帰納的部分関数である

関数定義の「=」は、部分関数の記法のものによる

④帰納的部分関数から、最小化で得られるものは帰納的部分関数である

上の4条件で得られるもののみを部分帰納的関数という

定義の④の揺れについて ref pp.101-103

定義の④を示す際に文献によって、多少表記の差があることについての説明

結論としては、表現は違うがどれも同じものを指している

以下のようなレパートリーがある

④-1: gが帰納的部分関数ならば、

f(\vec{x})=\mu y[(g(\vec{x}, y)=0) \wedge(\forall z<y)(g(\vec{x}, z) \downarrow)]

というfは部分帰納的関数である

これは上の定義の④を丁寧に書いたもの

④-2: gが帰納的全域関数ならば

f(\vec{x})=\mu y[g(\vec{x},y)=0]

④-1の「\land」以下の条件がないもの

④-3: gが原始帰納的述語がならば

f(\vec{x})=\mu y [P(\vec{x},y)]

というfは部分帰納的関数である

④-1がもっとも、部分帰納的関数を生成する能力が高い

「〜能力が高い」というのは、上の定義の「 gが○○ならば」の部分が指すものの広さのことを言っている

①-1の「帰納的部分関数」が一番広いので、それだけ汎用性の大きさがある

④-3が言えるとき、④-2も言える、このとき④-1も言える

「④-3ならば④-2」の証明

\mu y[]の中身を比較するのがコツ

④-3のPの特性関数f_Pをg(\vec{x},y)=1\dot{-}f_Pとすればいい

gは帰納的全域関数になっているので、④-2の定義を満たしている

「④-2ならば④-1」の証明

「○○ならば」のところを比較すればいい

④-2によってfが部分帰納的関数であることが言えると、

自動的に④-1によっても部分帰納的関数であると言える

なぜなら、ある関数は、全域関数なら部分関数でもあるから

gがそれ

「④-1ならば④-3」の確認

クリーネの標準形定理を使う

k変数の任意の部分帰納的関数は、f(\vec{x})=g(\mu t[T_k(p, \vec{x},t)]) で書ける

④-1を満たす関数fをクリーネの標準形定理に適用させると、

f(\vec{x})=g(\mu t[T_k(p, \vec{x},t)])であるような、関数g,T_kが存在する

そのT_kをPとみなすと、④-3を適用して

f(\vec{x})=\mu y [P(\vec{x},y)] は部分帰納的関数

参考

『C言語による計算の理論』 p.93-