|
|
| 1行目: |
1行目: |
| − | {{DISPLAYTITLE:s<sub>mn</sub>定理}} | + | {{テンプレート:20180815sk}} |
| − | '''s<sub>mn</sub>定理'''もしくは'''パラメータ定理'''とは、[[再帰理論]]における[[定理]]であり、[[プログラミング言語]]（より一般化すれば、[[計算可能関数]]の[[ゲーデル数]]）の基盤となっている<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:数学に関する記事]]
| |