Smn theorem

Template:Correct title 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 partial computable functions) (Soare 1987, Rogers 1967). It was first proved by Stephen Cole Kleene (1943). The name $S_m^n$ 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 in essence 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 $\phi$ of partial computable functions, there is a primitive recursive function $s$ of two arguments with the following property: for every Gödel number $e$ of a partial computable function $f$ with two arguments, the expressions ${\phi }_{s(e,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(e,x)}\simeq \lambda y.{\phi }_e(x,y).$

More generally, for any $m,n>0$, there exists a primitive recursive function $S_n^m$ of $m+1$ arguments that behaves as follows: for every Gödel number $e$ of a partial computable function with $m+n$ arguments, and all values of $x_1,x_2,\mathrm{...},x_m$:

${\phi }_{S_n^m(e,x_1,\dots ,x_m)}\simeq \lambda y_1,\dots ,y_n.{\phi }_e(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 $m$ and $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 $n$, 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 $S$ that allows $k$ to be calculated from $x$ and $y$; it is denoted $k=S_n^m(x,y_1,\dots ,y_m)$.

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

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, where Template:Code is a "fresh" symbol.

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