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

Revision as of 07:13, 18 December 2018

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.

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

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.

References

↑ https://cs.stackexchange.com/questions/80837/is-smn-theorem-the-same-concept-as-currying

[1] ttps://cs.stackexchange.com/questions/80837/is-smn-theorem-the-same-concept-as-currying

[1]

@@ Line 1: / Line 1: @@
 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.
+In other words, 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>