S^m_n定理

パラメータ定理ともいう

Stephen Cole Kleeneが最初に証明した

単純な例

任意の2引数関数fのゲーデル数をpとする

固定された実引数x,yについて、\varphi_{s(p,x)}(y)とf(x,y)が定義でき、その組み合わせが等しいような原始帰納的関数sが存在する

言い換えれば次のような外延的等価性が成り立つ

\varphi_{s(p,x)}=\lambda y.\varphi_p(x,y)

重要なのは、「↑を満たすような[* sが存在する]」という点

補足

ゲーデル数aをデコードしたものを\varphi_aと表している

つまり、上の例ではf=\varphi_p

ゲーデル数と、それをデコードしたものを同列に扱うからめちゃくちゃややこしくなる

一般化したものがS^m_n定理

\varphi_{s_{n}^{m}\left(p, x_{1}, \ldots, x_{m}\right)}=\lambda y_{1}, \ldots, y_{n} \cdot \varphi_{p}\left(x_{1}, \ldots, x_{m}, y_{1}, \ldots, y_{n}\right)

ref p.59

以下を満たすような(m+1)引数の計算可能全域関数S^m_nが存在する

任意の自然数p,x_1,\cdots,x_n,y_1,\cdots,y_mに対して以下が成り立つ

1. S^m_n(p,\vec{y})はn入力のプログラムのコードになる

2. \mathrm{comp}(S^m_n(p,\vec{y}),\lang\vec{x}\rang)=\mathrm{comp}(p,\lang\vec{x},\vec{y}\rang)

省略せずに書くなら\mathrm{comp}(S^m_n(p,y_1,\cdots,y_m),\lang x_1,\cdots,x_n\rang)=\mathrm{comp}(p,\lang x_1,\cdots,x_n,y_1,\cdots,y_m\rang)

補足

万能関数\mathrm{comp}の第一引数はプログラムのコードであることに注意

つまりS^m_n(p,\vec{y})は、一つの自然数であり、コードである

S^m_nは、

m+1個の引数を取ると、

「n個の引数(のコード)をとる関数」のコードになる

つまり「S^m_n(p,\vec{y})」はとあるコード。

S^m_nは、

引数である、関数のコードpと、パラメータの値\vec{y}から

パラメータ\vec{y}ごとに定まる、関数のコードS^m_n(p,\vec{y})を求める

ような関数

S^m_nは、

計算可能

全域関数

S :: p -> (y1 -> .. -> ym) -> <x1 -> .. -> xn -> Code> のイメージ

関数gが\vec{y}ごとに定まる

カリー化っぽいな