In computability theory the smn theorem, (also called the translation lemma, parameter theorem, or 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 (Kleene 1943). The name "smn" comes from the occurrence of a s with subscript n and superscript m in the original formulation of the theorem (see below).
Contents
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 free.
Details
The basic form of the theorem applies to functions of two arguments (Nies 2009, p. 6). Given a Gödel numbering
More generally, for any m, n > 0, there exists a primitive recursive function
The function s described above can be taken to be
Example
The following Lisp code implements s11 for Lisp.
For example, (s11 '(lambda (x y) (+ x y)) 3)
evaluates to (lambda (g42) ((lambda (x y) (+ x y)) 3 g42))
.