S m n定理

計算可能性理論において、 S m n  定理（「 smn 定理」または「smn 定理」とも表記される。翻訳補題、パラメータ定理、パラメータ化定理とも呼ばれる）は、プログラミング言語（より一般的には、部分計算可能関数のゲーデル番号付け）に関する基本的な結果である（Soare 1987、Rogers 1967）。これは、 Stephen Cole Kleene（1943）によって最初に証明された。${\displaystyle S_{m}^{n}}$は、${\displaystyle S}$添え字付き${\displaystyle n}$上付き文字${\displaystyle m}$定理の元の定式化において（下記参照）。

実際には、この定理は、特定のプログラミング言語と正の整数に対して、${\displaystyle m}$そして${\displaystyle n}$特定のアルゴリズムが存在し、入力としてプログラムのソースコードを受け取ります。${\displaystyle m+n}$自由変数、${\displaystyle m}$このアルゴリズムは、本質的に最初の値を置き換えるソースコードを生成します。${\displaystyle m}$自由変数とは、残りの変数を自由にする変数のことです。

この定理の基本形は、2つの引数を持つ関数に適用される（Nies 2009、p.  6）。ゲーデル数化が与えられた場合${\displaystyle \varphi }$部分計算可能な関数には、原始的な再帰関数が存在する。${\displaystyle s}$以下の性質を持つ2つの引数：すべてのゲーデル数に対して${\displaystyle e}$部分計算可能な関数${\displaystyle f}$2 つの引数を持つ式${\displaystyle \varphi _{s(e,x)}(y)}$そして${\displaystyle f(x,y)}$同じ自然数の組み合わせに対して定義される${\displaystyle x}$そして${\displaystyle y}$、そしてそれらの値は、そのような組み合わせのいずれにおいても等しい。言い換えれば、すべての に対して、関数の次の外延的等価性が成り立つ。${\displaystyle x}$:

${\displaystyle \varphi _{s(e,x)}\simeq \lambda y.\varphi _{e}(x,y).}$

より一般的には、${\displaystyle m,n>0}$原始的な再帰関数が存在する${\displaystyle S_{n}^{m}}$の${\displaystyle m+1}$次のような動作をする引数: すべてのゲーデル数に対して${\displaystyle e}$部分計算可能な関数の${\displaystyle m+n}$引数、およびすべての値${\displaystyle x_{1},x_{2},...,x_{m}}$:

$\displaystyle \varphi _{S_{n}^{m}(e,x_{1},\dots ,x_{m})}\simeq \lambda y_{1},\dots ,y_{n}.\varphi _{e}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n}).}$

機能${\displaystyle s}$上記で説明したものは、${\displaystyle S_{1}^{1}}$。

与えられたアリティ${\displaystyle m}$そして${\displaystyle n}$チューリングマシンごとに${\displaystyle {\text{TM}}_{x}}$位数の${\displaystyle m+n}$そして入力のすべての可能な値に対して${\displaystyle y_{1},\dots ,y_{m}}$チューリングマシンが存在する${\displaystyle {\text{TM}}_{k}}$位数の${\displaystyle n}$、したがって

$\displaystyle \forall z_{1},\dots ,z_{n}:{\text{TM}}_{x}(y_{1},\dots ,y_{m},z_{1},\dots ,z_{n})={\text{TM}}_{k}(z_{1},\dots ,z_{n}).}$

さらに、チューリングマシンが存在する。${\displaystyle S}$これにより${\displaystyle k}$計算対象${\displaystyle x}$そして${\displaystyle y}$; 表記される${\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})}$。

非公式には、${\displaystyle S}$チューリングマシンを発見する${\displaystyle {\text{TM}}_{k}}$これは、値をハードコーディングした結果です。${\displaystyle y}$の中へ${\displaystyle {\text{TM}}_{x}}$この結果は、あらゆるチューリング完全な計算モデルに一般化できる。

以下のLispコードは、Lisp用のs _{11を実装します。}

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

例えば、はに評価されます。ここで、は「新しい」シンボルです。(s11'(lambda(xy)(+xy))3)(lambda(g42)((lambda(xy)(+xy))3g42))g42

• カレー
• クリーネの再帰定理
• 部分的な評価

• Kleene, SC (1936). 「自然数の一般再帰関数」 . Mathematische Annalen . 112 (1): 727–742 . doi : 10.1007/BF01565439 . S2CID 120517999 . 
• Kleene, SC (1938). 「順序数の表記法について」(PDF) . The Journal of Symbolic Logic . 3 (4): 150– 155. doi : 10.2307/2267778 . JSTOR 2267778 . S2CID 34314018 .  （これは、オディフレディの「古典的再帰理論」の1989年版の 131ページで参照されているものです。${\displaystyle S_{n}^{m}}$定理。）
• Nies, A. (2009).計算可能性とランダム性. Oxford Logic Guides. Vol.  51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1. Zbl 1169.03034 . 
• オディフレッディ、P. (1999).古典的再帰理論. ノースホランド. ISBN 0-444-87295-7。
• ロジャース、H. (1987) [1967].再帰関数と有効計算可能性の理論. MIT出版ペーパーバック初版. ISBN 0-262-68052-1。
• Soare, R. (1987).再帰的に列挙可能な集合と次数. 数理論理学の展望. Springer-Verlag. ISBN 3-540-15299-7。

• Weisstein, Eric W. 「クリーネのs - m - n定理」 . MathWorld .