Smn定理

smn定理（Parameterization Theorem）

smn定理、またはパラメータ定理は、再帰理論の中核を成す重要な定理であり、コンピュータサイエンスにおける計算可能性の理解において、特にプログラミング言語の構造に深い影響を与えています。この定理は、スティーブン・コール・クリーネにより最初に証明され、時折「s-m-n定理」とも呼ばれます。

この定理は、特定の条件下で2引数関数の情報を他の形式に代入できる能力を示しています。具体的には、任意のプログラミング言語において、正の整数 m と n が与えられた場合、m + n 個の自由変数を持つプログラムに対して、特定のアルゴリズムの存在を示しています。このアルゴリズムは、与えられた m 個の値を最初の m 個の自由変数に束縛し、残りの変数は自由のままに保たれます。

基本的な性質

本定理の基本的な形は、2引数の関数に特化しています。与えられた再帰関数のゲーデル数
\( φ \) があるとき、次の性質を持つ原始再帰関数 s が存在します。この場合、あらゆる2引数の関数 f のゲーデル数 p を考えたとき、次の等式が成り立ちます。

\[ φ_{s(p,x)}(y) = f(x,y) \]

この式は、特定の x および y の組み合わせにおいて、s が条件を満たすことを示します。

一般化

smn定理をさらに一般化するために、数値を原始再帰関数として取り扱う手法が採用されます。具体的には、n 個の数を1つの数として符号化するアプローチが導入されます。例えば、数値のビットをインターリーブする方法が考えられます。この結果、任意の正の整数 m および n に対して、m＋1 個の引数を取る原始再帰関数 \( s_n^m \) が存在します。この関数は、次のように振る舞います。

\[ φ_{s_n^m(p,x_1,reakdots,x_m)} = λy_1, reakdots, y_n. φ_p(x_1, reakdots, x_m, y_1, reakdots, y_n) \]

ここで、\( s_{1}^{1} \) は、元の関数 s に帰着します。

実装例

実際のプログラミングでの実装例として、以下のLISPのコードは、\( s_{1}^{1} \) を実装したものです。

```lisp
(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))
```

このように、smn定理はプログラムの引数の取り扱いにおいて、重要な役割を果たしています。さまざまな計算機理論やプログラミングにおける応用があり、これにより計算の仕組みや関数の扱い方を思考する上で不可欠です。

関連項目

• - カリー化: 関数を部分的に適用する技術。
• - クリーネの再帰定理: 再帰理論におけるクリーネの重要な定理。
• - 部分評価: 一部の変数に対して評価を行う方法。

参考文献

• - Odifreddi, P. (1999). _Classical Recursion Theory_. North-Holland. ISBN 0-444-87295-7

外部リンク

• - Kleene's s-m-n Theorem - MathWorld

もう一度検索