Análise da Tese de Church e Indecidibilidade em Funções Computáveis

Tese de Church e o Problema da Indecidibilidade Continuação Existe uma Função Total PLComputável que não é PLGOTOComputável função total com uma entrada e uma saída computada por eventualmente pára por que não contém GOTO 0 1 2 é a enumeração de todos programas PLGOTO Primeiro lista todos os programas com 1 símbolo ie Depois lista todos os programas com 2 símbolos ie 4 símbolos ex A 0 fi W W i fx fxx 1 é efetivamente computável Dado obtenha e execute com como valor inicial de X1 x x x x Y1 será Adicione um ao resultado para obter fxx fx f não é PLGOTO computável diagonalização de Cantor f é PLcomputável tese de Church Procedimento efetivo Procedimento efetivo SIM Teorema 23 SIM Existe uma Função Total que não é PLComputável é a enumeração das funções totais PLcomputáveis 0 1 2 é a enumeração de todos programas PL fi W W fx fxx 1 não é PLcomputável diagonalização de Cantor f f0 f1 f2 Existe uma função total que não é efetivamente computável Tese de Church subconjunto A enumeração de funções totais PLcomputáveis não é efetiva Teorema 24 Corolário 25 f é total é total fx SIM O Conjunto das Funções Totais de em é Contável W W é qualquer enumeração de funções totais tal que f0 f1 f2 fi W W Existe f W W tal que f fi fx fxx 1 Teorema 26 A função é PLComputável h Seja uma listagem de funções PLComputáveis de em fx W W Como é definida pára na entrada fxx x x hx 1 se x dom fx Assuma que é PLcomputável e portanto é efetivamente computável h 0 se x dom fx gx fxx 1 se hx 1 0 se hx 0 Se é efetivamente computável é efetivamente computável h g Compute Se obtenha a apresentação para hx x fx hx 1 Então gx fxx 1 Se hx 0 gx 0 Se é efetivamente computável é PLcomputável Tese de Church g g Então enumeração das PLcomputáveis yg fy Mas definição de g gy fyy 1 se y dom fy Como é total e contradição fy y dom f hy 1 fyy fyy 1 Logo não é PLcomputável h NÃO Procedimento efetivo Teorema 27 Existe um procedimento efetivo que dado um programa PL arbitrário decide se pára na entrada x x y Para e arbitrários onde x y y dom fx Se é apresentado pelo programa fx x Então se e somente se pára na entrada y dom fx x y Corolário 28 NÃO Problema da Parada O problema da parada é indecidível Teorema 27 Tese de Church hx 1 se x dom fx 0 se x dom fx e são PLcomputáveis g1 g2 Compute Se obtenha a apresentação para g2x g2x 1 x fx g1x y 1 se y dom fx 0 se y dom fx g2x Se fosse PLcomputável também seria pois g1 h hx g1x x Se fosse PLcomputável seria total e PLcomputável ou efetivamente computável T de Church g2 g3 g3x fxx 1 se g2x 1 0 se g2x 0 Como é PLcomputável e total pára na entrada fxx x x Então g3x fxx 1 Se g2x 0 g3x 0 Então enumeração das PLcomputáveis e totais yg3 fy Mas se é PLcomputável e total definição de g3 fyy 1 fy g3 Como é total e contradição fy y dom f g2y 1 fyy fyy 1 Logo não é PLcomputável g2 NÃO Procedimento efetivo Teorema 29 Corolário 210 caso contrário 0 1 se é PLcomputável e total fx Problemas Indecisíveis a Dado um programa arbitrário e uma entrada pára na entrada y y b Dado um programa arbitrário ele pára em todas as entradas Ou Existe alguma entrada que faz o programa entrar em loop infinito Premissas Não existe limite de tempo para a execução Não existe limite de espaço de armazenamento disponível Teorema 211 A função é PLcomputável k Dado obtenha o programa que computa x fx Seja uma enumeração efetiva de funções PLcomputáveis f0 f1 fi W W i 0 kx 1 se x dom fx se x dom fx Execute na entrada irá parar se e somente se x x x x dom fx Se pára x kx 1 Se não o processo nunca termina dom k xx dom fx Apesar de não existir um procedimento que decida se um arbitrário está em existe um procedimento efetivo que irá eventualmente fornecer uma resposta afirmativa caso x dom fx x dom fx Procedimento efetivo SIM Teorema 211 Algoritmo Um algoritmo sempre pára Um programa efetivo apenas pára em entradas no domínio da função sendo computada Um procedimento efetivo programa que computa a função f Wr Ws é um algoritmo se e somente se dom f Wr Indecidibilidade kx 1 se x dom fx se x dom fx A função pode ser efetivamente computada k Existe um procedimento efetivo que dado retorna 1 se x x dom fx hx 1 se x dom fx 0 se x dom fx Se nenhuma saída é produzida uma vez que o procedimento efetivo não pára x dom fx A função não é efetivamente computável h Um procedimento efetivo para computar deve fornecer uma saída para qualquer entrada h Não existe procedimento efetivo para decidir se um procedimento efetivo arbitrário é um algoritmo Teorema 29 Pelo Teorema 27 isso é impossível Funções Recursivas Cap 3 Walter Brainerd Tese de Church Formalismos Funções Recursivas Parciais Linguagem de Programação PL Máquinas de Registradores Ilimitados Máquinas de Registrador Único Máquina de Turing Algoritmos Rotulados de Markov 1 2 3 4 5 6 Funções Recursivas Funções Recursivas Primitivas Funções Recursivas Parciais PLGOTOcomputáveis PLcomputáveis Novo Formalismo Funções Recursivas Parciais São definidas indutivamente a partir de um conjunto de funções iniciais e 4 operações usadas para obter funções a partir de outras já definidas Funções Iniciais ι W W Identidade Projeção π W W 0 Zero ζ W 0 W Sucessor ς W W πx ιx x ζ 0 ςx x 1 4 Operações f gx y fx gy Combinação Composição f gx fgx Exponenciação f x y y vezes f fx Repetição fx y x f kx y x 1 para algum x onde k é o menor valor tal que Funções Recursivas Parciais Uma função é recursiva parcial em se ela é uma das funções em ou pode ser obtida destas funções por um número finito de composições combinações exponenciações ou repetições f Wr Ws Σ π ι ζ ς Σ FRParcial Funções Recursivas Uma função é recursiva em se ela é recursiva parcial em e total f Wr Ws Σ Σ dom f Wr FRParcial FR Funções Recursivas Primitivas Uma função é recursiva primitiva em se ela é uma das funções em ou pode ser obtida destas funções por um número finito de composições combinações ou exponenciações f Wr Ws Σ π ι ζ ς Σ FRParcial FR FR Primitiva Definições Independentes de Representação As definições são a mesma para todo Σ Embora as manipulações com palavras variam com o Σ ς112 113 em Σ3 ς112 121 em Σ2 Números na base 10 são abreviações de palavras em Σ ς112 em Σ3 ς112 em Σ2 Fecho nas 4 Operações também são Se e são recursivas ou recursivas primitivas f g é parcial recursiva mas não é recursiva primitiva e pode não ser recursiva f f g f g e f Funções recursivas parciais são fechadas nas operações de composição combinação exponenciação e repetição FRParcial FR FR Primitiva Funções Identidade ιr Para r 0 ιr Wr Wr onde ι0 ι1w1 w1 ι2w1 w2 w1 w2 ιrx x Repete a entrada na saída ι0 ι1w1 ι2w1 w2 Funções Diagonalização δr δ W W 2 δx x x Para r 1 δr Wr Wr1 onde δ1w1 w1 w1 δ2w1 w2 w1 w2 w2 Adiciona uma cópia do último argumento δrx1 xr x1 xr xr δ1w1 δ2w1 w2 Funções Troca jξr jξrx1 xj xj1 xr x1 xj1 xj xr Para r 2 e 1 j r jξr Wr Wr onde Troca a posição de dois elementos consecutivos da entrada Funções Projeção πr Para cada r 1 πr Wr Wr1 onde π1w1 π2w1 w2 w1 π3w1 w2 w3 w1 w2 Remove o último elemento da entrada πrx1 xr x1 xr1 π1w1 π2w1 w2 π3w1 w2 w3 Funções de Reorganização Cada valor da saída é um dos valores da entrada fx1 x2 xr xi1 xi2 xis É qualquer função total dada por f Wr Ws r s 0 onde cada é um inteiro entre 1 e r ij 1 j s ιr i1 1 i2 2 ir r Exemplos δr i1 1 i2 2 ir ir1 r jξr i1 1 i2 2 ij j 1 ij1 j ir r π s 0 πr i1 1 ir1 r 1 r 2 ς ιr δr jξr π πr ζ não é função de reorganização não é função de reorganização