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

The s–m–n theorem (also called the parametrization theorem) states that if ${\phi }_e$ is an $(m+n)$ place computable partial function and $a_1,\dots ,a_m$ are natural numbers, then there exists a primitive recursive function $s_n^m$ such that ${\phi }_{s_n^m(e,a_1,\dots ,a_m)}\simeq \lambda y_1\cdots y_n[{\phi }_e(x_1,\dots ,x_m,y_1,\dots ,y_n)]$.

Roughly speaking, the theorem states that if we start out with a computable partial function ${\phi }_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.

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