💻 computer science

Nonlinear Arithmetic with SMTLIB Division is Undecidable

O artigo demonstra que a aritmética real não linear (NRA), conforme definida no padrão SMTLIB, é indecidível porque o tratamento da divisão por zero como uma função não interpretada permite a codificação de problemas indecidíveis da aritmética inteira.

Autores originais: Dejan Jovanovic

Publicado 2026-05-27

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Dejan Jovanovic

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um detetive tentando resolver um mistério usando um conjunto muito estrito de regras. No mundo da ciência da computação, essas regras são chamadas de "teorias", e elas ajudam os computadores a decidir se um quebra-cabeça matemático tem solução ou não.

Este artigo trata de um conjunto específico de regras chamado Aritmética Real Não Linear (NRA). Pense nisso como um jogo jogado com números reais (como 3,14, -5 ou 0,001), onde você pode adicioná-los, subtraí-los, multiplicá-los e dividi-los.

A Regra "Mágica" que Quebra o Jogo

Por muito tempo, os matemáticos acreditaram que este jogo era perfeitamente solucionável. Se você desse a um computador um quebra-cabeça usando esses números, ele eventualmente poderia dizer: "Sim, há uma solução", ou "Não, não há".

No entanto, o autor, Dejan Jovanović, descobriu uma armadilha oculta no livro de regras oficial (o padrão SMTLIB). A armadilha está na forma como as regras lidam com a divisão por zero.

Na matemática normal, dividir por zero é um grande "Não". Mas neste livro de regras específico de computador, as regras dizem: "Se você dividir por zero, não nos importamos qual é a resposta. Pode ser qualquer coisa, desde que aja como um número normal quando você não estiver dividindo por zero."

O autor chama isso de uma "função não interpretada". Para usar uma analogia: imagine uma máquina de vendas que funciona perfeitamente para qualquer lanche que você compra. Mas se você tentar comprar um "Lanche Zero", a máquina não trava; em vez disso, ela apenas cospe algo — talvez uma barra de chocolate, talvez uma pedra, talvez uma nuvem. As regras não dizem o que será; elas apenas dizem: "Será algo."

Como Isso Torna o Jogo Insolvável

O artigo argumenta que esta regra de "vale tudo" para divisão por zero é a chave que abre uma porta para o caos.

Aqui está a lógica, simplificada:

O Objetivo: O autor quer provar que, se você tiver esta regra de "divisão mágica", pode enganar o computador para resolver quebra-cabeças de inteiros (quebra-cabeças com números inteiros como 1, 2, 3).
O Problema: Resolver quebra-cabeças de inteiros é famosamente impossível para computadores fazerem perfeitamente para todos os casos (isso é conhecido como o Décimo Problema de Hilbert). É como tentar encontrar uma agulha em um palheiro que continua crescendo para sempre.
O Truque: O autor mostra que, usando a "divisão mágica" por zero, é possível construir uma ponte matemática. Você pode pegar um quebra-cabeça difícil de inteiros e traduzi-lo em um quebra-cabeça de números reais usando este truque de divisão.
- Analogia: Imagine que você tem um código secreto escrito em uma linguagem que apenas humanos entendem (inteiros). Você constrói uma máquina (o truque de divisão) que traduz este código para uma linguagem que computadores entendem (números reais). Como a linguagem do computador tem esta regra "mágica" de divisão por zero, o computador pode acidentalmente resolver o código humano.
O Resultado: Como sabemos que os computadores não podem resolver todos os quebra-cabeças de inteiros, e este truque permite que eles tentem resolver quebra-cabeças de inteiros usando números reais, isso significa que o computador não pode resolver todos os quebra-cabeças de números reais também. O jogo torna-se indecidível.

A Analogia da Função "Teto"

Para provar isso, o autor usa um truque inteligente. Ele mostra que, se você tiver esta "divisão mágica", pode forçar o computador a agir como uma função floor (uma função que arredonda um número para baixo até o inteiro mais próximo, como transformar 3,9 em 3).

Uma vez que o computador pode arredondar números para baixo, ele pode começar a contar inteiros. Uma vez que pode contar inteiros, pode tentar resolver aqueles quebra-cabeças de inteiros impossíveis. Como esses quebra-cabeças são impossíveis de resolver em geral, todo o sistema de matemática de números reais com esta regra de divisão torna-se impossível de resolver em geral.

O Que Isso Significa para o Mundo Real (De Acordo com o Artigo)

O artigo não fala sobre IA futura ou usos médicos. Ele foca no estado atual dos benchmarks de computador (problemas de teste):

A Armadilha: Muitos problemas de teste existentes na biblioteca SMTLIB (uma enorme coleção de quebra-cabeças matemáticos usados para testar computadores) usam divisão com variáveis (como x / y). Se y acontecer de ser zero, esses quebra-cabeças caem na armadilha "indecidível".
A Solução? O autor sugere duas maneiras de corrigir o livro de regras:
1. Escolher uma resposta específica: Decidir que dividir por zero sempre é igual a um número específico (como 0 ou 1), assim como alguns sistemas de computador lidam com isso para números binários.
2. Dividir o jogo: Criar uma nova categoria separada para problemas onde você divide por variáveis, e manter a categoria "segura" para problemas onde você só divide por números conhecidos (constantes).

A Conclusão

O artigo afirma que uma regra específica, aparentemente inofensiva, sobre como os computadores lidam com "divisão por zero" acidentalmente quebra a capacidade dos computadores de resolver todos os problemas matemáticos envolvendo números reais. Transforma um jogo solucionável em um insolvável, permitindo que o computador resolva furtivamente problemas que ele não deveria ser capaz de resolver.

Resumo Técnico: Aritmética Não Linear com Divisão SMTLIB é Indecidível

Enunciado do Problema
O artigo aborda o status de decidibilidade da teoria da Aritmética Real Não Linear (NRA) conforme definida formalmente no padrão SMTLIB. Embora a teoria dos corpos reais fechados (composta por igualdades e desigualdades sobre polinômios) seja um fragmento bem estabelecido da lógica matemática e seja decidível (Tarski [7]), a definição de NRA no SMTLIB estende essa assinatura para incluir divisão. A questão crítica surge do tratamento da divisão por zero. No padrão SMTLIB, a divisão é interpretada conforme o esperado para divisores não nulos, mas permanece uma função não interpretada quando o divisor é zero. Especificamente, o axioma $(\forall x, y \in \mathbb{R}) (y \neq 0) \Rightarrow (x = \frac{x}{y} \cdot y)$ permite qualquer valor para $\frac{x}{0}$ , desde que o comportamento padrão seja mantido em outros casos. O artigo investiga se esse tratamento específico da divisão por zero preserva a decidibilidade da teoria.

Metodologia
O autor emprega uma prova de redução para demonstrar a indecidibilidade. A metodologia procede em duas etapas lógicas:

Redução da Aritmética Inteira: O artigo estabelece primeiro que a aritmética real aumentada com uma única função unária não interpretada é indecidível. Isso é alcançado ao axiomatizar a função não interpretada $f$ $f$ para se comportar como a função piso $\lfloor \cdot \rfloor$ $⌊ \cdot ⌋$ usando os axiomas:
- $(\forall x \in \mathbb{R}) f(x) + 1 = f(x + 1)$
- $(\forall x \in \mathbb{R}) (0 \le x < 1) \Rightarrow (f(x) = 0)$
  Ao impor esses axiomas, qualquer fórmula sobre variáveis inteiras pode ser equissatisfatível a uma fórmula sobre variáveis reais envolvendo $f$ . Como a aritmética inteira é indecidível (10º Problema de Hilbert [4]), a teoria de aritmética real estendida torna-se indecidível.
Mapeamento para Divisão por Zero: O artigo então mapeia a função não interpretada $f$ da etapa anterior diretamente para a operação de divisão por zero ( $\frac{x}{0}$ ). Ao tratar $\frac{x}{0}$ como a função não interpretada, os axiomas necessários para simular a função piso podem ser codificados dentro da teoria NRA. Consequentemente, a satisfatibilidade de fórmulas inteiras arbitrárias pode ser reduzida à satisfatibilidade de fórmulas NRA envolvendo divisão por zero.

Principais Contribuições e Resultados

Prova de Indecidibilidade: O resultado primário é a demonstração de que a teoria SMTLIB da Aritmética Real Não Linear (NRA) é indecidível. Isso é uma consequência direta da inclusão da divisão onde o divisor é uma função não interpretada em zero.
Mecanismo de Codificação: O artigo fornece uma codificação concreta (Exemplo 1) mostrando como traduzir a satisfatibilidade de equações diofantinas (por exemplo, $a^3 + b^3 = c^3$ sobre inteiros) em fórmulas NRA. Isso é feito ao afirmar que as variáveis atuam como inteiros via simulação da função piso usando $\frac{x}{0}$ , e então aplicando as restrições polinomiais.
Impacto em Benchmarks Existentes: A análise revela que, embora muitos benchmarks na categoria NRA do SMTLIB usem divisão apenas com divisores constantes (um fragmento decidível), aqueles que utilizam divisores não constantes caem no fragmento indecidível recém-identificado.

Significância e Alegações
O artigo alega que este resultado é "inesperado", dado que o fragmento decidível de restrições polinomiais é um resultado marcante na lógica matemática. A significância reside em esclarecer os limites teóricos do padrão SMTLIB: a inclusão da divisão como uma função não interpretada em zero altera fundamentalmente o panorama da decidibilidade, tornando a teoria completa indecidível.

O autor observa que essa limitação impede a extensão de técnicas completas de eliminação de quantificadores (como as usadas em CAD ou abordagens de eliminação de quantificadores preguiçosas [3, 5, 6]) para a teoria NRA completa na presença de divisão por zero.

Mitigações Propostas
O artigo conclui delineando duas abordagens potenciais para abordar essa indecidibilidade, sem alegar ter resolvido o problema dentro do padrão atual:

Divisão Total: Atribuir um valor específico à divisão por zero (semelhante à teoria de vetores de bits [1]), embora isso apresente desafios na seleção de um valor apropriado.
Separação de Teorias: Mover a divisão com divisores não constantes para uma teoria separada (proposta como UFNRA) e restringir a NRA a restrições polinomiais mais divisão por constantes não nulas. O autor reconhece que isso necessitaria de uma reclassificação dos benchmarks existentes.