Smn theorem

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 Template:Math 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 ${\varphi }_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_m^n$ is designed to mimic the behavior of $\varphi (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 $\varphi (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 $\phi$ 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 ${\phi }_{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:

${\phi }_{s(p,x)}\simeq \lambda y.{\phi }_p(x,y).$

More generally, for any m, Template:Math, there exists a primitive recursive function $S_n^m$ of Template:Math arguments that behaves as follows: for every Gödel number p of a partial computable function with Template:Math arguments, and all values of x₁, …, x_m:

${\phi }_{S_n^m(p,x_1,\dots ,x_m)}\simeq \lambda y_1,\dots ,y_n.{\phi }_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 Template:Mvar and Template:Mvar, 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 Template:Mvar, such that

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

Informally, Template:Mvar finds the Turing Machine ${\text{TM}}_k$ that is the result of hardcoding the values of Template:Mvar 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}\to \mathbb{N}$ and $m,n\ge 1$ such that $\mathrm{\forall }\overrightarrow{x}\in {\mathbb{N}}^m,\mathrm{\forall }\overrightarrow{y}\in {\mathbb{N}}^n$, $\mathrm{\forall }e\in \mathbb{N}$:

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

$f(\overrightarrow{x},\overrightarrow{y})={\varphi }_{S(\overrightarrow{x})}^{(n)}(\overrightarrow{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, Template:Code evaluates to Template:Code.

See also

• Currying
• Kleene's recursion theorem
• Partial evaluation

References

• Template:Cite journal
• Template:Cite journal (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the $S_n^m$ theorem.)
• Template:Cite book
• Template:Cite book
• Template:Cite book
• Template:Cite book

External links

• Template:Mathworld