「Smn定理」の版間の差分
ja>Cpro 細 ({{DISPLAYTITLE:}}) |
細 (1版 をインポートしました) |
(相違点なし)
| |
2018/8/19/ (日) 17:31時点における版
smn定理もしくはパラメータ定理とは、再帰理論における定理であり、プログラミング言語（より一般化すれば、計算可能関数のゲーデル数）の基盤となっている[1][2]。これを最初に証明したのはスティーブン・コール・クリーネである[3]。s-m-n定理と表記されることもある。
この定理を実用的に解説すると、あるプログラミング言語と正の整数 m と n があるとき、m+n 個の自由変数を持つプログラムのソースコードを操作する特定のアルゴリズムがあることを示している。そのアルゴリズムは、与えられた m 個の値を最初の m 個の自由変数に束縛し、残りの変数を自由変数のままにしておく。
詳細
本定理の基本形は、2引数の関数に適用される。再帰関数のゲーデル数 [math]\varphi[/math] が与えられたとき、次のような性質の2引数の原始再帰関数 s が存在する。すなわち、あらゆる2引数の関数 f のゲーデル数 p について、同じ x と y の組合せでの [math]\varphi_{s(p,x)}(y)[/math] と [math]f(x,y)[/math] が定義され、その組合せにおいて等しい。言い換えれば、次のような外延的等価性が成り立つ。
- [math]\varphi_{s(p,x)} = \lambda y.\varphi_p(x,y)\,[/math]
これを一般化するため、元の数を原始再帰関数で引き出せるように、n 個の数を1つの数に符号化する方法を採用する。例えば、それらの数のビットをインターリーブするといった符号化が考えられる。すると任意の正の数 m と n について、m+1 個の引数をとる原始再帰関数 [math]s^m_n[/math] が存在し、次のように振舞う。すなわち、あらゆる m+n 引数の関数のゲーデル数 p について、
- [math]\varphi_{s^{m}_{n}(p,x_1,\dots,x_m)} = \lambda y_1,\dots,y_n.\varphi_p(x_1,\dots,x_m,y_1,\dots,y_n)\,[/math]
となる。[math]s^1_1[/math] は、関数 s そのものである。
例
以下のLISPのコードは、s11 を実装したものである。
(defun s11 (f x) (list 'lambda '(y) (list f x 'y))
例えば、(s11 '(lambda (x y) (+ x y)) 3) を評価すると (lambda (y) ((lambda (x y) (+ x y)) 3 y)) になる。
関連項目
脚注
- ↑ Soare, R. (1987年). Recursively enumerable sets and degrees, Perspectives in Mathematical Logic. Springer-Verlag. ISBN 3-540-15299-7.
- ↑ Rogers, H. [1967年] (1987年). The Theory of Recursive Functions and Effective Computability. First MIT press paperback edition. ISBN 0-262-68052-1.
- ↑ Kleene, S. C. (1943年). “General recursive functions of natural numbers”. Mathematische Annalen 53: 727–742.
参考文献
- Odifreddi, P. (1999年). Classical Recursion Theory. North-Holland. ISBN 0-444-87295-7.
外部リンク
- Weisstein, Eric W. “Kleene's s-m-n Theorem”. MathWorld（英語）. Template:Cite webの呼び出しエラー：引数 accessdate は必須です。