Saltar para o conteúdo

Diferenças entre edições de "Problema da parada"

9 776 bytes removidos ,  21h32min de 7 de dezembro de 2011
bot: revertidas edições de Pedro.atmc ( modificação suspeita : -38), para a edição 27889175 de Helder.wiki
(bot: revertidas edições de Pedro.atmc ( modificação suspeita : -38), para a edição 27889175 de Helder.wiki)
 
[[Alan Turing]] provou em 1936 que um [[algoritmo]] genérico para resolver o problema da parada para ''todos'' pares programa-entrada possíveis não pode existir. Dizemos que o problema da parada é ''indecidível'' nas [[Máquina de Turing|Máquinas de Turing]].
 
==Introdução==
 
O problema da parada é um problema de decisão sobre as propriedades de programas de computadores em um determinado modelo [[Turing-completo]] de computação, por exemplo todos os programas que podem ser escritos em uma [[linguagem de programação]] que generaliza o suficiente para ser equivalente a uma máquina de Turing. O problema é determinar para uma dada entrada o programa irá parar com ela. Nesta área de trabalho abstrata não há limitações de memória ou tempo necessário para a execução de um programa, pois poderão ser necessários tempo e espaço arbitrários para o programa parar. A questão é se o programa simplesmente poderá parar com uma certa entrada.
 
Por exemplo, em [[pseudocódigo]], o programa:
 
:<tt>enquanto Verdadeiro: continue</tt>
 
Não para, pelo contrário, entra em loop infinito. Por outro lado, o programa:
 
:<tt>imprimir "Hello World!"</tt>
 
Pára muito rapidamente.
 
Um programa mais complexo pode ser mais difícil de se analisar. O programa pode rodar por um tempo fixo e se ele não parar, não há um jeito de saber se o programa irá parar eventualmente ou se ele irá continuar rodando para sempre. Turing provou que não há um algoritmo que pode ser aplicado a qualquer programa arbitrário, com uma entrada, para decidir se o programa pára ou não com esta entrada.
 
==Enunciado Informal==
 
A introdução de Turing do modelo de máquina que posteriormente ficou conhecido como Máquinas de Turing, introduzido no artigo, provou-se um modelo muito conveniente para a [[Teoria da Computação]].
 
==Representando o problema da parada como um conjunto==
 
A representação convencional dos problemas de decisão é o conjunto de objectos que possuem a propriedade em questão. O “conjunto da parada”
: ''K'' := { (''i'', ''x'') | programa ''i'' eventualmente irá parar com a entrada ''x''}
Representa o problema da parada.
Este conjunto é [[Conjuntos recursivamente enumeráveis|recursivamente enumerável]], o que significa que há uma função computável que lista todos os pares (''i'',&nbsp;''x'') contidos no conjunto. Porém, o complemento deste conjunto não é recursivamente enumerável.
Existem muitas formulações equivalentes do problema da parada. Qualquer conjunto no qual o [[Grau de Turing]] é igual ao do problema da parada é uma dessas formulações. Exemplos:
*{ ''i'' | programa ''i'' eventualmente para quando a entrada é 0 }
*{ ''i'' | há uma entrada''x'' para que um dado programa ''i'' eventualmente pare com a entrada ''x'' }.
 
==Esboço da Prova==
A prova mostra que não há uma [[função parcial]] [[função computável|computável]] que decide se um programa arbitrário ''i'' pára com uma entrada arbitrária ‘’x’’, isto é, a seguinte função ‘’h’’ não é computável:
:<math>h(i,x) =
\begin{cases}
1 & \text{se } \text{ o programa }i\text{ para com a entrada }x, \\
0 & \text{caso contrario.}
\end{cases}</math>
 
<div style="float:right; padding-left:2em; width:3in; background:white;">
{| class="wikitable" style="padding-bottom:0.5em; margin-bottom:0; margin-top:1em; margin-left:auto; margin-right:auto;"
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| colspan="2" rowspan="2" style="vertical-align: middle;" | ''f''(''i'',''j'')
| style="background:#f2f2f2; width:24.75;"| i
| style="background:#f2f2f2; width:24.75;"| i
| style="background:#f2f2f2; width:24.75;"| i
| style="background:#f2f2f2; width:24.75;"| i
| style="background:#f2f2f2; width:24.75;"| i
| style="background:#f2f2f2; width:24.75;"| i
|- style="font-size:9pt; text-align:center; vertical-align:bottom; background:#f2f2f2;"
| style="background:#f2f2f2;"| 1
| style="background:#f2f2f2;"| 2
| style="background:#f2f2f2;"| 3
| style="background:#f2f2f2;"| 4
| style="background:#f2f2f2;"| 5
| style="background:#f2f2f2;"| 6
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="background:#f2f2f2; height:12px; width:18.75;"| j
| style="background:#f2f2f2;"| 1
| style="background:#ffc000;"| 1
| 0
| 0
| 1
| 0
| 1
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="background:#f2f2f2; height:12px;"| j
| style="background:#f2f2f2;"| 2
| 0
| style="background:#ffc000;"| 0
| 0
| 1
| 0
| 0
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="background:#f2f2f2; height:12px;"| j
| style="background:#f2f2f2;"| 3
| 0
| 1
| style="background:#ffc000;"| 0
| 1
| 0
| 1
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="background:#f2f2f2; height:12px;"| j
| style="background:#f2f2f2;"| 4
| 1
| 0
| 0
| style="background:#ffc000;"| 1
| 0
| 0
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="background:#f2f2f2; height:12px;"| j
| style="background:#f2f2f2;"| 5
| 0
| 0
| 0
| 1
| style="background:#ffc000;"| 1
| 1
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="background:#f2f2f2; height:12px;"| j
| style="background:#f2f2f2;"| 6
| 1
| 1
| 0
| 0
| 1
| style="background:#ffc000;"| 0
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="height:12px;"|
|
|
|
|
|
|
|
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="height:12px;"|
| style="background:#ffc000;"| ''f''(''i'',''i'')
| style="background:#ffc000;"| 1
| style="background:#ffc000;"| 0
| style="background:#ffc000;"| 0
| style="background:#ffc000;"| 1
| style="background:#ffc000;"| 1
| style="background:#ffc000;"| 0
|- style="font-size:9pt; text-align:center; vertical-align:bottom;"
| style="height:12px;"|
| style="background:#99ff8b;"| ''g''(''i'')
| style="background:#99ff8b;"| U
| style="background:#99ff8b;"| 0
| style="background:#99ff8b;"| 0
| style="background:#99ff8b;"| U
| style="background:#99ff8b;"| U
| style="background:#99ff8b;"| 0
|}
<div style="margin-right: 1em;">
<small>
Possíveis valores para uma função parcial computável ‘’f’’ organizada em uma tabela bidimensional. As células laranjas são a diagonal. Os valores de ‘’f’’(‘’i’’, ‘’i’’) e ‘’g’’(‘’i’’) são demonstrados no fundo. ‘’U’’ indica que a função ‘’g’’ é indefinida para um valor de entrada em particular.</small></div>
</div>
 
Neste caso, o ‘’programa i’’ se refere ao programa ‘’i’’ em uma [[enumeração]] de todos os programas de um modelo [[Turing-completa|Turing completo]] fixo de computação.
A prova segue estabelecendo que total função parcial computável com dois argumentos se diferencia da função necessária ‘’h’’. Com esta finalidade, dada qualquer função parcial computável binária ‘’f’’, a seguinte [[função parcial]] ‘’g’’ também é computável por um certo programa ‘’e’’:
:<math>g(i) =
\begin{cases}
0 & \text{se } f(i,i) = 0,\\
\text{indefinida} & \text{caso contrario.}
\end{cases}</math>
 
A verificação de que ''g'' é computável depende das construções seguintes:
* subprogramas computáveis (o programa que computa ''f'' é um subprograma no programa ''e''),
* duplicação de valores (o programa ''e'' computa as entradas ''i'', ''i'' para ''f'' da entrada ''i'' para ''g''),
* ramificação condicional (o programa ''e'' seleciona entre dois resultados dependendo do valor que ele computa para ''f''(''i'', ''i'')),
* não-produção de um resultado definido (por exemplo, rodar para sempre [loop infinito]),
* retornar um valor 0.
 
O [[pseudocódigo]] seguinte ilustra um meio simples de se computar ''g'':
<div style="width: 50%;">
<source lang="pascal" >
procedimento compute_g(i):
if f(i,i) == 0 então
retorne 0
caso contrário
loop infinito
</source>
</div>
 
Por ''g'' ser uma função parcial computável, deve haver um programa ''e'' que compute ''g'', assumindo que o modelo de computação é Turing-completo. Este programa é um de vários outros programas em que a função de parada ''h'' é definida. O próximo passo da prova demonstra que ''h''(''e'', ''e'') não irá ter os mesmos valores que ''f''(''e'', ''e'').
 
É seguida a definição de ''g'' que exatamente um dos dois casos deve ser verdadeiro:
* ''g''(''e'') = ''f''(''e'', ''e'') = 0. Neste caso ''h''(''e'',''e'') = 1, porque o programa ''e'' pára com a entrada ''e''.
* ''g''(''e'') é indefinido e ''f''(''e'',''e'') ? 0. Neste caso ''h''(''e'',''e'') = 0, porque o programa ''e'' não pára com a entrada ''e''.
Em qualquer caso, ''f'' não pode ser a mesma função que ''h'', porque ''f'' foi uma função parcial computável ''arbitrária'' com dois argumentos, todas estas funções devem divergir de ''h''.
 
Esta prova é análoga ao [[Argumento de diagonalização de Cantor]]. O indivíduo deve visualizar um array bidimensional com uma coluna e uma linha para cada número natual, como indicado na tabela acima. O valor de ''f''(''i'',''j'') é colocado na coluna ''i'', linha ''j''. Porque assumimos que ''f'' deve ser uma função parcial computável, qualquer elemento do array pode ser calculado usando ''f''. A construção da função ''g'' pode ser visualizada utilizando a diagonal principal deste array. Se o array tem um 0 na posição (''i'',''i''), então ''g''(''i'') é 0. Caso contrário ''g''(''i'') é indefinido. A contradição vem do fato que existe uma coluna ''e'' do array correspondendo ao ''g''. Se ''f'' fosse a função de parada ''h'', haveria um 1 na posição (''e'',''e'') se e somente se ''g''(''e'') for definido, mas ''g'' é construído de forma que se e somente se há um 0 na posição (''e'',''e'').
 
 
== Histórico do problema da parada ==
* 1952 - "Davis [Martin Davis] pensa que é provável que ele tenha usado pela primeira vez o termo 'problema da parada' em uma série de palestras que ele deu no Laboratório de Sistemas de Controle da Universidade de Illinois em 1952 (carta de Davis para Copeland, 12 de dezembro de 2001.)" (nota de rodapé 61 em Copeland (2004) pp.40ff).
 
==Referências Bibliográficas==
* {{cite book | authorlink = Michael Sipser | last = Sipser | first = Michael | year = 2006 | title = Introdução à Teoria da Computação | edition = Segunda edição | publisher = Cengage | id = ISBN 8522104999 | chapter = Seção 4.2: O problema da parada | pages = pp.182–192 }}
 
[[Categoria:Problemas matemáticos]]