Smn theorem

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 , there exists a primitive recursive function S^m_n of arguments that behaves as follows: for every Gödel number e of a partial computable function with arguments, and all values of x1, …, xm: : \varphi_{S^m_n(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. ==Formal statement==

Given arities and , 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 , 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 that allows to be calculated from and ; it is denoted k = S_n^m(x, y_1, \dots, y_m). Informally, finds the Turing Machine \text{TM}_k that is the result of hardcoding the values of into \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, evaluates to , where is a "fresh" symbol. ==See also==