# smn theorem

In computability theory the smn 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 "smn" 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 ${\displaystyle \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 ${\displaystyle \varphi _{s(p,x)}(y)}$ and ${\displaystyle 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:

${\displaystyle \varphi _{s(p,x)}\simeq \lambda y.\varphi _{p}(x,y).\,}$

More generally, for any mn > 0, there exists a primitive recursive function ${\displaystyle s_{n}^{m}}$ 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 x1,…,xm:

${\displaystyle \varphi _{s_{n}^{m}(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 ${\displaystyle s_{1}^{1}}$.

## Formal Statement

For all arities ${\displaystyle m}$ and ${\displaystyle n}$,

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

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

${\displaystyle \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 ${\displaystyle s}$ that allows ${\displaystyle k}$ to be calculated from ${\displaystyle x}$ and ${\displaystyle y}$; it is denoted ${\displaystyle k=s_{n}^{m}(x,y_{1}\dots y_{m})}$.

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

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

## Example

The following Lisp code implements s11 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)).