Máquina de Turing e Decidibilidade

A máquina de Turing é o modelo que define o que significa "computável". Sua importância não está na eficiência — é um modelo deliberadamente primitivo — mas em delimitar a fronteira do possível.

O modelo

Uma fita infinita dividida em células, uma cabeça que lê e escreve, e um controle finito. A cada passo, com base no estado atual e no símbolo lido, a máquina escreve um símbolo, move a cabeça uma célula e muda de estado.

Formalmente, uma 7-upla $(Q,\Sigma,\Gamma,\delta,q_0,q_{\text{aceita}},q_{\text{rejeita}})$.

Três comportamentos possíveis: aceitar, rejeitar ou não parar. Esta terceira possibilidade é a fonte de tudo o que se segue.

Decidível e reconhecível

• Decidível (recursiva): existe máquina que sempre para e responde corretamente.
• Reconhecível (recursivamente enumerável): existe máquina que aceita as cadeias da linguagem, mas pode não parar nas demais.

A diferença é decisiva. Uma linguagem é decidível se e somente se ela e seu complemento são reconhecíveis.

Tese de Church-Turing

Tudo que é "efetivamente calculável" pode ser calculado por uma máquina de Turing.

Não é um teorema — é uma tese sobre a adequação do modelo à noção intuitiva. A evidência é forte: cálculo lambda, funções recursivas, máquinas de registradores e toda linguagem de programação real definem exatamente a mesma classe de funções.

A consequência prática: a escolha da linguagem de programação não muda o que é computável. Só muda a conveniência.

O problema da parada

$$\text{PARADA} = {\langle M,w\rangle : M \text{ para com entrada } w}$$

Teorema (Turing, 1936). PARADA é indecidível.

A prova é por diagonalização. Suponha que exista $H$ que decida a parada. Construa $D$ que, ao receber $\langle M\rangle$, roda $H(\langle M\rangle,\langle M\rangle)$ e faz o oposto: entra em laço se $H$ diz que para, e para se $H$ diz que não para.

Agora pergunte: $D$ para com entrada $\langle D\rangle$?

Se para, então $H$ disse que não para — contradição. Se não para, $H$ disse que para — contradição. Logo $H$ não existe. $\blacksquare$

O argumento é o mesmo do paradoxo do barbeiro e da diagonal de Cantor: autorreferência produzindo contradição.

Redução

A técnica padrão para provar indecidibilidade de outros problemas: se $A$ é indecidível e $A$ se reduz a $B$, então $B$ é indecidível.

A leitura intuitiva: "se eu soubesse resolver $B$, saberia resolver $A$; como não sei resolver $A$, não posso saber resolver $B$".

Teorema de Rice

Um resultado devastador e pouco conhecido fora da área: toda propriedade não trivial do comportamento de programas é indecidível.

"Não trivial" significa que alguma máquina tem a propriedade e alguma não tem. "Do comportamento" significa que depende da função computada, não do texto do programa.

Consequências diretas, todas indecidíveis em geral:

• Este programa termina?
• Estes dois programas calculam a mesma coisa?
• Este programa acessa memória inválida?
• Este trecho de código é alcançável?
• Este programa tem vazamento de memória?

Como a prática convive com isso

Este é o ponto mais importante da página. A indecidibilidade não impede ferramentas úteis — impede ferramentas simultaneamente completas, corretas e sempre terminantes. Abre-se mão de uma das três:

Aproximação conservadora. Analisadores estáticos e sistemas de tipos rejeitam alguns programas corretos, mas nunca aceitam um errado. Um verificador de tipos que recusa código que funcionaria é o preço da decidibilidade.

Incompletude. Ferramentas que podem responder "não sei". A maioria dos analisadores modernos faz isso.

Não terminação. Provadores de teoremas que podem rodar indefinidamente, com limite de tempo imposto de fora.

Restrição do domínio. Linguagens totais (Coq, Agda) garantem terminação restringindo a recursão ao que se pode provar decrescente. Em troca, não são Turing-completas.

Compreender essa negociação evita duas ilusões opostas: esperar que o compilador detecte todos os defeitos, e concluir que análise estática não serve para nada.

Contagem: por que quase tudo é incomputável

Um argumento simples e esclarecedor. Programas são cadeias finitas sobre alfabeto finito, logo o conjunto de programas é enumerável. Já o conjunto de funções $\mathbb{N}\to{0,1}$ tem a cardinalidade dos reais — não enumerável.

Portanto quase toda função é incomputável. As funções que sabemos calcular são uma parcela infinitesimal do que existe. A surpresa não é que haja problemas indecidíveis; é que tantos problemas úteis sejam decidíveis.

Exemplo trabalhado

Por que não é possível escrever um detector universal de laços infinitos?

Se para(prog, entrada) existisse, poderíamos escrever:

def diagonal(prog):
    if para(prog, prog):
        while True:      # entra em laço
            pass
    else:
        return           # termina

Aplicando diagonal a si mesma, ambas as respostas de para levam a contradição. Portanto para não pode existir.

Aplicações em computação

Compiladores. Otimizações são sempre aproximações conservadoras; eliminação de código morto detecta só o que consegue provar.

Sistemas de tipos. A negociação entre expressividade e decidibilidade define o desenho da linguagem.

Verificação formal. Model checking restringe o espaço de estados a finito, tornando o problema decidível.

Segurança. Detectar malware por comportamento é indecidível em geral — daí heurísticas e assinaturas.

Ferramentas de análise. Falsos positivos são inerentes ao problema, não defeitos de implementação.

Erros comuns

• Concluir que análise estática é inútil por causa da indecidibilidade.
• Confundir indecidível com difícil. NP-completo é difícil; indecidível é impossível.
• Esquecer que instâncias particulares podem ser decidíveis. É o caso geral que não é.
• Achar que a tese de Church-Turing é teorema.

Leituras recomendadas

• Sipser, capítulos 3 a 5 — máquinas de Turing, decidibilidade e redução, com provas acessíveis.
• Turing, "On Computable Numbers" (1936) — o artigo original, surpreendentemente legível.
• Hopcroft, Motwani e Ullman, capítulos 8 e 9.
• Rice (1953) — o teorema que generaliza a indecidibilidade a toda propriedade semântica.

Michael Sipser (2012). Introduction to the Theory of Computation. Cengage Learning. ISBN 9781133187790. John E. Hopcroft and Rajeev Motwani and Jeffrey D. Ullman (2006). Introduction to Automata Theory, Languages, and Computation. Pearson. ISBN 9780321455369.

Referências

1. Michael Sipser (2012). Introduction to the Theory of Computation. Cengage Learning.
2. John E. Hopcroft; Rajeev Motwani; Jeffrey D. Ullman (2006). Introduction to Automata Theory, Languages, and Computation. Pearson.