Sm n theorem

Sm n theorem In computability theory the 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 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 effectively substitutes the values for the first m free variables, leaving the rest of the variables free.

Contents 1 Details 2 Formal statement 3 Example 4 See also 5 References 6 External links 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 m, n > 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 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.

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 Currying Kleene's recursion theorem Partial evaluation References Kleene, S. C. (1936). "General recursive functions of natural numbers". Mathematische Annalen. 112 (1): 727–742. doi:10.1007/BF01565439. Kleene, S. C. (1938). "On Notations for Ordinal Numbers" (PDF). The Journal of Symbolic Logic. 3: 150–155. (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the {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. External links Weisstein, Eric W. "Kleene's s-m-n Theorem". MathWorld. Categories: Computability theoryTheorems in theory of computationArticles with example Lisp (programming language) code