smn theorem

In computability theory the s_mn 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 "s_mn" comes from the occurrence of a 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.

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, n > 0, there exists a primitive recursive function $s^m_n$ 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:

\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

For all arities $m$ and $n$ ,

For every Turing Machine ${\rm {TM}}_{x}$ of arity $m + n$ , and for all possible values of inputs $y_{1}\dots y_{m}$ ,

there exists a Turing Machine ${\rm {TM}}_{k}$ of arity $n$ , such that

\forall z_{1}\dots z_{n}~:~{\rm {TM}}_{x}(y_{1}\dots y_{m},~z_{1}\dots z_{n})={\rm {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}\dots y_{m})$ .

Futhermore, the result generalizes to any Turing Complete computing model.

Informally, $s$ finds the Turing Machine ${\rm {TM}}_{k}$ which is the result of hardcoding the values of $y$ into ${\rm {TM}}_{x}$ .

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)).

References

Kleene, S. C. (1936). "General recursive functions of natural numbers". Mathematische Annalen. 112 (1): 727–742. doi:10.1007/BF01565439.
Kleene, S. C. (1938). "On Notations for Ordinal Numbers" (PDF). The Journal of Symbolic Logic. 3: 150–155. (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the s_mn theorem.)
Nies, A. (2009). Computability and randomness. Oxford Logic Guides. 51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1. Zbl 1169.03034.
Odifreddi, P. (1999). Classical Recursion Theory. North-Holland. ISBN 0-444-87295-7.
Rogers, H. (1987) [1967]. 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". MathWorld.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.