S-m-n定理
$ S^m_n定理
smn theorem
単純な例
固定された実引数$ 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
ゲーデル数と、それをデコードしたものを同列に扱うからめちゃくちゃややこしくなるmrsekut.icon
一般化したものが$ 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 『C言語による計算の理論』.icon 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}ごとに定まる
https://gyazo.com/292520ca5514ca8df19f43207b7f8051