In computability theory the S mn 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 S m n {\displaystyle S_{m}^{n}} comes from the occurrence of an S {\displaystyle S} with subscript n {\displaystyle n} and superscript m {\displaystyle 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 {\displaystyle m} and n {\displaystyle n} , there exists a particular algorithm that accepts as input the source code of a program with m + n {\displaystyle m+n} free variables, together with m {\displaystyle m} values. This algorithm generates source code that in essence substitutes the values for the first m {\displaystyle 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. 6). Given a Gödel numbering φ {\displaystyle \varphi } of partial computable functions, there is a primitive recursive function s {\displaystyle s} of two arguments with the following property: for every Gödel number e {\displaystyle e} of a partial computable function f {\displaystyle f} with two arguments, the expressions φ s ( e , x ) ( y ) {\displaystyle \varphi _{s(e,x)}(y)} and f ( x , y ) {\displaystyle f(x,y)} are defined for the same combinations of natural numbers x {\displaystyle x} and y {\displaystyle y} , and their values are equal for any such combination. In other words, the following extensional equality of functions holds for every x {\displaystyle x} :
φ s ( e , x ) ≃ λ y . φ e ( x , y ) . {\displaystyle \varphi _{s(e,x)}\simeq \lambda y.\varphi _{e}(x,y).}
More generally, for any m , n > 0 {\displaystyle m,n>0} , there exists a primitive recursive function S n m {\displaystyle S_{n}^{m}} of m + 1 {\displaystyle m+1} arguments that behaves as follows: for every Gödel number e {\displaystyle e} of a partial computable function with m + n {\displaystyle m+n} arguments, and all values of x 1 , x 2 , . . . , x m {\displaystyle x_{1},x_{2},...,x_{m}} :
φ S n m ( e , x 1 , … , x m ) ≃ λ y 1 , … , y n . φ e ( x 1 , … , x m , y 1 , … , y n ) . {\displaystyle \varphi _{S_{n}^{m}(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}).}
The function s {\displaystyle s} described above can be taken to be S 1 1 {\displaystyle S_{1}^{1}} .
… excerpt ends here. Continue reading the full article.
