Smn theorem

In computability theory the S m
n  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 ${\displaystyle S_{m}^{n}}$ comes from the occurrence of an ${\displaystyle S}$ with subscript ${\displaystyle n}$ and superscript ${\displaystyle 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 ${\displaystyle m}$ and ${\displaystyle n}$, there exists a particular algorithm that accepts as input the source code of a program with ${\displaystyle m+n}$ free variables, together with ${\displaystyle m}$ values. This algorithm generates source code that in essence substitutes the values for the first ${\displaystyle m}$ free variables, leaving the rest of the variables free.

The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering ${\displaystyle \varphi }$ of partial computable functions, there is a primitive recursive function ${\displaystyle s}$ of two arguments with the following property: for every Gödel number ${\displaystyle e}$ of a partial computable function ${\displaystyle f}$ with two arguments, the expressions ${\displaystyle \varphi _{s(e,x)}(y)}$ and ${\displaystyle f(x,y)}$ are defined for the same combinations of natural numbers ${\displaystyle x}$ and ${\displaystyle y}$, and their values are equal for any such combination. In other words, the following extensional equality of functions holds for every ${\displaystyle x}$:

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

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

${\displaystyle \varphi _{S_{n}^{m}(e,x_{1},\dots ,x_{m})}\simeq \lambda y_{1},\dots ,y_{n}.\varphi _{e}(x_{1},\dots ,x_{m},y_{1},\dots ,y_{n}).}$

The function ${\displaystyle s}$ described above can be taken to be ${\displaystyle S_{1}^{1}}$.

Given arities ${\displaystyle m}$ and ${\displaystyle n}$, for every Turing Machine ${\displaystyle {\text{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 {\text{TM}}_{k}}$ of arity ${\displaystyle n}$, such that

${\displaystyle \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 ${\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})}$.

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

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)), where g42 is a "fresh" symbol.