In computability theory the S mn 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 S mn 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 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 ) {\displaystyle g(x,y)} which is computable, there exists a total and computable function such that ϕ s ( x ) ( y ) = g ( x , y ) {\displaystyle \phi _{s}(x)(y)=g(x,y)} basically "fixing" the first argument of g {\displaystyle g} . It's like partially applying an argument to a function. This is generalized over m , n {\displaystyle m,n} tuples for x , y {\displaystyle x,y} . In other words, it addresses the idea of "parameterization" 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 {\displaystyle s_{m}^{n}} is designed to mimic the behavior of ϕ ( x , y ) {\displaystyle \phi (x,y)} when given the appropriate parameters. Essentially, by selecting the right values for m {\displaystyle m} and n {\displaystyle n} , you can make s {\displaystyle s} behave like for a specific computation. Instead of dealing with the complexity of ϕ ( x , y ) {\displaystyle \phi (x,y)} , we can work with a simpler s m n {\displaystyle 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 φ {\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 φ s ( p , x ) ( y ) {\displaystyle \varphi _{s(p,x)}(y)} and f ( x , y ) {\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:
φ s ( p , x ) ≃ λ y . φ p ( x , y ) . {\displaystyle \varphi _{s(p,x)}\simeq \lambda y.\varphi _{p}(x,y).}More generally, for any m, n > 0, there exists a primitive recursive function S n m {\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:
φ S n m ( p , x 1 , … , x m ) ≃ λ y 1 , … , y n . φ p ( x 1 , … , x m , y 1 , … , y n ) . {\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 S 1 1 {\displaystyle S_{1}^{1}} .
Formal statement
Given arities m and n, for every Turing Machine TM x {\displaystyle {\text{TM}}_{x}} of arity m + n {\displaystyle m+n} and for all possible values of inputs y 1 , … , y m {\displaystyle y_{1},\dots ,y_{m}} , there exists a Turing machine TM k {\displaystyle {\text{TM}}_{k}} of arity n, such that
∀ z 1 , … , z n : TM x ( y 1 , … , y m , z 1 , … , z n ) = TM k ( z 1 , … , z n ) . {\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 S that allows k to be calculated from x and y; it is denoted k = S n m ( x , y 1 , … , y m ) {\displaystyle k=S_{n}^{m}(x,y_{1},\dots ,y_{m})} .
Informally, S finds the Turing Machine TM k {\displaystyle {\text{TM}}_{k}} that is the result of hardcoding the values of y into TM x {\displaystyle {\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 : N m + 1 → N {\displaystyle s_{m,n}:\mathbb {N} ^{m+1}\rightarrow \mathbb {N} } and m , n ≥ 1 {\displaystyle m,n\geq 1} such that ∀ x → ∈ N m , ∀ y → ∈ N n {\displaystyle \forall {\vec {x}}\in \mathbb {N} ^{m},\forall {\vec {y}}\in \mathbb {N} ^{n}} , ∀ e ∈ N {\displaystyle \forall e\in \mathbb {N} } :
ϕ e m + n ( x → , y → ) = ϕ s m , n ( e , x → ) n ( y → ) {\displaystyle \phi _{e}^{m+n}({\vec {x}},{\vec {y}})=\phi _{s_{m,n}{(e,{\vec {x}})}}^{n}({\vec {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 : N n + m → N {\displaystyle f:\mathbb {N} ^{n+m}\rightarrow \mathbb {N} } be a computable function. There, there is a total computable function s : N m → N {\displaystyle s:\mathbb {N} ^{m}\rightarrow \mathbb {N} } such that ∀ x ∈ N m {\displaystyle \forall x\in \mathbb {N} ^{m}} , y → ∈ N n {\displaystyle {\vec {y}}\in \mathbb {N} ^{n}} :
f ( x → , y → ) = ϕ S ( x → ) ( n ) ( y → ) {\displaystyle f({\vec {x}},{\vec {y}})=\phi _{S({\vec {x}})}^{(n)}({\vec {y}})}
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)).
See also
- Kleene, S. C. (1936). "General recursive functions of natural numbers". Mathematische Annalen. 112 (1): 727–742. doi:10.1007/BF01565439. S2CID 120517999.
- Kleene, S. C. (1938). "On Notations for Ordinal Numbers" (PDF). The Journal of Symbolic Logic. 3 (4): 150–155. doi:10.2307/2267778. JSTOR 2267778. S2CID 34314018. (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the S n m {\displaystyle S_{n}^{m}} theorem.)
- Nies, A. (2009). Computability and randomness. Oxford Logic Guides. Vol. 51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1. Zbl 1169.03034.
- Odifreddi, P. (1999). Classical Recursion Theory. North-Holland. ISBN 0-444-87295-7.
- Rogers, H. (1987) [1967]. The Theory of Recursive Functions and Effective Computability. First MIT press paperback edition. ISBN 0-262-68052-1.
- Soare, R. (1987). Recursively enumerable sets and degrees. Perspectives in Mathematical Logic. Springer-Verlag. ISBN 3-540-15299-7.