Smn theorem explained

In computability theory the 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 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 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 "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

s ^{n} _{m} 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 ^{n} _{m} 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,} (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,} \simeq λ y.\varphi _{p(x,} y).

More generally, for any m,, there exists a primitive recursive function

S ^{m} _{n} of arguments that behaves as follows: for every Gödel number p of a partial computable function with arguments, and all values of x₁, …, x_m:\varphi _{S ^{m} _{n(p,} x _{1,} ... , x _{m)}} \simeq λ y _{1,} ... , y _{n.\varphi} _{p(x} _{1,} ... , x _{m,} y _{1,} ... , y _{n).}

The function s described above can be taken to be

S ^{1} _{1} .

Formal statement

Given arities and, for every Turing Machine

TM _{x} of arity m + n and for all possible values of inputs y _{1,} ... , y _{m} , there exists a Turing machine TM _{k} of arity, such that\forall z _{1,} ... , z _{n} : TM _{x(y} _{1,} ... , y _{m,} z _{1,} ... , z _{n)} = TM _{k(z} _{1,} ... , z _{n).}

Furthermore, there is a Turing machine that allows to be calculated from and ; it is denoted

k = S ^{m(x,} _{n} y _{1,} ... , y _{m)} .

Informally, finds the Turing Machine

TM _{k} that is the result of hardcoding the values of into 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} : N ^{m+1} → N and m,n \geq 1 such that \forall \vec{x} \in N ^{m,} \forall \vec{y} \in N ^{n} , \forall e \in N :\phi ^{m + n} _{e} (\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: N ^{n+m} → N be a computable function. There, there is a total computable function s: N ^{m} → N such that \forall x \in N ^{m} , \vec{y} \in 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, evaluates to .

See also

• Currying
• Kleene's recursion theorem
• Partial evaluation

References

• 10.1007/BF01565439 . Kleene. S. C. . General recursive functions of natural numbers . Mathematische Annalen . 112 . 1 . 727–742 . 1936 . 120517999.
• Kleene. S. C. . On Notations for Ordinal Numbers. The Journal of Symbolic Logic. 1938. 3. 150–155. 10.2307/2267778 . 2267778 . 34314018 . (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the

S ^{m} _{n} theorem.)

• Book: Nies, A. . Computability and randomness . Oxford Logic Guides . 51 . Oxford . Oxford University Press . 2009 . 978-0-19-923076-1 . 1169.03034 .
• Book: Odifreddi, P. . Classical Recursion Theory . North-Holland . 1999 . 0-444-87295-7 . registration .
• Book: Rogers, H. . The Theory of Recursive Functions and Effective Computability . First MIT press paperback edition . 1987 . 1967 . 0-262-68052-1 .
• Book: Soare, R.. Recursively enumerable sets and degrees . Perspectives in Mathematical Logic . Springer-Verlag . 1987 . 3-540-15299-7 .