Teorema Smn

Fonte: testwiki
Saltar para a navegação Saltar para a pesquisa

Na teoria da computabilidade, o teorema Smn (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 m e n', existe um algoritmo específico que aceita como entrada o código fonte do programa com m+n variáveis livres, juntamente com m valores. Esse algoritmo gera um código fonte que substitui efetivamente os valores para as primeiras m variáveis livres, deixando o resto livre.

Detalhes

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 φ de funções recursivas, há um função recursiva primitiva s de dois argumentos com a seguinte propriedade: para cada número de Gödel p de uma função computável parcial f com dois argumentos, as expressões φs(p,x)(y) e f(x,y) são definidas para as mesmas combinações de números naturais x e 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 x:Predefinição:QuoteDe forma mais genérica, para cada m,n>0, existe uma função recursiva primitiva smn de m+1 argumentos que funciona da seguinte maneira: para cada número de Gödel p de uma função computável parcial com m+n argumentos, e todos os valores de x1,,xm:Predefinição:QuoteA função s descrita acima pode ser tida como sendo s11.

Exemplos

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))

Veja também

Referências

Ligações externas