User:IssaRice/Computability and logic/S–m–n theorem: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
The '''s–m–n theorem''' states that if <math>\varphi_e</math> is an <math>(m+n)</math> place [[../Computable partial function|computable partial function]] and <math>a_1,\ldots,a_m</math> are natural numbers, then there exists a [[../Primitive recursive function|primitive recursive function]] <math>s^m_n</math> such that <math>\varphi_{s^m_n(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)]</math>. | The '''s–m–n theorem''' (also called the '''parametrization theorem''') states that if <math>\varphi_e</math> is an <math>(m+n)</math> place [[../Computable partial function|computable partial function]] and <math>a_1,\ldots,a_m</math> are natural numbers, then there exists a [[../Primitive recursive function|primitive recursive function]] <math>s^m_n</math> such that <math>\varphi_{s^m_n(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)]</math>. | ||
Roughly speaking, the theorem states that if we start out with a computable partial function <math>\varphi_e</math> of <math>m+n</math> variables, then we can fill in <math>m</math> of the variables with actual values. When we do this, the resulting <math>n</math>-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.<ref>https://cs.stackexchange.com/questions/80837/is-smn-theorem-the-same-concept-as-currying</ref> | |||
==References== | |||
<references/> | |||
Revision as of 06:41, 18 December 2018
The s–m–n theorem (also called the parametrization theorem) states that if is an place computable partial function and are natural numbers, then there exists a primitive recursive function such that .
![{\displaystyle \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})]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/da691513388a92532626fe4d68fc835a2f6bd5c3)
Roughly speaking, the theorem states that if we start out with a computable partial function of variables, then we can fill in of the variables with actual values. When we do this, the resulting -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.[1]