Teorema Smn

Na teoria da computabilidade, o teorema S_mn (também chamado de lema da tradução, teorema do parâmetro ou teorema da parametrização), é um resultado básico sobre linguagens de programação (e, mais genericamente, numerações de Gödel das funções computáveis) (Soare 1987, Rogers 1967). Foi primeiramente provado por Stephen Cole Kleene (Kleene 1943).

Em termos práticos, o teorema diz que para uma dada linguagem de programação e inteiros positivos ${\displaystyle m}$ e ${\displaystyle n}$', existe um algoritmo específico que aceita como entrada o código fonte do programa com ${\displaystyle m+n}$ variáveis livres, juntamente com ${\displaystyle m}$ valores. Esse algoritmo gera um código fonte que substitui efetivamente os valores para as primeiras ${\displaystyle m}$ variáveis livres, deixando o resto livre.

A forma básica do teorema se aplica a funções de dois argumentos (Nies 2009, p. 6). Dada uma numeração de Gödel ${\displaystyle \varphi }$ de funções recursivas, há um função recursiva primitiva ${\displaystyle s}$ de dois argumentos com a seguinte propriedade: para cada número de Gödel ${\displaystyle p}$ de uma função computável parcial ${\displaystyle f}$ com dois argumentos, as expressões ${\displaystyle \varphi _{s(p,x)}(y)}$ e ${\displaystyle f(x,y)}$ são definidas para as mesmas combinações de números naturais ${\displaystyle x}$ e ${\displaystyle y}$ e seus valores são iguais para qualquer combinação. Em outras palavras, a seguinte igualdade extensional de funções detém para cada ${\displaystyle x}$:

${\displaystyle \varphi _{s(p,x)}\simeq \lambda y.\varphi _{p}(x,y)}$

De forma mais genérica, para cada ${\displaystyle m,n>0}$, existe uma função recursiva primitiva ${\displaystyle s_{m}^{n}}$ de ${\displaystyle m+1}$ argumentos que funciona da seguinte maneira: para cada número de Gödel ${\displaystyle p}$ de uma função computável parcial com ${\displaystyle m+n}$ argumentos, e todos os valores de ${\displaystyle x_{1},\cdots ,x_{m}:}$

${\displaystyle \varphi _{s_{n}^{m}(p,x_{1},...,x_{m})}\simeq \lambda y_{1},...,y_{n}.\varphi _{p}(x_{1},...,x_{m},y_{1},...,y_{1})}$

A função s descrita acima pode ser tida como sendo ${\displaystyle s_{1}^{1}}$.

O seguinte código implementa s11 para Lisp.

(defun s11 (f x))
    (let ((y (gensym))))
        (list 'lamba (list y) (list f x y))

Por exemplo,

(s11 '(lamba(x y) (+ x y)) 3)

avalia para

(lambda (g42) ((lambda (x y) (+ x y)) 3 g42))

• Teorema da recursividade de Kleene
• Currying

• Kleene, S. C. (1936). "General recursive functions of natural numbers". Mathematische Annalen 112 (1): 727–742. doi:10.1007/BF01565439.
• Stephen Cole Kleen (1938). "On Notations for Ordinal Numbers" (PDF). The Journal of Simbolyc Logic 3: 150-155. (This is the reference that the 1989 edition of Odifreddi's "Classical Recursion Theory" gives on p. 131 for the s_mn theorem.)
• Nies, André (2009). Computability and randomness. Oxford Logic Guides 51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1 Zbl [1]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.

• Weisstein, Eric W.,  [2]"Kleene's s-m-n Theorem", MathWorld.