Jump to content

Smn theorem

From Wikipedia, the free encyclopedia
(Redirected from Parameterization 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 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.

The smn-theorem states that given a function of two arguments which is computable, there exists a total and computable function such that basically "fixing" the first argument of . It's like partially applying an argument to a function. This is generalized over tuples for . In other words,it addresses the idea of "parametrization" 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 is designed to mimic the behavior of when given the appropriate parameters. Essentially, by selecting the right values for and , you can make behave like for a specific computation. Instead of dealing with the complexity of , we can work with a simpler that captures the essence of the computation.

Details

[edit]

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

More generally, for any m, n > 0, there exists a primitive recursive function 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:

The function s described above can be taken to be .

Formal statement

[edit]

Given arities m and n, for every Turing Machine of arity and for all possible values of inputs , there exists a Turing machine of arity n, such that

Furthermore, there is a Turing machine S that allows k to be calculated from x and y; it is denoted .

Informally, S finds the Turing Machine that is the result of hardcoding the values of y into . 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 and such that , :

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 be a computable function. There, there is a total computable function such that , :

Example

[edit]

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

[edit]

References

[edit]
  • 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: 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 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.
[edit]