s定理もしくはパラメータ定理とは、再帰理論における定理であり、プログラミング言語（より一般化すれば、計算可能関数のゲーデル数）の基盤となっている。これを最初に証明したのはスティーブン・コール・クリーネである。s-m-n定理と表記されることもある。この定理を実用的に解説すると、あるプログラミング言語と正の整数 "m" と "n" があるとき、"m"+"n" 個の自由変数を持つプログラムのソースコードを操作する特定のアルゴリズムがあることを示している。そのアルゴリズムは、与えられた "m" 個の値を最初の "m" 個の自由変数に束縛し、残りの変数を自由変数のままにしておく。本定理の基本形は、2引数の関数に適用される。再帰関数のゲーデル数 formula_1 が与えられたとき、次のような性質の2引数の原始再帰関数 "s" が存在する。すなわち、あらゆる2引数の関数 "f" のゲーデル数 "p" について、同じ x と y の組合せでの formula_2 と formula_3 が定義され、その組合せにおいて等しい。言い換えれば、次のような外延的等価性が成り立つ。これを一般化するため、元の数を原始再帰関数で引き出せるように、"n" 個の数を1つの数に符号化する方法を採用する。例えば、それらの数のビットをインターリーブするといった符号化が考えられる。すると任意の正の数 "m" と "n" について、"m"+1 個の引数をとる原始再帰関数 formula_5 が存在し、次のように振舞う。すなわち、あらゆる "m+n" 引数の関数のゲーデル数 "p" について、となる。formula_7 は、関数 "s" そのものである。以下のLISPのコードは、s を実装したものである。例えば、(s11 '(lambda (x y) (+ x y)) 3) を評価すると (lambda (y) ((lambda (x y) (+ x y)) 3 y)) になる。

出典:wikipedia