Teorema Smn

Teorema

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

Detalhes

editar

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   de dois argumentos com a seguinte propriedade: para cada número de Gödel   de uma função computável parcial   com dois argumentos, as expressões   e   são definidas para as mesmas combinações de números naturais   e   e seus valores são iguais para qualquer combinação. Em outras palavras, a seguinte igualdade extensional de funções detém para cada  :

 

De forma mais genérica, para cada  , existe uma função recursiva primitiva   de   argumentos que funciona da seguinte maneira: para cada número de Gödel   de uma função computável parcial com   argumentos, e todos os valores de  

 

A função s descrita acima pode ser tida como sendo  .

Exemplos

editar

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

editar

Referências

editar

Ligações externas

editar