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.

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.

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.