Smn theorem

<h2 id="details">Details</h2>
The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering 
 
 
 
 φ
 
 
 {\displaystyle \varphi }
 
 of recursive functions, there is a <a href="/facts/Primitive_recursive_function/4z97gRnl">primitive recursive function</a> s of two arguments with the following property: for every Gödel number p of a partial computable function f with two arguments, the expressions 
 
 
 
 
 φ
 
 s
 (
 p
 ,
 x
 )
 
 
 (
 y
 )
 
 
 {\displaystyle \varphi _{s(p,x)}(y)}
 
 and 
 
 
 
 f
 (
 x
 ,
 y
 )
 
 
 {\displaystyle f(x,y)}
 
 are defined for the same combinations of natural numbers x and y, and their values are equal for any such combination. In other words, the following <a href="/facts/Extensional_equality/CwPNkVTW">extensional equality</a> of functions holds for every x:

φ
          
            s
            (
            p
            ,
            x
            )
          
        
        ≃
        λ
        y
        .
        
          φ
          
            p
          
        
        (
        x
        ,
        y
        )
        .
      
    
    {\displaystyle \varphi _{s(p,x)}\simeq \lambda y.\varphi _{p}(x,y).}

More generally, for any m, n > 0, there exists a primitive recursive function 
 
 
 
 
 S
 
 n
 
 
 m
 
 
 
 
 {\displaystyle S_{n}^{m}}
 
 of m + 1 arguments that behaves as follows: for every Gödel number p of a partial computable function with m + n arguments, and all values of x1, …, xm:

φ
          
            
              S
              
                n
              
              
                m
              
            
            (
            p
            ,
            
              x
              
                1
              
            
            ,
            …
            ,
            
              x
              
                m
              
            
            )
          
        
        ≃
        λ
        
          y
          
            1
          
        
        ,
        …
        ,
        
          y
          
            n
          
        
        .
        
          φ
          
            p
          
        
        (
        
          x
          
            1
          
        
        ,
        …
        ,
        
          x
          
            m
          
        
        ,
        
          y
          
            1
          
        
        ,
        …
        ,
        
          y
          
            n
          
        
        )
        .
      
    
    {\displaystyle \varphi _{S_{n}^{m}(p,x_{1},\dots ,x_{m})}\simeq \lambda y_{1},\dots ,y_{n}.\varphi _{p}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n}).}

The function s described above can be taken to be 
 
 
 
 
 S
 
 1
 
 
 1
 
 
 
 
 {\displaystyle S_{1}^{1}}
 
.

<h2 id="formal-statement">Formal statement</h2>
Given arities m and n, for every Turing Machine 
 
 
 
 
 
 TM
 
 
 x
 
 
 
 
 {\displaystyle {\text{TM}}_{x}}
 
 of arity 
 
 
 
 m
 +
 n
 
 
 {\displaystyle m+n}
 
 and for all possible values of inputs 
 
 
 
 
 y
 
 1
 
 
 ,
 …
 ,
 
 y
 
 m
 
 
 
 
 {\displaystyle y_{1},\dots ,y_{m}}
 
, there exists a Turing machine 
 
 
 
 
 
 TM
 
 
 k
 
 
 
 
 {\displaystyle {\text{TM}}_{k}}
 
 of arity n, such that

∀
        
          z
          
            1
          
        
        ,
        …
        ,
        
          z
          
            n
          
        
        :
        
          
            TM
          
          
            x
          
        
        (
        
          y
          
            1
          
        
        ,
        …
        ,
        
          y
          
            m
          
        
        ,
        
          z
          
            1
          
        
        ,
        …
        ,
        
          z
          
            n
          
        
        )
        =
        
          
            TM
          
          
            k
          
        
        (
        
          z
          
            1
          
        
        ,
        …
        ,
        
          z
          
            n
          
        
        )
        .
      
    
    {\displaystyle \forall z_{1},\dots ,z_{n}:{\text{TM}}_{x}(y_{1},\dots ,y_{m},z_{1},\dots ,z_{n})={\text{TM}}_{k}(z_{1},\dots ,z_{n}).}

Furthermore, there is a Turing machine S that allows k to be calculated from x and y; it is denoted 
 
 
 
 k
 =
 
 S
 
 n
 
 
 m
 
 
 (
 x
 ,
 
 y
 
 1
 
 
 ,
 …
 ,
 
 y
 
 m
 
 
 )
 
 
 {\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})}
 
.
Informally, S finds the Turing Machine 
 
 
 
 
 
 TM
 
 
 k
 
 
 
 
 {\displaystyle {\text{TM}}_{k}}
 
 that is the result of hardcoding the values of y into 
 
 
 
 
 
 TM
 
 
 x
 
 
 
 
 {\displaystyle {\text{TM}}_{x}}
 
. The result generalizes to any <a href="/facts/Turing-complete/73goop44">Turing-complete</a> computing model.
This can also be extended to <a href="/facts/Total_function/0vJMw0Nm">total</a> <a href="/facts/Computable_function/dzwBlLGn">computable functions</a> as follows:
Given a total computable function 
 
 
 
 
 s
 
 m
 ,
 n
 
 
 :
 
 
 N
 
 
 m
 +
 1
 
 
 →
 
 N
 
 
 
 {\displaystyle s_{m,n}:\mathbb {N} ^{m+1}\rightarrow \mathbb {N} }
 
 and 
 
 
 
 m
 ,
 n
 ≥
 1
 
 
 {\displaystyle m,n\geq 1}
 
 such that 
 
 
 
 ∀
 
 
 
 x
 →
 
 
 
 ∈
 
 
 N
 
 
 m
 
 
 ,
 ∀
 
 
 
 y
 →
 
 
 
 ∈
 
 
 N
 
 
 n
 
 
 
 
 {\displaystyle \forall {\vec {x}}\in \mathbb {N} ^{m},\forall {\vec {y}}\in \mathbb {N} ^{n}}
 
, 
 
 
 
 ∀
 e
 ∈
 
 N
 
 
 
 {\displaystyle \forall e\in \mathbb {N} }
 
:

 
 
 
 
 ϕ
 
 e
 
 
 m
 +
 n
 
 
 (
 
 
 
 x
 →
 
 
 
 ,
 
 
 
 y
 →
 
 
 
 )
 =
 
 ϕ
 
 
 s
 
 m
 ,
 n
 
 
 
 (
 e
 ,
 
 
 
 x
 →
 
 
 
 )
 
 
 
 n
 
 
 (
 
 
 
 y
 →
 
 
 
 )
 
 
 {\displaystyle \phi _{e}^{m+n}({\vec {x}},{\vec {y}})=\phi _{s_{m,n}{(e,{\vec {x}})}}^{n}({\vec {y}})}

There is also a simplified version of the same theorem (defined infact as "simplified smn-theorem", which basically uses a total computable function as index as follows:
Let 
 
 
 
 f
 :
 
 
 N
 
 
 n
 +
 m
 
 
 →
 
 N
 
 
 
 {\displaystyle f:\mathbb {N} ^{n+m}\rightarrow \mathbb {N} }
 
 be a computable function. There, there is a total computable function 
 
 
 
 s
 :
 
 
 N
 
 
 m
 
 
 →
 
 N
 
 
 
 {\displaystyle s:\mathbb {N} ^{m}\rightarrow \mathbb {N} }
 
 such that 
 
 
 
 ∀
 x
 ∈
 
 
 N
 
 
 m
 
 
 
 
 {\displaystyle \forall x\in \mathbb {N} ^{m}}
 
, 
 
 
 
 
 
 
 y
 →
 
 
 
 ∈
 
 
 N
 
 
 n
 
 
 
 
 {\displaystyle {\vec {y}}\in \mathbb {N} ^{n}}
 
:

 
 
 
 f
 (
 
 
 
 x
 →
 
 
 
 ,
 
 
 
 y
 →
 
 
 
 )
 =
 
 ϕ
 
 S
 (
 
 
 
 x
 →
 
 
 
 )
 
 
 (
 n
 )
 
 
 (
 
 
 
 y
 →
 
 
 
 )
 
 
 {\displaystyle f({\vec {x}},{\vec {y}})=\phi _{S({\vec {x}})}^{(n)}({\vec {y}})}

<h2 id="example">Example</h2>
The following <a href="/facts/Lisp_programming_language/xJHA3CrX">Lisp</a> code implements s11 for Lisp.

(defun s11 (f x)
 (let ((y (gensym)))
 (list 'lambda (list y) (list f x y))))

For example, (s11 '(lambda (x y) (+ x y)) 3) evaluates to (lambda (g42) ((lambda (x y) (+ x y)) 3 g42)).

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Currying/AmD3PP5B">Currying</a></li>
<li><a href="/facts/Kleene%27s_recursion_theorem/Q6mLLe3B">Kleene's recursion theorem</a></li>
<li><a href="/facts/Partial_evaluation/cSBKhRPo">Partial evaluation</a></li></ul>

<ul><li>Kleene, S. C. (1936). <a href="http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=PPN235181684_0112&DMDID=DMDLOG_0043&L=1">"General recursive functions of natural numbers"</a>. Mathematische Annalen. 112 (1): 727–742. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2FBF01565439">10.1007/BF01565439</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:120517999">120517999</a>.</li>
<li>Kleene, S. C. (1938). <a href="http://www.thatmarcusfamily.org/philosophy/Course_Websites/Readings/Kleene%20-%20Ordinals.pdf">"On Notations for Ordinal Numbers"</a> (PDF). The Journal of Symbolic Logic. 3 (4): 150–155. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F2267778">10.2307/2267778</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/2267778">2267778</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:34314018">34314018</a>. (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the 
 
 
 
 
 S
 
 n
 
 
 m
 
 
 
 
 {\displaystyle S_{n}^{m}}
 
 theorem.)</li>
<li>Nies, A. (2009). Computability and randomness. Oxford Logic Guides. Vol. 51. Oxford: Oxford University Press. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-0-19-923076-1. <a href="/facts/Zbl_(identifier)/P6rFxKKx">Zbl</a> <a href="https://zbmath.org/?format=complete&q=an:1169.03034">1169.03034</a>.</li>
<li>Odifreddi, P. (1999). <a href="https://archive.org/details/classicalrecursi0000odif">Classical Recursion Theory</a>. North-Holland. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-444-87295-7.</li>
<li>Rogers, H. (1987) [1967]. The Theory of Recursive Functions and Effective Computability. First MIT press paperback edition. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-262-68052-1.</li>
<li>Soare, R. (1987). Recursively enumerable sets and degrees. Perspectives in Mathematical Logic. Springer-Verlag. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 3-540-15299-7.</li></ul>
<h2 id="external-links">External links</h2>
<ul><li><a href="/facts/Eric_W._Weisstein/FbMuVDep">Weisstein, Eric W.</a> <a href="https://mathworld.wolfram.com/Kleeness-m-nTheorem.html">"Kleene's s-m-n Theorem"</a>. <a href="/facts/MathWorld/yc1jodbq">MathWorld</a>.</li></ul>

Smn theorem open-in-new

Smn theorem