Encyclopedia

Smn theorem

On transforming a program by substituting constants for free variables

Wikipedia contributorsAdapted for Fathomly · View authors

2 min read
Source updated June 7, 2026

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 $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.

01Details

The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering $\varphi$ 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 $\varphi _{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$ :

$\varphi _{s(e,x)}\simeq \lambda y.\varphi _{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},...,x_{m}$ :

$\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 $s$ described above can be taken to be $S_{1}^{1}$ .

02Formal 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

$\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.

03Example

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.

Watch videos about Smn theoremExplainers and documentaries on YouTube (opens in a new tab)

Sources and credits

This article is adapted from the Wikipedia article “Smn theorem”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.

Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.

Smn theorem

01Details

02Formal statement

03Example

Sources and credits

Related topics

Currying

Kleene's recursion theorem

Partial evaluation