Smn定理 - 暇つぶしWikipedia

Smn定理

smn定理 (英: smn theorem) もしくはパラメータ定理 (英: parameterization theorem) とは、再帰理論における定理であり、プログラミング言語（より一般化すれば、計算可能関数のゲーデル数）の基盤となっている [1][2]。これを最初に証明したのはスティーブン・コール・クリーネである [3]。s-m-n定理と表記されることもある。

この定理を実用的に解説すると、あるプログラミング言語と正の整数 m と n があるとき、m+n 個の自由変数を持つプログラムのソースコードを操作する特定のアルゴリズムがあることを示している。そのアルゴリズムは、与えられた m 個の値を最初の m 個の自由変数に束縛し、残りの変数を自由変数のままにしておく。
詳細

本定理の基本形は、2引数の関数に適用される。再帰関数のゲーデル数 φ {\displaystyle \varphi } が与えられたとき、次のような性質の2引数の原始再帰関数 s が存在する。すなわち、あらゆる2引数の関数 f のゲーデル数 p について、同じ x と y の組合せでの φ s ( p , x ) ( y ) {\displaystyle \varphi _{s(p,x)}(y)} と f ( x , y ) {\displaystyle f(x,y)} が定義され、その組合せにおいて等しい。言い換えれば、次のような外延的等価性が成り立つ。 φ s ( p , x ) = λ y . φ p ( x , y ) {\displaystyle \varphi _{s(p,x)}=\lambda y.\varphi _{p}(x,y)\,}

これを一般化するため、元の数を原始再帰関数で引き出せるように、n 個の数を1つの数に符号化する方法を採用する。例えば、それらの数のビットをインターリーブするといった符号化が考えられる。すると任意の正の数 m と n について、m+1 個の引数をとる原始再帰関数 s n m {\displaystyle s_{n}^{m}} が存在し、次のように振舞う。すなわち、あらゆる m+n 引数の関数のゲーデル数 p について、 φ s n m ( p , x 1 , … , x m ) = λ y 1 , … , y n . φ p ( x 1 , … , x m , y 1 , … , y n ) {\displaystyle \varphi _{s_{n}^{m}(p,x_{1},\dots ,x_{m})}=\lambda y_{1},\dots ,y_{n}.\varphi _{p}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n})\,}

となる。 s 1 1 {\displaystyle s_{1}^{1}} は、関数 s そのものである。
例

以下の LISPのコードは、s11 を実装したものである。(defun s11 (f x) (list 'lambda '(y) (list f x 'y))

Size:8871 Bytes
出典: フリー百科事典『ウィキペディア（Wikipedia）』
担当:undef