Smn Theorem

Idea

Loosely, the $S_n^m$ theorem states that arguments can be “hard-coded” into programs effectively.

Statement

Fix some computable denumeration of partial computable functions ${\varphi }_e^{(n)}:{\mathbb{N}}^n\rightharpoonup \mathbb{N}$. Then there is a primitive-recursive function $s:{\mathbb{N}}^2\to \mathbb{N}$ such that for every program index $e$ and every value $x,y:\mathbb{N}$,

$${\varphi }_{s(e,x)}^{(1)}(y)\simeq {\varphi }_e^{(2)}(x,y)$$

Remarks

This is effectively currying at the level of program codes.

References

cutland1980-computability