On transforming a program by substituting constants for free variables
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 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 "m" + "n" free variables, together with "m" values. This algorithm generates source code that effectively substitutes the values for the first "m" free variables, leaving the rest of the variables free.
The smn-theorem states that given a function of two arguments formula_1 which is computable, there exists a total and computable function such that formula_2 basically "fixing" the first argument of formula_3. It's like partially applying an argument to a function. This is generalized over formula_4 tuples for formula_5. In other words, it addresses the idea of "parametrization" or "indexing" of computable functions. It's like creating a simplified version of a function that takes an additional parameter (index) to mimic the behavior of a more complex function.
The function formula_6 is designed to mimic the behavior of formula_7 when given the appropriate parameters. Essentially, by selecting the right values for formula_8 and formula_9, you can make formula_10 behave like for a specific computation. Instead of dealing with the complexity of formula_7, we can work with a simpler formula_6 that captures the essence of the computation.
Details.
The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering formula_13 of recursive functions, there is a primitive recursive function "s" of two arguments with the following property: for every Gödel number "p" of a partial computable function "f" with two arguments, the expressions formula_14 and formula_15 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":
 formula_16
More generally, for any "m", "n" ; 0, there exists a primitive recursive function formula_17 of "m" + 1 arguments that behaves as follows: for every Gödel number "p" of a partial computable function with "m" + "n" arguments, and all values of "x"1, …, "x""m":
 formula_18
The function "s" described above can be taken to be formula_19.
Formal statement.
Given arities m and n, for every Turing Machine formula_20 of arity formula_21 and for all possible values of inputs formula_22, there exists a Turing machine formula_23 of arity n, such that
 formula_24
Furthermore, there is a Turing machine S that allows k to be calculated from x and y; it is denoted formula_25.
Informally, S finds the Turing Machine formula_23 that is the result of hardcoding the values of y into formula_20. The result generalizes to any Turing-complete computing model.
This can also be extended to total computable functions as follows:
Given a total computable function formula_28 and formula_29 such that formula_30, formula_31:
formula_32
There is also a simplified version of the same theorem (defined infact as "simplified smn-theorem", which basically uses a total computable function as index as follows:
Let formula_33 be a computable function. There, there is a total computable function formula_34 such that formula_35, formula_36:
formula_37
Example.
The following Lisp code implements s11 for Lisp.
 (let ((y (gensym)))
 (list 'lambda (list y) (list f x y))))
For example, evaluates to .