User:IssaRice/Computability and logic/S–m–n theorem

The s–m–n theorem (also called the parametrization theorem) states that if $\varphi _{e}$ is an $(m+n)$ place computable partial function and $a_{1},\ldots ,a_{m}$ are natural numbers, then there exists a primitive recursive function $s_{n}^{m}$ such that $\varphi _{s_{n}^{m}(e,a_{1},\ldots ,a_{m})}\simeq \lambda y_{1}\cdots y_{n}[\varphi _{e}(x_{1},\ldots ,x_{m},y_{1},\ldots ,y_{n})]$.

In other words, the theorem states that if we start out with a computable partial function $\varphi _{e}$ of $m+n$ variables, then we can fill in $m$ of the variables with actual values. When we do this, the resulting $n$-place partial function continues to be computable. Moreover, we can find the index of this new partial function in terms of the old index and the values in a primitive recursive way.

To give an example, suppose we start out with the function $\varphi _{e}(x,y)=x+y$. Then we can "fill in" one of the variables with a value, e.g. by taking $y=3$. Now we have $\varphi _{e}(x,3)=x+3$. The s–m–n theorem claims that this resulting function is also computable. It also says that we can find the source code of this new function using $e$ (the original source code) and 3 (the value we are substituting).

The s–m–n theorem is essentially the same thing as currying in functional programming languages.

The s–m–n theorem, together with the universal function, is useful for proving other theorems and also to avoid the arbitrariness of the specific encoding used.

Different kinds of proofs:

• Tape/register-based way
• Using recursive functions and ways of encoding them

Etymology

The name "s–m–n" comes from the notation $s_{n}^{m}$ (denoted $s_{m}^{n}$ in some texts) for the function that finds the new index.