Smn定理のソースを表示

{{DISPLAYTITLE:s<sub>mn</sub>定理}}
'''s<sub>mn</sub>定理''' ({{lang-en-short|s<sub>mn</sub> theorem}}) もしくは'''パラメータ定理''' ({{lang-en-short|parameterization theorem}}) とは、[[再帰理論]]における[[定理]]であり、[[プログラミング言語]]（より一般化すれば、[[計算可能関数]]の[[ゲーデル数]]）の基盤となっている<ref>{{cite book | author = Soare, R.| title = Recursively enumerable sets and degrees | series = Perspectives in Mathematical Logic | publisher = Springer-Verlag | date = 1987年 | id = ISBN 3-540-15299-7 }}</ref><ref>{{cite book | author = Rogers, H. | title = The Theory of Recursive Functions and Effective Computability | publisher = First MIT press paperback edition | date = 1987年 | origyear=1967年 |id = ISBN 0-262-68052-1 }}</ref>。これを最初に証明したのは[[スティーブン・コール・クリーネ]]である<ref>{{cite journal | author = Kleene, S. C. | title = General recursive functions of natural numbers | journal = Mathematische Annalen | volume = 53 | pages = 727–742 | date = 1943年 }}</ref>。'''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]]のコードは、s<sub>11</sub> を実装したものである。

 (defun s11 (f x)
   (list 'lambda '(y) (list f x 'y))

例えば、<tt>(s11 '(lambda (x y) (+ x y)) 3)</tt> を評価すると <tt>(lambda (y) ((lambda (x y) (+ x y))  3 y))</tt> になる。

== 関連項目 ==
*[[カリー化]]
*[[クリーネの再帰定理]]
*[[部分評価]]

== 脚注 ==
{{Reflist}}

== 参考文献 ==
* {{cite book | author = Odifreddi, P. | title = Classical Recursion Theory | publisher = North-Holland| date = 1999年| id = ISBN 0-444-87295-7 }}

== 外部リンク ==
*{{MathWorld|urlname=Kleeness-m-nTheorem|title=Kleene's s-m-n Theorem}}

{{DEFAULTSORT:SNMていり}}
[[Category:数理論理学]]
[[Category:計算可能性理論]]
[[Category:計算理論の定理]]
[[Category:スティーヴン・コール・クリーネ]]
[[Category:数学に関する記事]]