smn theorem

{{short description|On transforming a program by substituting constants for free variables}}

In computability theory the {{subsup|S|n|m}} 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 {{subsup|S|n|m}} 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 {{math|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 $g(x,y)$ which is computable, there exists a total and computable function such that $\phi_s(x)(y)=g(x,y)$ basically "fixing" the first argument of $g$ . It's like partially applying an argument to a function. This is generalized over $m,n$ tuples for $x,y$ . In other words, it addresses the idea of "parameterization" 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 $s_m^n$ is designed to mimic the behavior of $\phi(x,y)$ when given the appropriate parameters. Essentially, by selecting the right values for $m$ and $n$ , you can make $s$ behave like for a specific computation. Instead of dealing with the complexity of $\phi(x,y)$ , we can work with a simpler $s_m^n$ 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 $\varphi$ 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 $\varphi_{s(p, x)}(y)$ and $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 extensional equality of functions holds for every x:

: $\varphi_{s(p, x)} \simeq \lambda y.\varphi_p(x, y).$

More generally, for any m, {{math|n > 0}}, there exists a primitive recursive function $S^m_n$ of {{math|m + 1}} arguments that behaves as follows: for every Gödel number p of a partial computable function with {{math|m + n}} arguments, and all values of x₁, …, x_m:

: $\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).$

The function s described above can be taken to be $S^1_1$ .

Formal statement

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

: $\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 {{mvar|S}} that allows {{mvar|k}} to be calculated from {{mvar|x}} and {{mvar|y}}; it is denoted $k = S_n^m(x, y_1, \dots, y_m)$ .

Informally, {{mvar|S}} finds the Turing Machine $\text{TM}_k$ that is the result of hardcoding the values of {{mvar|y}} into $\text{TM}_x$ . 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 $s_{m,n}: \mathbb{N}^{m+1} \rightarrow \mathbb{N}$ and $m,n \geq 1$ such that $\forall \vec{x} \in \mathbb{N}^m, \forall \vec{y} \in \mathbb{N}^n$ , $\forall e \in \mathbb{N}$ :

$\phi_{e}^{m+n}(\vec{x}, \vec{y})=\phi^{n}_{s_{m,n}{(e, \vec{x})}}(\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:\mathbb{N}^{n+m} \rightarrow \mathbb{N}$ be a computable function. There, there is a total computable function $s: \mathbb{N}^{m} \rightarrow \mathbb{N}$ such that $\forall x \in \mathbb{N}^m$ , $\vec{y} \in \mathbb{N}^n$ :

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

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, {{code|lang=lisp|(s11 '(lambda (x y) (+ x y)) 3)}} evaluates to {{code|lang=lisp|(lambda (g42) ((lambda (x y) (+ x y)) 3 g42))}}.

References

{{cite journal | doi = 10.1007/BF01565439 | last1 = Kleene| first1 = S. C. | title = General recursive functions of natural numbers | journal = Mathematische Annalen | volume = 112 | issue = 1 | pages = 727–742 | year = 1936 | s2cid = 120517999| url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=PPN235181684_0112&DMDID=DMDLOG_0043&L=1 }}
{{cite journal| last1 = Kleene| first1 = S. C. | title=On Notations for Ordinal Numbers| journal=The Journal of Symbolic Logic| year=1938| volume=3| issue = 4 | pages=150–155| doi = 10.2307/2267778 | jstor = 2267778 | s2cid = 34314018 | url=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 $S^m_n$ theorem.)
{{cite book | last=Nies | first=A. | title=Computability and randomness | series=Oxford Logic Guides | volume=51 | location=Oxford | publisher=Oxford University Press | year=2009 | isbn=978-0-19-923076-1 | zbl=1169.03034 }}
{{cite book | author = Odifreddi, P. | title = Classical Recursion Theory | publisher = North-Holland | year = 1999 | isbn = 0-444-87295-7 | url-access = registration | url = https://archive.org/details/classicalrecursi0000odif }}
{{cite book | author = Rogers, H. | title = The Theory of Recursive Functions and Effective Computability | publisher = First MIT press paperback edition | year = 1987 | orig-year=1967 |isbn = 0-262-68052-1 }}
{{cite book | author = Soare, R.| title = Recursively enumerable sets and degrees | series = Perspectives in Mathematical Logic | publisher = Springer-Verlag | year = 1987 | isbn = 3-540-15299-7 }}

External links

{{mathworld|urlname=Kleeness-m-nTheorem|title=Kleene's s-m-n Theorem}}

Category:Computability theory

Category:Theorems in theory of computation

Category:Articles with example Lisp (programming language) code