Teorema de recursão de Kleene - Kleene's recursion theorem

Na teoria da computabilidade , os teoremas de recursão de Kleene são um par de resultados fundamentais sobre a aplicação de funções computáveis às suas próprias descrições. Os teoremas foram provados pela primeira vez por Stephen Kleene em 1938 e aparecem em seu livro de 1952, Introdução à Metamatemática . Um teorema relacionado, que constrói pontos fixos de uma função computável, é conhecido como teorema de Rogers e é devido a Hartley Rogers, Jr ..

Os teoremas de recursão podem ser aplicados para construir pontos fixos de certas operações em funções computáveis , para gerar quines e para construir funções definidas por meio de definições recursivas .

Notação

O enunciado dos teoremas refere-se a uma numeração admissível das funções recursivas parciais , de modo que a função correspondente ao índice seja . ${\ displaystyle \ varphi}$${\ displaystyle e}$${\ displaystyle \ varphi _ {e}}$

Se e forem funções parciais nos números naturais, a notação indica que, para cada n , e são ambos definidos e iguais, ou então e são ambos indefinidos. ${\ displaystyle F}$${\ displaystyle G}$${\ displaystyle F \ simeq G}$${\ displaystyle F (n)}$${\ displaystyle G (n)}$${\ displaystyle F (n)}$${\ displaystyle G (n)}$

Teorema do ponto fixo de Rogers

Dada uma função , um ponto fixo de é um índice tal que . Rogers descreve o seguinte resultado como "uma versão mais simples" do teorema da recursão de Kleene (segundo). ${\ displaystyle F}$${\ displaystyle F}$${\ displaystyle e}$${\ displaystyle \ varphi _ {e} \ simeq \ varphi _ {F (e)}}$

Teorema do ponto fixo de Rogers . Se for uma função computável total, ela tem um ponto fixo.${\ displaystyle F}$

Prova do teorema do ponto fixo

A prova usa uma função computável total particular , definida como segue. Dado um número natural , a função produz o índice da função computável parcial que realiza o seguinte cálculo: ${\ displaystyle h}$${\ displaystyle x}$${\ displaystyle h}$

Dada uma entrada , primeiro tente calcular . Se esse cálculo retornar uma saída , calcule e retorne seu valor, se houver.${\ displaystyle y}$${\ displaystyle \ varphi _ {x} (x)}$${\ displaystyle e}$${\ displaystyle \ varphi _ {e} (y)}$

Assim, para todos os índices de funções computáveis ​​parciais, se for definido, então . Se não for definida, então é uma função que não está definida em nenhum lugar. A função pode ser construída a partir da função computável parcial descrita acima e do teorema smn : para cada um , é o índice de um programa que calcula a função . ${\ displaystyle x}$${\ displaystyle \ varphi _ {x} (x)}$${\ displaystyle \ varphi _ {h (x)} \ simeq \ varphi _ {\ varphi _ {x} (x)}}$${\ displaystyle \ varphi _ {x} (x)}$${\ displaystyle \ varphi _ {h (x)}}$${\ displaystyle h}$${\ displaystyle g (x, y)}$${\ displaystyle x}$${\ displaystyle h (x)}$${\ displaystyle y \ mapsto g (x, y)}$

Para completar a prova, seja qualquer função computável total e construa como acima. Let Ser um índice da composição , que é uma função computável total. Então, pela definição de . Mas, porque é um índice de , e, assim, . Pela transitividade de , isso significa . Daí para . ${\ displaystyle F}$${\ displaystyle h}$${\ displaystyle e}$${\ displaystyle F \ circ h}$${\ displaystyle \ varphi _ {h (e)} \ simeq \ varphi _ {\ varphi _ {e} (e)}}$${\ displaystyle h}$${\ displaystyle e}$${\ displaystyle F \ circ h}$${\ displaystyle \ varphi _ {e} (e) = (F \ circ h) (e)}$${\ displaystyle \ varphi _ {\ varphi _ {e} (e)} \ simeq \ varphi _ {F (h (e))}}$${\ displaystyle \ simeq}$${\ displaystyle \ varphi _ {h (e)} \ simeq \ varphi _ {F (h (e))}}$${\ displaystyle \ varphi _ {n} \ simeq \ varphi _ {F (n)}}$${\ displaystyle n = h (e)}$

Esta prova é uma construção de uma função recursiva parcial que implementa o combinador Y .

Funções livres de ponto fixo

Uma função tal que para todos é chamada de ponto fixo livre . O teorema do ponto fixo mostra que nenhuma função computável total é livre de ponto fixo, mas existem muitas funções livres de ponto fixo não computáveis. O critério de completude de Arslanov afirma que o único grau de Turing recursivamente enumerável que calcula uma função livre de ponto fixo é 0 ′ , o grau do problema da parada . ${\ displaystyle F}$${\ displaystyle \ varphi _ {e} \ not \ simeq \ varphi _ {F (e)}}$${\ displaystyle e}$

Segundo teorema de recursão de Kleene

O segundo teorema da recursão é uma generalização do teorema de Rogers com uma segunda entrada na função. Uma interpretação informal do segundo teorema da recursão é que é possível construir programas autorreferenciais; consulte "Aplicação a quines" abaixo.

O segundo teorema da recursão . Para qualquer função recursiva parcial, existe um índice tal que .${\ displaystyle Q (x, y)}$${\ displaystyle p}$${\ displaystyle \ varphi _ {p} \ simeq \ lambda yQ (p, y)}$

O teorema pode ser provado a partir do teorema de Rogers, deixando ser uma função tal que (uma construção descrita pelo teorema Smn ). Pode-se então verificar que um ponto fixo disso é um índice conforme necessário. O teorema é construtivo no sentido de que uma função computável fixa mapeia um índice para Q no índice p . ${\ displaystyle F (p)}$${\ displaystyle \ varphi _ {F (p)} (y) = Q (p, y)}$${\ displaystyle F}$${\ displaystyle p}$

Comparação com o teorema de Rogers

O segundo teorema da recursão de Kleene e o teorema de Rogers podem ser provados, de forma bastante simples, um do outro. No entanto, uma prova direta do teorema de Kleene não faz uso de um programa universal, o que significa que o teorema é válido para certos sistemas de programação sub-cursiva que não têm um programa universal.

Aplicativo para quines

Um exemplo clássico usando o segundo teorema da recursão é a função . O índice correspondente , neste caso, produz uma função computável que produz seu próprio índice quando aplicado a qualquer valor. Quando expressos como programas de computador, esses índices são conhecidos como quines . ${\ displaystyle Q (x, y) = x}$${\ displaystyle p}$

O exemplo a seguir em Lisp ilustra como o no corolário pode ser efetivamente produzido a partir da função . A função no código é a função desse nome produzida pelo teorema Smn . ${\ displaystyle p}$${\ displaystyle Q}$s11

Q pode ser alterado para qualquer função de dois argumentos.

(setq Q '(lambda (x y) x))
(setq s11 '(lambda (f x) (list 'lambda '(y) (list f x 'y))))
(setq n (list 'lambda '(x y) (list Q (list s11 'x 'x) 'y)))
(setq p (eval (list s11 n n)))

Os resultados das seguintes expressões devem ser os mesmos. ${\ displaystyle \ varphi}$ p(nil)

(eval (list p nil))

Q(p, nil)

(eval (list Q p nil))

Aplicação para eliminação de recursão

Suponha que e sejam funções computáveis ​​totais usadas em uma definição recursiva para uma função : ${\ displaystyle g}$${\ displaystyle h}$${\ displaystyle f}$

${\ displaystyle f (0, y) \ simeq g (y),}$

${\ displaystyle f (x + 1, y) \ simeq h (f (x, y), x, y),}$

O segundo teorema de recursão pode ser usado para mostrar que tais equações definem uma função computável, onde a noção de computabilidade não tem que permitir, prima facie, para definições recursivas (por exemplo, pode ser definido por μ-recursão , ou por Turing máquinas ). Esta definição recursiva pode ser convertida em uma função computável que assume ser um índice para si mesma, para simular a recursão: ${\ displaystyle \ varphi _ {F} (e, x, y)}$${\ displaystyle e}$

${\ displaystyle \ varphi _ {F} (e, 0, y) \ simeq g (y),}$

${\ displaystyle \ varphi _ {F} (e, x + 1, y) \ simeq h (\ varphi _ {e} (x, y), x, y).}$

O teorema da recursão estabelece a existência de uma função computável tal que . Assim, satisfaz a definição recursiva fornecida. ${\ displaystyle \ varphi _ {f}}$${\ displaystyle \ varphi _ {f} (x, y) \ simeq \ varphi _ {F} (f, x, y)}$${\ displaystyle f}$

Programação reflexiva

A programação reflexiva ou reflexiva refere-se ao uso de autorreferência em programas. Jones apresenta uma visão do segundo teorema da recursão com base em uma linguagem reflexiva. Mostra-se que a linguagem reflexiva definida não é mais forte do que uma linguagem sem reflexão (porque um intérprete para a linguagem reflexiva pode ser implementado sem usar reflexão); então, mostra-se que o teorema da recursão é quase trivial na linguagem reflexiva.

O primeiro teorema de recursão

Enquanto o segundo teorema de recursão é sobre pontos fixos de funções computáveis, o primeiro teorema de recursão está relacionado a pontos fixos determinados por operadores de enumeração, que são um análogo computável de definições indutivas. Um operador de enumeração é um conjunto de pares ( A , n ) onde A é um ( código para a) conjunto finito de números en é um único número natural. Freqüentemente, n será visto como um código para um par ordenado de números naturais, particularmente quando as funções são definidas por meio de operadores de enumeração. Os operadores de enumeração são de importância central no estudo da redutibilidade de enumeração .

Cada operador de enumeração Φ determina uma função de conjuntos de naturais para conjuntos de naturais dados por

${\ displaystyle \ Phi (X) = \ {n \ mid \ existe A \ subseteq X [(A, n) \ in \ Phi] \}.}$

Um operador recursivo é um operador de enumeração que, quando dado o gráfico de uma função recursiva parcial, sempre retorna o gráfico de uma função recursiva parcial.

Um ponto fixo de um operador Φ enumeração é um conjunto F de tal modo que Φ ( F ) = F . O primeiro teorema de enumeração mostra que pontos fixos podem ser efetivamente obtidos se o próprio operador de enumeração for computável.

Primeiro teorema da recursão . As seguintes afirmações são válidas.

1. Para qualquer operador de enumeração computável Φ, há um conjunto recursivamente enumerável F tal que Φ ( F ) = F e F é o menor conjunto com esta propriedade.
2. Para qualquer operador recursivo Ψ existe uma função computável parcial φ tal que Ψ (φ) = φ e φ é a menor função computável parcial com esta propriedade.

Exemplo

Como o segundo teorema da recursão, o primeiro teorema da recursão pode ser usado para obter funções que satisfaçam sistemas de equações de recursão. Para aplicar o primeiro teorema de recursão, as equações de recursão devem primeiro ser reformuladas como um operador recursivo.

Considere as equações de recursão para a função fatorial f :

${\ displaystyle f (0) = 1}$

${\ displaystyle f (n + 1) = (n + 1) \ cdot f (n)}$

O operador recursivo correspondente Φ terá informações que informam como chegar ao próximo valor de f a partir do valor anterior. No entanto, o operador recursivo realmente definirá o gráfico de f . Primeiro, Φ conterá o par . Isso indica que f (0) é inequivocamente 1 e, portanto, o par (0,1) está no gráfico de f . ${\ displaystyle (\ varnothing, (0,1))}$

A seguir, para cada n e m , Φ conterá o par . Isso indica que, se f ( n ) é m , então f ( n  + 1) é ( n  + 1) m , de modo que o par ( n  + 1, ( n  + 1) m ) está no gráfico de f . Ao contrário do caso base f (0) = 1, o operador recursivo requer algumas informações sobre f ( n ) antes de definir um valor de f ( n  + 1). ${\ displaystyle (\ {(n, m) \}, (n + 1, (n + 1) \ cdot m))}$

O primeiro teorema de recursão (em particular, a parte 1) afirma que existe um conjunto F tal que Φ ( F ) = F. O conjunto F consistirá inteiramente de pares ordenados de números naturais e será o gráfico da função fatorial f , como desejado.

A restrição às equações de recursão que podem ser reformuladas como operadores recursivos garante que as equações de recursão realmente definam um ponto mínimo fixo. Por exemplo, considere o conjunto de equações de recursão:

${\ displaystyle g (0) = 1}$

${\ displaystyle g (n + 1) = 1}$

${\ displaystyle g (2n) = 0}$

Não há função g que satisfaça essas equações, porque elas implicam g (2) = 1 e também implicam g (2) = 0. Assim, não há ponto fixo g satisfazendo essas equações de recursão. É possível fazer um operador de enumeração correspondente a essas equações, mas não será um operador recursivo.

Esboço de prova para o primeiro teorema de recursão

A prova da parte 1 do primeiro teorema da recursão é obtida iterando o operador de enumeração Φ começando com o conjunto vazio. Primeiro, uma sequência F _k é construída, para . Seja F ₀ o conjunto vazio. Procedendo indutivamente, para cada k , deixe F _{k + 1} ser . Finalmente, F é considerado . O restante da prova consiste em uma verificação de que F é recursivamente enumerável e é o ponto mínimo fixo de Φ. A seqüência F _k usada nesta prova corresponde à cadeia de Kleene na prova do teorema de ponto fixo de Kleene . ${\ displaystyle k = 0,1, \ ldots}$${\ displaystyle F_ {k} \ cup \ Phi (F_ {k})}$${\ displaystyle \ bigcup F_ {k}}$

A segunda parte do primeiro teorema da recursão segue da primeira parte. A suposição de que Φ é um operador recursivo é usada para mostrar que o ponto fixo de Φ é o gráfico de uma função parcial. O ponto principal é que, se o ponto fixo F não é o gráfico de uma função, então existe algum k tal que F _k não é o gráfico de uma função.

Comparação com o segundo teorema de recursão

Comparado com o segundo teorema da recursão, o primeiro teorema da recursão produz uma conclusão mais forte, mas apenas quando as hipóteses mais restritas são satisfeitas. Rogers usa o termo teorema da recursão fraca para o primeiro teorema da recursão e teorema da recursão forte para o segundo teorema da recursão.

Uma diferença entre o primeiro e o segundo teorema da recursão é que os pontos fixos obtidos pelo primeiro teorema da recursão são garantidos como pontos mínimos fixos, enquanto aqueles obtidos pelo segundo teorema da recursão podem não ser pelo menos pontos fixos.

Uma segunda diferença é que o primeiro teorema da recursão só se aplica a sistemas de equações que podem ser reformulados como operadores recursivos. Essa restrição é semelhante à restrição a operadores contínuos no teorema de ponto fixo de Kleene da teoria da ordem . O segundo teorema da recursão pode ser aplicado a qualquer função recursiva total.

Teorema generalizado

No contexto de sua teoria das numerações, Ershov mostrou que o teorema da recursão de Kleene é válido para qualquer numeração pré-completa . Uma numeração de Gödel é uma numeração pré-completa no conjunto de funções computáveis, então o teorema generalizado produz o teorema de recursão de Kleene como um caso especial.

Dada uma numeração pré-completa , então para qualquer função computável parcial com dois parâmetros existe uma função computável total com um parâmetro tal que ${\ displaystyle \ nu}$${\ displaystyle f}$${\ displaystyle t}$

${\ displaystyle \ forall n \ in \ mathbb {N}: \ nu \ circ f (n, t (n)) = \ nu \ circ t (n).}$

Veja também

• Semântica denotacional , onde outro teorema de menos ponto fixo é usado para o mesmo propósito que o primeiro teorema de recursão.
• Combinadores de ponto fixo , que são usados ​​no cálculo lambda para o mesmo propósito do primeiro teorema de recursão.

Referências

• Ershov, Yuri L. (1999). "Parte 4: Matemática e Teoria da Computabilidade. 14. Teoria da numeração". Em Griffor, Edward R. (ed.). Handbook of Computability Theory . Estudos em lógica e os fundamentos da matemática. 140 . Amsterdã: Elsevier . pp. 473–503. ISBN 9780444898821. OCLC  162130533 . Página visitada em 6 de maio de 2020 .
• Jones, Neil D. (1997). Computabilidade e complexidade: de uma perspectiva de programação . Cambridge, Massachusetts : MIT Press . ISBN 9780262100649. OCLC  981293265 .
• Kleene, Stephen C. (1952). Introdução à Metamatemática . Bibliotheca Mathematica. Publicação da Holanda do Norte . ISBN 9780720421033. OCLC  459805591 . Página visitada em 6 de maio de 2020 .
• Rogers, Hartley (1967). Teoria das funções recursivas e computabilidade efetiva . Cambridge, Massachusetts : MIT Press . ISBN 9780262680523. OCLC  933975989 . Página visitada em 6 de maio de 2020 .

Notas de rodapé

Leitura adicional

• Jockusch, CG ; Lerman, M .; Soare, RI ; Solovay, RM (1989). "Conjuntos recursivamente enumeráveis ​​por módulo de saltos iterados e extensões do critério de completude de Arslanov". The Journal of Symbolic Logic . 54 (4): 1288–1323. doi : 10.1017 / S0022481200041104 . ISSN  0022-4812 . JSTOR  2274816 .

links externos

• Entrada "Recursive Functions" de Piergiorgio Odifreddi na Stanford Encyclopedia of Philosophy , 2012.