Smn theorem

Short description: On transforming a program by substituting constants for free variables

In computability theory the Template:Subsup theorem, written also as "smn-theorem" or "s-m-n theorem" (also called the translation lemma, parameter theorem, and the parameterization theorem) is a basic result about programming languages (and, more generally, Gödel numberings of the computable functions) (Soare 1987, Rogers 1967). It was first proved by Stephen Cole Kleene (1943). The name Template:Subsup comes from the occurrence of an S with subscript n and superscript m in the original formulation of the theorem (see below).

In practical terms, the theorem says that for a given programming language and positive integers m and n, there exists a particular algorithm that accepts as input the source code of a program with m + n free variables, together with m values. This algorithm generates source code that effectively substitutes the values for the first m free variables, leaving the rest of the variables free.

The smn-theorem states that given a function of two arguments [math]\displaystyle{ g(x,y) }[/math] which is computable, there exists a total and computable function such that [math]\displaystyle{ \phi_s(x)(y)=g(x,y) }[/math] basically "fixing" the first argument of [math]\displaystyle{ g }[/math]. It's like partially applying an argument to a function. This is generalized over [math]\displaystyle{ m,n }[/math] tuples for [math]\displaystyle{ x,y }[/math]. In other words,it addresses the idea of "parametrization" or "indexing" of computable functions. It's like creating a simplified version of a function that takes an additional parameter (index) to mimic the behavior of a more complex function.

The function [math]\displaystyle{ s_m^n }[/math] is designed to mimic the behavior of [math]\displaystyle{ \phi(x,y) }[/math] when given the appropriate parameters. Essentially, by selecting the right values for [math]\displaystyle{ m }[/math] and [math]\displaystyle{ n }[/math], you can make [math]\displaystyle{ s }[/math] behave like for a specific computation. Instead of dealing with the complexity of [math]\displaystyle{ \phi(x,y) }[/math], we can work with a simpler [math]\displaystyle{ s_m^n }[/math] that captures the essence of the computation.

Details

The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering [math]\displaystyle{ \varphi }[/math] of recursive functions, there is a primitive recursive function 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 [math]\displaystyle{ \varphi_{s(p, x)}(y) }[/math] and [math]\displaystyle{ f(x, y) }[/math] 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 extensional equality of functions holds for every x:

[math]\displaystyle{ \varphi_{s(p, x)} \simeq \lambda y.\varphi_p(x, y). }[/math]

More generally, for any m, n > 0, there exists a primitive recursive function [math]\displaystyle{ S^m_n }[/math] 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 x₁, …, x_m:

[math]\displaystyle{ \varphi_{S^m_n(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). }[/math]

The function s described above can be taken to be [math]\displaystyle{ S^1_1 }[/math].

Formal statement

Given arities m and n, for every Turing Machine [math]\displaystyle{ \text{TM}_x }[/math] of arity [math]\displaystyle{ m + n }[/math] and for all possible values of inputs [math]\displaystyle{ y_1, \dots, y_m }[/math], there exists a Turing machine [math]\displaystyle{ \text{TM}_k }[/math] of arity n, such that

[math]\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). }[/math]

Furthermore, there is a Turing machine S that allows k to be calculated from x and y; it is denoted [math]\displaystyle{ k = S_n^m(x, y_1, \dots, y_m) }[/math].

Informally, S finds the Turing Machine [math]\displaystyle{ \text{TM}_k }[/math] that is the result of hardcoding the values of y into [math]\displaystyle{ \text{TM}_x }[/math]. The result generalizes to any Turing-complete computing model.

This can also be extended to total computable functions as follows:

Given a total computable function [math]\displaystyle{ s_{m,n}: \mathbb{N}^{m+1} \rightarrow \mathbb{N} }[/math] and [math]\displaystyle{ m,n \geq 1 }[/math] such that [math]\displaystyle{ \forall \vec{x} \in \mathbb{N}^m, \forall \vec{y} \in \mathbb{N}^n }[/math], [math]\displaystyle{ \forall e \in \mathbb{N} }[/math]:

[math]\displaystyle{ \phi_{e}^{m+n}(\vec{x}, \vec{y})=\phi^{n}_{s_{m,n}{(e, \vec{x})}}(\vec{y}) }[/math]

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 [math]\displaystyle{ f:\mathbb{N}^{n+m} \rightarrow \mathbb{N} }[/math] be a computable function. There, there is a total computable function [math]\displaystyle{ s: \mathbb{N}^{m} \rightarrow \mathbb{N} }[/math] such that [math]\displaystyle{ \forall x \in \mathbb{N}^m }[/math], [math]\displaystyle{ \vec{y} \in \mathbb{N}^n }[/math]:

[math]\displaystyle{ f(\vec{x}, \vec{y})=\phi^{(n)}_{S(\vec{x})}(\vec{y}) }[/math]

Example

The following Lisp code implements s₁₁ 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)).

See also

• Currying
• Kleene's recursion theorem
• Partial evaluation

References

• Kleene, S. C. (1936). "General recursive functions of natural numbers". Mathematische Annalen 112 (1): 727–742. doi:10.1007/BF01565439. http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=PPN235181684_0112&DMDID=DMDLOG_0043&L=1. 
• Kleene, S. C. (1938). "On Notations for Ordinal Numbers". The Journal of Symbolic Logic 3: 150–155. doi:10.2307/2267778. http://www.thatmarcusfamily.org/philosophy/Course_Websites/Readings/Kleene%20-%20Ordinals.pdf.  (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the [math]\displaystyle{ S^m_n }[/math] theorem.)
• Nies, A. (2009). Computability and randomness. Oxford Logic Guides. 51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1. 
• Odifreddi, P. (1999). Classical Recursion Theory. North-Holland. ISBN 0-444-87295-7. https://archive.org/details/classicalrecursi0000odif. 
• Rogers, H. (1987). The Theory of Recursive Functions and Effective Computability. First MIT press paperback edition. ISBN 0-262-68052-1. 
• Soare, R. (1987). Recursively enumerable sets and degrees. Perspectives in Mathematical Logic. Springer-Verlag. ISBN 3-540-15299-7. 

External links

• Weisstein, Eric W.. "Kleene's s-m-n Theorem". http://mathworld.wolfram.com/Kleeness-m-nTheorem.html.