In computability theory the S n m 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 S n m 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 g(x,y) which is computable, there exists a total and computable function such that basically "fixing" the first argument of g. It's like partially applying an argument to a function. This is generalized over m,n tuples for x,y. 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 s_m^n is designed to mimic the behavior of \phi(x,y) when given the appropriate parameters. Essentially, by selecting the right values for m and n, you can make s behave like for a specific computation. Instead of dealing with the complexity of \phi(x,y), we can work with a simpler s_m^n 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 \varphi 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 and f(x, y) 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: More generally, for any m, n > 0 , there exists a primitive recursive function S^m_n 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 x1, …, xm: The function s described above can be taken to be S^1_1.

Formal statement

Given arities m and n, for every Turing Machine \text{TM}_x of arity m + n and for all possible values of inputs, there exists a Turing machine \text{TM}_k of arity n, such that Furthermore, there is a Turing machine S that allows k to be calculated from x and y; it is denoted. Informally, S finds the Turing Machine \text{TM}_k that is the result of hardcoding the values of y into \text{TM}_x. 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 and m,n \geq 1 such that, : 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 be a computable function. There, there is a total computable function such that, :

Example

The following Lisp code implements s11 for Lisp. For example, (s11 '(lambda (x y) (+ x y)) 3) evaluates to (lambda (g42) ((lambda (x y) (+ x y)) 3 g42)).