A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

1. O Problema

O artigo aborda a demonstração dos teoremas fundamentais da teoria da computação: o Teorema de Rice e o Problema da Parada (Halting Problem).

• Teorema de Rice: Afirma que nenhuma propriedade semântica não trivial de programas é decidível.
• Problema da Parada: Afirma que não existe um algoritmo que possa determinar, para qualquer programa e entrada, se o programa terminará (halt) ou divergirá.

A Limitação das Provas Clássicas:
As provas tradicionais, como as de Rice e Turing, dependem essencialmente de princípios clássicos de lógica que não são válidos na lógica intuicionista (construtiva):

1. Lei do Terceiro Excluído (LEM): Usada para assumir que um programa ou termina ou não termina.
2. Diagonalização e Auto-referência: A construção de programas que se referem a si mesmos ou a índices de programas (usando o Teorema do Ponto Fixo de Kleene).
3. Análise de Casos em $\bot$: Uma prova clássica de Rice frequentemente exige decidir se o programa que diverge sempre ($\bot$) satisfaz ou não a propriedade $P$, forçando uma divisão de casos baseada na LEM.

O objetivo do autor é fornecer uma prova construtiva (válida na lógica intuicionista) que evite esses princípios, eliminando a necessidade de auto-referência e da Lei do Terceiro Excluído.

2. Metodologia

A abordagem central do artigo é uma redução direta ao Décimo Problema de Hilbert (H10), em vez da redução clássica ao Problema da Parada.

• Fundamento Axiomático: A prova assume apenas a indecidibilidade do Décimo Problema de Hilbert (o teorema MRDP - Davis-Putnam-Robinson-Matiyasevich), que estabelece que o conjunto de soluções de equações diofantinas é indecidível. Esta indecidibilidade é assumida como um axioma externo, mas o restante da prova é puramente intuicionista.
• Modelo de Computação: O autor utiliza um modelo de computação indexado por passos (step-indexed model). Neste modelo, a convergência de um programa é definida pela existência de um limite de "combustível" (fuel) após o qual o programa produz o mesmo resultado, em vez de assumir uma dicotomia clássica entre "termina" e "não termina".
• Construção de Dois Testemunhos (Two-Witness Construction):
  • Dada uma propriedade semântica não trivial $P$ com testemunhos $e_0$ (que não satisfaz $P$) e $e_1$ (que satisfaz $P$).
  • Para cada polinômio diofantino $D$, o autor constrói dois programas, $S^0_D$ e $S^1_D$.
  • Comportamento:
    • Se $D$ tiver solução: $S^0_D$ comporta-se como $e_0$ e $S^1_D$ comporta-se como $e_1$.
    • Se $D$ não tiver solução: Ambos os programas divergem idênticamente (comportam-se como $\bot$).
  • Crucial: Não há necessidade de saber se $P(\bot)$ é verdadeiro ou falso. Se $D$ não tem solução, $S^0_D$ e $S^1_D$ são observacionalmente equivalentes, logo $P(S^0_D) \iff P(S^1_D)$ por extensãoalidade, independentemente do valor de $P$ em $\bot$.
• O Decisor Hipotético: Se existisse um decisor $Decide_P$ para a propriedade $P$, ele poderia distinguir os casos de solvabilidade de $D$ calculando a diferença $\delta_D = Decide_P(S^1_D) - Decide_P(S^0_D)$.
  • Se $D$ é solvável: $\delta_D = 1$.
  • Se $D$ é insolvável: $\delta_D = 0$.
  • Isso criaria um decisor para o Décimo Problema de Hilbert, contradizendo o teorema MRDP.

3. Contribuições Principais

1. Prova Construtiva de Rice e Halting: A primeira prova que demonstra a indecidibilidade de Rice e do Problema da Parada estritamente dentro da lógica intuicionista, sem usar a Lei do Terceiro Excluído, diagonalização ou auto-referência.
2. Eliminação da Divisão de Casos em $\bot$: A prova evita completamente a necessidade de determinar se o programa divergente satisfaz a propriedade, contornando um dos maiores obstáculos para provas construtivas de Rice.
3. Redução Não-Bifurcada (Non-branching): A informação sobre a solvabilidade é codificada na diferença relacional entre dois programas ($\delta_D$), e não em uma decisão de caso sobre um único programa.
4. Formalização em Rocq (Coq): O artigo inclui uma formalização completa no assistente de prova Rocq (Coq).
   • O código tem 1919 linhas.
   • Zero axiomas clássicos admitidos.
   • O único axioma externo é a indecidibilidade de H10 (proveniente da biblioteca coq-library-undecidability), que já é provada construtivamente.
   • O comando Print Assumptions confirma que os teoremas de Rice e Halting estão "fechados sob o contexto global" (dependem apenas do axioma H10, sem lógica clássica adicional).

4. Resultados

• Teorema de Rice Construtivo: Foi provado que, para qualquer propriedade semântica não trivial, não existe um programa que a decida. A prova é válida para programas parciais arbitrários, sem exigir que os testemunhos sejam totais.
• Problema da Parada como Corolário: A indecidibilidade do Problema da Parada é derivada como uma consequência imediata do Teorema de Rice, aplicando o teorema à propriedade "Termina". A prova do Problema da Parada neste contexto é de apenas uma linha de código no Rocq após as definições necessárias.
• Hierarquia de Graus: O artigo discute que a indecidibilidade pode ser "saturada" em polinômios de grau 4 (devido ao teorema MRDP), sugerindo que propriedades indecidíveis podem ser testemunhadas por polinômios de grau baixo, embora a questão de graus 2 ou 3 permaneça aberta.

5. Significado e Impacto

• Conteúdo Computacional: Provas construtivas possuem "conteúdo computacional" que provas clássicas não têm. Isso permite que a lógica de indecidibilidade seja internalizada em sistemas de extração de programas (como Coq e Agda) sem axiomas clássicos ocultos.
• Matemática Reversa Construtiva: O trabalho contribui para a matemática reversa construtiva, identificando exatamente quais princípios não construtivos são necessários para cada teorema. Neste caso, mostra-se que a indecidibilidade de Rice e Halting depende apenas da indecidibilidade de H10, e não da LEM.
• Verificação Formal: A formalização em Rocq serve como uma verificação rigorosa de que a lógica intuicionista é suficiente para estabelecer a indecidibilidade fundamental da computação, desde que se aceite a indecidibilidade de H10.
• Aplicação Prática: O autor fornece um exemplo em C (undecidable.c) que ilustra como a estrutura de prova se traduz em um programa real que busca soluções para equações diofantinas, demonstrando que nenhum analisador estático pode decidir a terminação dessa família de programas.

Em resumo, o artigo reestrutura a fundação da teoria da indecidibilidade, removendo a dependência de argumentos de auto-referência e lógica clássica, substituindo-os por uma redução elegante e construtiva baseada na aritmética diofantina.