In computability theory the ' theorem, written also as "smn-theorem" or "s-m-n theorem" (also called the translation lemma, parameter theorem, and the parameterization theorem) is a basic result about programming languages (and, more generally, Gödel numberings of the partial computable functions) (Soare 1987, Rogers 1967). It was first proved by Stephen Cole Kleene (1943). The name ' comes from the occurrence of an S with subscript n and superscript m in the original formulation of the theorem (see below).

In practical terms, the theorem says that for a given programming language and positive integers m and n, there exists a particular algorithm that accepts as input the source code of a program with free variables, together with m values. This algorithm generates source code that in essence substitutes the values for the first m free variables, leaving the rest of the variables free.

Details

The basic form of the theorem applies to functions of two arguments (Nies 2009, p.&nbsp;6). Given a Gödel numbering <math>\varphi</math> of partial computable functions, there is a primitive recursive function s of two arguments with the following property: for every Gödel number e of a partial computable function f with two arguments, the expressions <math>\varphi_{s(e, x)}(y)</math> and <math>f(x, y)</math> are defined for the same combinations of natural numbers x and y, and their values are equal for any such combination. In other words, the following extensional equality of functions holds for every x:

: <math>\varphi_{s(e, x)} \simeq \lambda y.\varphi_e(x, y).</math>

More generally, for any , there exists a primitive recursive function <math>S^m_n</math> of arguments that behaves as follows: for every Gödel number e of a partial computable function with arguments, and all values of x<sub>1</sub>, …, x<sub>m</sub>:

: <math>\varphi_{S^m_n(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).</math>

The function s described above can be taken to be <math>S^1_1</math>.

Formal statement

Given arities and , for every Turing Machine <math>\text{TM}_x</math> of arity <math>m + n</math> and for all possible values of inputs <math>y_1, \dots, y_m</math>, there exists a Turing machine <math>\text{TM}_k</math> of arity , such that

: <math>\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).</math>

Furthermore, there is a Turing machine that allows to be calculated from and ; it is denoted <math>k = S_n^m(x, y_1, \dots, y_m)</math>.

Informally, finds the Turing Machine <math>\text{TM}_k</math> that is the result of hardcoding the values of into <math>\text{TM}_x</math>. The result generalizes to any Turing-complete computing model.

Example

The following Lisp code implements s<sub>11</sub> for Lisp.

<syntaxhighlight lang="lisp">

(defun s11 (f x)

(let ((y (gensym)))

(list 'lambda (list y) (list f x y))))

</syntaxhighlight>

For example, evaluates to , where is a "fresh" symbol.

See also

  • Currying
  • Kleene's recursion theorem
  • Partial evaluation

References

  • (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p.&nbsp;131 for the <math>S^m_n</math> theorem.)