Problema da parada

Na teoria da computabilidade o experimento mental do problema da parada é um problema de decisão que pode ser declarado informalmente da seguinte forma:

Dado uma descrição de um programa e uma entrada finita, decida se o programa termina de rodar ou rodará indefinidamente, dada essa entrada.

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á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 é geral o suficiente para ser equivalente a uma máquina de Turing. O problema é determinar para uma dada entrada se 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:

enquanto Verdadeiro: continue

Não para, pelo contrário, entra em loop infinito. Por outro lado, o programa:

imprimir "Hello World!"

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

Um problema de decisão é um conjunto de números naturais; o "problema" é determinar se um número em particular pertence ao conjunto.

Dada uma enumeração de Gödel $\varphi$ de uma função computável (como os números de descrição de Turing) e uma função de pareamento $\langle i,x\rangle$, o problema da parada é o problema de decisão para o conjunto:

$K_{\varphi }^{0}:=\{\langle i,x\rangle |\varphi _{i}(x)\ \mathrm {existe} \}$

com $\varphi _{i}$ a i-ésima função computável na enumeração de Gödel $\varphi$.

Embora o conjunto K seja recursivamente enumerável, o problema da parada não é solúvel por uma função computável.

Existem diversas formulações equivalentes do problema da parada; qualquer conjunto cujo grau de insolubilidade da Teoria da Computação e da Complexidade Computacional (no inglês, Turing degree) é o mesmo que o do problema da parada pode ser considerado como tal formulação. Exemplos de tais conjuntos incluem:

• $\{i\mid \varphi _{i}(0)\ \mathrm {para} \}$
• $\{i\mid \exists n(\varphi _{i}(n)\ \mathrm {para} )\}$

Importância e consequências

A importância histórica do problema da parada reside no fato de que foi um dos primeiros problemas a ser provado indecidível. (A prova de Turing foi lançada em maio de 1936, enquanto a prova de Alonzo Church da indecidibilidade de um problema no cálculo lambda já havia sido lançada em abril de 1936). Subsequentemente, muitos outros problemas foram descritos; o método típico de provar que um problema é indecidível é a técnica de redução. Para isso, o cientista da computação mostra que se uma solução para o novo problema foi encontrada, ela poderia ser usada para decidir um problema indecidível (transformando instâncias do problema indecidível em instâncias do novo problema). Como sabemos de antemão que nenhum método pode decidir o problema antigo, então nenhum método pode decidir o problema novo também.

Uma consequência da indecidibilidade do problema da parada é que não pode existir um algoritmo genérico que decida se um dado enunciado sobre os números naturais é verdadeiro ou falso. A razão para isso é que a proposição que afirma que um certo algoritmo vai parar dado uma certa entrada pode ser convertido em um enunciado equivalente sobre os números naturais. Se nós tivéssemos um algoritmo que pudesse resolver todo enunciado sobre os números naturais, ele certamente poderia resolver tal enunciado; mas isso determinaria se o problema original para o que é impossível, já que o problema da parada é indecidível.

Outra consequência da indecidibilidade do problema da parada é o Teorema de Rice que enuncia que a verdade de qualquer enunciado não-trivial sobre a função definida por um algoritmo é indecidível. Então, por exemplo, o problema da parada "esse algoritmo parará para a entrada 0" já é indecidível. Perceba que esse teorema considera a função definida pelo algoritmo e não o algoritmo propriamente dito. É, por exemplo, possível decidir se um algoritmo vai parar dentro de 100 passos, mas isso não é um enunciado sobre a função que é definida pelo algoritmo.

Gregory Chaitin definiu uma probabilidade de parada, representada pelo símbolo Ω, um tipo de número real que informalmente representa a probabilidade que um programa produzido aleatoriamente pare. Esses números têm o mesmo grau de insolubilidade da Teoria da Computação e da Complexidade Computacional que o problema da parada. É um número normal e um número transcendente que pode ser definido mas não completamente computado. Isso significa que pode ser provado que não existe algoritmo que produza dígitos de Ω, embora seja possível calcular seus primeiros dígitos nos casos simples.

Enquanto a prova de Turing mostrou que não pode existir algoritmo ou método genérico para determinar se um algoritmo para, instâncias individuais de um problema podem muito bem ser suscetíveis a ataques. Dado um algoritmo específico, um pode geralmente mostrar que ele deve parar para qualquer entrada, e de fato cientistas da computação geralmente fazem isso como parte de uma prova exata. Mas cada prova tem que ser desenvolvida especificamente para o algoritmo em mãos; não existe modo mecânico ou genérico para determinar se algoritmos em Máquinas de Turing param. Entretanto, existem algumas heurísticas que podem ser usadas para tentar-se construir uma prova, que freqüentemente dão seguimento a programas típicos. Este campo de pesquisa é conhecido como análise terminatória automatizada.

Devido ao fato de que a resposta negativa ao problema da parada demonstra que existem problemas que não podem ser resolvidos por máquinas de Turing, a tése de Church-Turing limita o que pode ser atingido por qualquer máquina que implemente métodos efetivos. Porém, nem todas as máquinas imagináveis são sujeitas à tese de Church-Turing (i.e. Máquina Oráculo não são). Ainda não se pode afirmar se é possível ou não existir um processo físico determinístico que a longo prazo possa contornar uma simulação por máquina de Turing, desta forma, também é relevante saber se este processo hipotético pode ter utilidade na forma de uma máquina calculadora (um hipercomputador) que poderia resolver o problema da parada para uma máquina de Turing, assim como outras coisas. Também se pergunta se qualquer um destes processos físicos desconhecidos estão envolvidos no funcionamento do cérebro humano e se humanos podem resolver o problema da parada.

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 é recursivamente enumerável, o que significa que há uma função computável que lista todos os pares (i, 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 entradax 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 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:

$h(i,x)={\begin{cases}1&{\text{se }}{\text{ o programa }}i{\text{ para com a entrada }}x,\\0&{\text{caso contrario.}}\end{cases}}$

f(i,j)		i	i	i	i	i	i
		1	2	3	4	5	6
j	1	1	0	0	1	0	1
j	2	0	0	0	1	0	0
j	3	0	1	0	1	0	1
j	4	1	0	0	1	0	0
j	5	0	0	0	1	1	1
j	6	1	1	0	0	1	0
	f(i,i)	1	0	0	1	1	0
	g(i)	U	0	0	U	U	0

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.

Neste caso, o programa i se refere ao programa i em uma enumeração de todos os programas de um modelo Turing completo fixo de computação. A prova segue estabelecendo que toda 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:

$g(i)={\begin{cases}0&{\text{se }}f(i,i)=0,\\{\text{indefinida}}&{\text{caso contrario.}}\end{cases}}$

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:

  procedimento compute_g(i):
      if f(i,i) == 0 então
          retorne 0
       caso contrário
          loop infinito

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

• 1900 - David Hilbert colocou seus 23 problemas (conhecidos como problemas de Hilbert) no Congresso Internacional de Matemáticos em Paris. "Desses, o segundo foi o de provar a consistência dos "axiomas de Peano" em que, como ele tinha mostrado, o rigor da matemática o dependia" (Hodges p. 83, commentário do autor em Davis, 1965, p. 108).
• 1920-1921 - Emil Post explora o problema da parada para a máquina de Post, o considerando como candidato à insolubilidade.(Fonte: Absolutely unsolvable problems and relatively undecidable propositions – account of an anticipation, in Davis, 1965, pp. 340–433.) Sua insolubilidade não foi estabelecida até muito depois, por Marvin Minsky [1961].
• 1928 - Hilbert reformula seu segundo problema no Congresso Internacional de Bolonha. Hodges afirma que ele colocou três perguntas: i.e. #1: Era a matemática completa? #2: Era a matemática consistente? #3: Era a matemática decidível? (Hodges p.91). A terceira pergunta é conhecida como Entscheidungsproblem (Problema de decisão) (Hodges p. 91, Penrose p. 34).
• 1930 - Kurt Gödel anunciou uma prova como resposta para as duas primeiras questões de Hilbert de 1928 [cf Reid p. 198]. "No começo, ele [Hilbert] estava só com raiva e frustrado, mas depois ele começou a tentar lidar de forma construtiva com o problema... Gödel sentiu - e exprimiu o pensamento em seu trabalho - que seu trabalho não contradiz ponto de vista formalista de Hilbert" (Reid p. 199).
• 1931 — Gödel publica "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I", (reimpresso em Davis, 1965, p. 5ff).
• 19 de abril de 1935 - Alonzo Church publicou "An Unsolvable Problem of Elementary Number Theory", em que ele identifica o que significa para uma função a ser efetivamente calculável. Tal função terá um algoritmo, e "... o fato de que o algoritmo tenha terminado torna-se efetivamente conhecido ..." (grifo do autor, Davis, 1965, p. 100).
• 1936 - Church publicou a primeira prova que o problema de decisão era insolúvel. [A Note on the Entscheidungsproblem, reimpresso em Davis, 1965, p. 110].
• 7 de outubro de 1936 - O artigo de Post "Finite Combinatory Processes. Formulation I" foi recebido. Post adiciona ao "processo" uma instrução "(C)Pare". Ele chamou esse processo de "Tipo 1 ... se o processo que determina termina para cada problema específico" (Davis, 1965, p. 289ff).
• 1937 - O artigo de Alan Turing "On Computable Numbers With an Application to the Entscheidungsproblem" foi impresso (reimpresso em Davis, 1965, p. 115).
• 1939 – J. Barkley Rosser observa a equivalência essencial do "método eficaz" definido por Gödel, Church e Turing (Rosser em Davis, 1965, p. 273, "Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem").
• 1943 - Em um artigo, Stephen Kleene afirma que "Na criação de uma teoria completa e algoritmica, o que fazemos é descrever um procedimento ... qual o procedimento necessariamente termina, e de modo que a partir do resultado podemos ler uma resposta definitiva, 'Sim' ou 'Não' à pergunta, 'É o valor do predicado verdade?'".
• 1952 - Kleene (1952) Capítulo XIII ("funções computáveis​​") inclui uma discussão sobre a indecidibilidade do problema da parada para máquinas de Turing e reformula em termos de máquinas que "eventualmente param", ou seja: "... não há algoritmo para decidir se alguma determinada máquina, quando iniciada a partir de qualquer situação, eventualmente para" (Kleene (1952) p.382).
• 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

• Sipser, Michael (2006). «Seção 4.2: O problema da parada». Introdução à Teoria da Computação Segunda edição ed. [S.l.]: Cengage. pp. pp.182–192. ISBN 8522104999  !CS1 manut: Texto extra (link)
• Alan Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, 42 (1936), pp 230–265. online version This is the epochal paper where Turing defines Turing machines, formulates the halting problem, and shows that it (as well as the Entscheidungsproblem) is unsolvable.
• Wiki:HaltingProblem
• B. Jack Copeland ed. (2004), The Essential Turing: Seminal Writings in Computing, Logic, Philosophy, Artificial Intelligence, and Artificial Life plus The Secrets of Enigma, Clarendon Press (Oxford University Press), Oxford UK, ISBN 0-19-825079-7.
• Davis, Martin (1965). The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. New York: Raven Press . Turing's paper is #3 in this volume. Papers include those by Godel, Church, Rosser, Kleene, and Post.
• Davis, Martin (1958). Computability and Unsolvability. New York: McGraw-Hill .
• Alfred North Whitehead and Bertrand Russell, Principia Mathematica to *56, Cambridge at the University Press, 1962. Re: the problem of paradoxes, the authors discuss the problem of a set not be an object in any of its "determining functions", in particular "Introduction, Chap. 1 p. 24 "...difficulties which arise in formal logic", and Chap. 2.I. "The Vicious-Circle Principle" p.37ff, and Chap. 2.VIII. "The Contradictions" p. 60ff.
• Martin Davis, "What is a computation", in Mathematics Today, Lynn Arthur Steen, Vintage Books (Random House), 1980. A wonderful little paper, perhaps the best ever written about Turing Machines for the non-specialist. Davis reduces the Turing Machine to a far-simpler model based on Post's model of a computation. Discusses Chaitin proof. Includes little biographies of Emil Post, Julia Robinson.
• Marvin Minsky, Computation, Finite and Infinite Machines, Prentice-Hall, Inc., N.J., 1967. See chapter 8, Section 8.2 "The Unsolvability of the Halting Problem." Excellent, i.e. readable, sometimes fun. A classic.
• Roger Penrose, The Emperor's New Mind: Concerning computers, Minds and the Laws of Physics, Oxford University Press, Oxford England, 1990 (with corrections). Cf: Chapter 2, "Algorithms and Turing Machines". An overly-complicated presentation (see Davis's paper for a better model), but a thorough presentation of Turing machines and the halting problem, and Church's Lambda Calculus.
• John Hopcroft and Jeffrey Ullman, Introduction to Automata Theory, Languages and Computation, Addison-Wesley, Reading Mass, 1979. See Chapter 7 "Turing Machines." A book centered around the machine-interpretation of "languages", NP-Completeness, etc.
• Andrew Hodges, Alan Turing: The Enigma, Simon and Schuster, New York. Cf Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof.
• Constance Reid, Hilbert, Copernicus: Springer-Verlag, New York, 1996 (first published 1970). Fascinating history of German mathematics and physics from 1880s through 1930s. Hundreds of names familiar to mathematicians, physicists and engineers appear in its pages. Perhaps marred by no overt references and few footnotes: Reid states her sources were numerous interviews with those who personally knew Hilbert, and Hilbert's letters and papers.
• Edward Beltrami, What is Random? Chance and order in mathematics and life, Copernicus: Springer-Verlag, New York, 1999. Nice, gentle read for the mathematically-inclined non-specialist, puts tougher stuff at the end. Has a Turing-machine model in it. Discusses the Chaitin contributions.
• Ernest Nagel and James R. Newman, Godel’s Proof, New York University Press, 1958. Wonderful writing about a very difficult subject. For the mathematically-inclined non-specialist. Discusses Gentzen's proof on pages 96–97 and footnotes. Appendices discuss the Peano Axioms briefly, gently introduce readers to formal logic.
• Taylor Booth, Sequential Machines and Automata Theory, Wiley, New York, 1967. Cf Chapter 9, Turing Machines. Difficult book, meant for electrical engineers and technical specialists. Discusses recursion, partial-recursion with reference to Turing Machines, halting problem. Has a Turing Machine model in it. References at end of Chapter 9 catch most of the older books (i.e. 1952 until 1967 including authors Martin Davis, F. C. Hennie, H. Hermes, S. C. Kleene, M. Minsky, T. Rado) and various technical papers. See note under Busy-Beaver Programs.
• Busy Beaver Programs are described in Scientific American, August 1984, also March 1985 p. 23. A reference in Booth attributes them to Rado, T.(1962), On non-computable functions, Bell Systems Tech. J. 41. Booth also defines Rado's Busy Beaver Problem in problems 3, 4, 5, 6 of Chapter 9, p. 396.
• David Bolter, Turing’s Man: Western Culture in the Computer Age, The University of North Carolina Press, Chapel Hill, 1984. For the general reader. May be dated. Has yet another (very simple) Turing Machine model in it.
• Stephen Kleene, Introduction to Metamathematics, North-Holland, 1952. Chapter XIII ("Computable Functions") includes a discussion of the unsolvability of the halting problem for Turing machines. In a departure from Turing's terminology of circle-free nonhalting machines, Kleene refers instead to machines that "stop", i.e. halt.