Smn定理

計算可能性理論では、 S m
n 定理は、「 smn定理」または「smn定理」とも表記され（翻訳補題、パラメータ定理、パラメータ化定理とも呼ばれる）、プログラミング言語（およびより一般的には、計算可能関数のゲーデル数）に関する基本的な結果である（Soare 1987、Rogers 1967）。これは、 Stephen Cole Kleene（1943）によって最初に証明されました。S m
n これは、定理の元の定式化で 下付き文字nと上付き文字mを持つSが出現したことに由来します(以下を参照)。

実用的には、この定理は、与えられたプログラミング言語と正の整数mおよびnに対して、 m + n 個の自由変数とm個の値を持つプログラムのソース コードを入力として受け入れる特定のアルゴリズムが存在することを示しています。このアルゴリズムは、最初のm 個の自由変数の値を効果的に置き換え、残りの変数を自由のままにするソース コードを生成します。

smn 定理は、計算可能な2つの引数の関数が与えられた場合、基本的に の最初の引数を「固定」する、完全かつ計算可能な関数が存在することを述べています。これは、引数を関数に部分的に適用するようなものです。これは、のタプルに一般化されています。言い換えると、これは計算可能な関数の「パラメーター化」または「インデックス付け」の考え方に対応しています。これは、より複雑な関数の動作を模倣するために、追加のパラメーター (インデックス) を受け取る関数の簡略化されたバージョンを作成するようなものです。 ${\displaystyle g(x,y)}$${\displaystyle \phi _{s}(x)(y)=g(x,y)}$${\displaystyle g}$${\displaystyle m,n}$${\displaystyle x,y}$

関数は、適切なパラメータが与えられた場合にの動作を模倣するように設計されています。基本的に、とに適切な値を選択することで、 を特定の計算に対して のように動作させることができます。 の複雑さに対処する代わりに、計算の本質を捉えたより 単純な を扱うことができます。${\displaystyle s_{m}^{n}}$${\displaystyle \phi (x,y)}$${\displaystyle m}$${\displaystyle n}$${\displaystyle s}$${\displaystyle \phi (x,y)}$${\displaystyle s_{m}^{n}}$

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

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

より一般的には、任意のm、n > 0に対して、次のように動作するm + 1 個の引数を持つ原始再帰関数が存在する。m + n 個の引数を持つ部分計算可能関数のすべてのゲーデル数pと、すべてのx ₁、…、x _mの値に対して、次のようになる。 ${\displaystyle S_{n}^{m}}$

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

上記の関数sは とみなすことができます。 ${\displaystyle S_{1}^{1}}$

引数がmとnのとき、引数がnのチューリングマシンと入力の可能な値すべてに対して、引数がnのチューリングマシンが存在し、 ${\displaystyle {\text{TM}}_{x}}$${\displaystyle m+n}$${\displaystyle y_{1},\dots ,y_{m}}$${\displaystyle {\text{TM}}_{k}}$

${\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}).}$

さらに、 xとyからk を計算できるチューリングマシンSがあり、これは と表記されます。 ${\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})}$

非公式には、S はyの値を にハードコーディングした結果であるチューリング マシンを見つけます。結果は、任意のチューリング完全なコンピューティング モデルに一般化されます。 ${\displaystyle {\text{TM}}_{k}}$${\displaystyle {\text{TM}}_{x}}$

これは次のように全 計算可能関数に拡張することもできます。

となる全計算可能関数およびが与えられた場合、次のようになります。 ${\displaystyle s_{m,n}:\mathbb {N} ^{m+1}\rightarrow \mathbb {N} }$${\displaystyle m,n\geq 1}$${\displaystyle \forall {\vec {x}}\in \mathbb {N} ^{m},\forall {\vec {y}}\in \mathbb {N} ^{n}}$${\displaystyle \forall e\in \mathbb {N} }$

${\displaystyle \phi _{e}^{m+n}({\vec {x}},{\vec {y}})=\phi _{s_{m,n}{(e,{\vec {x}})}}^{n}({\vec {y}})}$

同じ定理の簡略化されたバージョン（実際には「簡略化された smn 定理」として定義され、基本的に次のように合計計算可能関数をインデックスとして使用します）もあります。

を 計算可能関数とします。ここで、 となる全計算可能関数が存在します。${\displaystyle f:\mathbb {N} ^{n+m}\rightarrow \mathbb {N} }$${\displaystyle s:\mathbb {N} ^{m}\rightarrow \mathbb {N} }$${\displaystyle \forall x\in \mathbb {N} ^{m}}$${\displaystyle {\vec {y}}\in \mathbb {N} ^{n}}$

${\displaystyle f({\vec {x}},{\vec {y}})=\phi _{S({\vec {x}})}^{(n)}({\vec {y}})}$

次のLispコードは Lisp 用の s ₁₁を実装します。

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

たとえば、は と評価されます。 (s11 '(lambda (x y) (+ x y)) 3)(lambda (g42) ((lambda (x y) (+ x y)) 3 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 年版の Odifreddi の「Classical Recursion Theory」の 131 ページで定理について示されている参照です。)${\displaystyle S_{n}^{m}}$
• Nies, A. (2009).計算可能性とランダム性. Oxford Logic Guides. 第 51 巻. オックスフォード: Oxford University Press. ISBN 978-0-19-923076-1.ZBL1169.03034  。​
• Odifreddi, P. (1999).古典的再帰理論. North-Holland. ISBN 0-444-87295-7。
• ロジャース、H. (1987) [1967]。再帰関数の理論と効果的な計算可能性。MITプレスペーパーバック第1版。ISBN 0-262-68052-1。
• Soare, R. (1987)。再帰的に列挙可能な集合と次数。数理論理学の展望。Springer- Verlag。ISBN 3-540-15299-7。

• Weisstein, Eric W.「Kleene の smn 定理」。MathWorld。