In
computability theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ex ...
the ' 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 language
A programming language is a system of notation for writing computer programs.
Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
s (and, more generally,
Gödel numbering
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. Kurt Gödel developed the concept for the proof of his incom ...
s of the
computable function
Computable functions are the basic objects of study in computability theory. Informally, a function is ''computable'' if there is an algorithm that computes the value of the function for every value of its argument. Because of the lack of a precis ...
s) (Soare 1987, Rogers 1967). It was first proved by
Stephen Cole Kleene
Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
(1943). The name ' 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
In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...
that accepts as input the
source code
In computing, source code, or simply code or source, is a plain text computer program written in a programming language. A programmer writes the human readable source code to control the behavior of a computer.
Since a computer, at base, only ...
of a program with
free variables
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a variable may be said to be either free or bound. Some older books use the terms real variable and apparent variable for f ...
, 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
Computability is the ability to solve a problem by an effective procedure. It is a key topic of the field of computability theory within mathematical logic and the theory of computation within computer science. The computability of a problem is cl ...
, there exists a
total
Total may refer to:
Mathematics
* Total, the summation of a set of numbers
* Total order, a partial order without incomparable pairs
* Total relation, which may also mean
** connected relation (a binary relation in which any two elements are comp ...
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 "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
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
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
In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
''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'', , there exists a primitive recursive function
of arguments that behaves as follows: for every Gödel number ''p'' of a partial computable function with arguments, and all values of ''x''
1, …, ''x''
''m'':
:
The function ''s'' described above can be taken to be
.
Formal statement
Given arities and , for every Turing Machine
of arity
and for all possible values of inputs
, there exists a Turing machine
of arity , such that
:
Furthermore, there is a Turing machine that allows to be calculated from and ; it is denoted
.
Informally, finds the Turing Machine
that is the result of hardcoding the values of into
. The result generalizes to any
Turing-complete
In computability theory, a system of data-manipulation rules (such as a model of computation, a computer's instruction set, a programming language, or a cellular automaton) is said to be Turing-complete or computationally universal if it can be ...
computing model.
This can also be extended to
total
Total may refer to:
Mathematics
* Total, the summation of a set of numbers
* Total order, a partial order without incomparable pairs
* Total relation, which may also mean
** connected relation (a binary relation in which any two elements are comp ...
computable functions as follows:
Given a total computable function
and
such that
,
:
There is also a simplified smn-theorem, which uses a total computable function as index as follows:
Let
be a computable function. There, there is a total computable function
such that
,
:
Example
The following
Lisp
Lisp (historically LISP, an abbreviation of "list processing") is a family of programming languages with a long history and a distinctive, fully parenthesized Polish notation#Explanation, prefix notation.
Originally specified in the late 1950s, ...
code implements s
11 for Lisp.
(defun s11 (f x)
(let ((y (gensym)))
(list 'lambda (list y) (list f x y))))
For example, evaluates to .
See also
*
Currying
In mathematics and computer science, currying is the technique of translating a function that takes multiple arguments into a sequence of families of functions, each taking a single argument.
In the prototypical example, one begins with a functi ...
*
Kleene's recursion theorem
In computability theory, Kleene's recursion theorems are a pair of fundamental results about the application of computable functions to their own descriptions. The theorems were first proved by Stephen Kleene in 1938 and appear in his 1952 ...
*
Partial evaluation
In computing, partial evaluation is a technique for several different types of program optimization by specialization. The most straightforward application is to produce new programs that run faster than the originals while being guaranteed to ...
References
*
* (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the
theorem.)
*
*
*
*
External links
*{{mathworld, urlname=Kleeness-m-nTheorem, title=Kleene's ''s''-''m''-''n'' Theorem
Computability theory
Theorems in theory of computation
Articles with example Lisp (programming language) code