The Smn theorem, also known as the iteration theorem, was first proved by Stephen Cole Kleene, and provides the theoretical justification for use of currying functions (or partial evaluation) in the lambda calculus, here presented in terms of Turing machines. It basically states that if we have some a Turing machine that computes some partial recursive function of m + n variables, we can effectively construct another Turing machine that holds m of these variables fixed, so when n more variables are applied, the value of the original function can be calculated.

Formally, the Smn theorem states that for every m, n ≥ 1, there exists a total recursive function Smn : Nm+1N, such that for some Turing machine description number e that denotes a TM calculating a partial recursive function of m+n variables, we have:

φSmn(e, x1, ... xm)(xm+1, ... xm+n) = φe(x1, ..., xm+n)

where φe denotes the TM with description number e.

An important corollary of the Smn theorem states that for every partial recursive function ψ(e, x) there exists a total recursive function f such that φf(e)(x) = ψ(e, x).

Log in or register to write something here or to contact authors.