# Smn theorem

In computability theory the S m n 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 m n 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 $\phi _{s}(x)(y)=g(x,y)$ 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 $\varphi _{s(p,x)}(y)$ 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:
    $\varphi _{s(p,x)}\simeq \lambda y.\varphi _{p}(x,y).$
More generally, for any m, n > 0, there exists a primitive recursive function $S_{n}^{m}$ 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$:
    $\varphi _{S_{n}^{m}(p,x_{1},\dots ,x_{m})}\simeq \lambda y_{1},\dots ,y_{n}.\varphi _{p}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n}).$
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 $y_{1},\dots ,y_{m}$, there exists a Turing machine ${\text{TM}}_{k}$ of arity n, such that
    $\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}).$
Furthermore, there is a Turing machine S that allows k to be calculated from x and y; it is denoted $k=S_{n}^{m}(x,y_{1},\dots ,y_{m})$.
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 $s_{m,n}:\mathbb {N} ^{m+1}\rightarrow \mathbb {N}$ and $m,n\geq 1$ such that $\forall {\vec {x}}\in \mathbb {N} ^{m},\forall {\vec {y}}\in \mathbb {N} ^{n}$, $\forall e\in \mathbb {N}$:
$\phi _{e}^{m+n}({\vec {x}},{\vec {y}})=\phi _{s_{m,n}{(e,{\vec {x}})}}^{n}({\vec {y}})$
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 $f:\mathbb {N} ^{n+m}\rightarrow \mathbb {N}$ be a computable function. There, there is a total computable function $s:\mathbb {N} ^{m}\rightarrow \mathbb {N}$ such that $\forall x\in \mathbb {N} ^{m}$, ${\vec {y}}\in \mathbb {N} ^{n}$:
$f({\vec {x}},{\vec {y}})=\phi _{S({\vec {x}})}^{(n)}({\vec {y}})$

## Example

The following Lisp code implements s$_{11}$ for Lisp.
For example, (s11 '(lambda (x y) (+ x y)) 3) evaluates to (lambda (g42) ((lambda (x y) (+ x y)) 3 g42)).