💻 computer science

Nonlinear Arithmetic with SMTLIB Division is Undecidable

El artículo demuestra que la aritmética real no lineal (NRA) tal como se define en el estándar SMTLIB es indecidible porque su tratamiento de la división por cero como una función no interpretada permite la codificación de problemas de aritmética entera indecidibles.

Autores originales: Dejan Jovanovic

Publicado 2026-05-27

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Dejan Jovanovic

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que eres un detective tratando de resolver un misterio usando un conjunto de reglas muy estrictas. En el mundo de la informática, estas reglas se llaman "teorías", y ayudan a las computadoras a decidir si un rompecabezas matemático tiene solución o no.

Este artículo trata sobre un conjunto específico de reglas llamado Aritmética Real No Lineal (NRA). Piensa en esto como un juego jugado con números reales (como 3.14, -5 o 0.001) donde puedes sumarlos, restarlos, multiplicarlos y divididos.

La regla "mágica" que rompe el juego

Durante mucho tiempo, los matemáticos creyeron que este juego era perfectamente resoluble. Si le dabas a una computadora un rompecabezas usando estos números, eventualmente podía decir: "Sí, hay una solución", o "No, no la hay".

Sin embargo, el autor, Dejan Jovanović, descubrió una trampa oculta en el libro de reglas oficial (el estándar SMTLIB). La trampa está en cómo las reglas manejan la división por cero.

En matemáticas normales, dividir por cero es un gran "No". Pero en este libro de reglas informático específico, las reglas dicen: "Si divides por cero, no nos importa cuál sea la respuesta. Puede ser cualquier cosa, siempre que actúe como un número normal cuando no estás dividiendo por cero".

El autor llama a esto una "función no interpretada". Para usar una analogía: Imagina una máquina expendedora que funciona perfectamente para cada snack que compras. Pero si intentas comprar un "Snack Cero", la máquina no se bloquea; en su lugar, simplemente expulsa algo —quizás una barra de chocolate, quizás una piedra, quizás una nube. Las reglas no te dicen qué será; solo dicen: "Será algo".

Cómo esto vuelve el juego irresoluble

El artículo argumenta que esta regla de "vale todo" para la división por cero es la llave que abre una puerta al caos.

Aquí está la lógica, simplificada:

El objetivo: El autor quiere probar que si tienes esta regla "mágica" de división, puedes engañar a la computadora para que resuelva rompecabezas de enteros (rompecabezas con números enteros como 1, 2, 3).
El problema: Resolver rompecabezas de enteros es famosamente imposible para que las computadoras lo hagan perfectamente para cada caso (esto se conoce como el Décimo Problema de Hilbert). Es como intentar encontrar una aguja en un pajar que sigue creciendo para siempre.
El truco: El autor muestra que al usar la "magia" de la división por cero, puedes construir un puente matemático. Puedes tomar un rompecabezas de enteros difícil y traducirlo a un rompecabezas de números reales usando este truco de división.
- Analogía: Imagina que tienes un código secreto escrito en un idioma que solo entienden los humanos (enteros). Construyes una máquina (el truco de división) que traduce este código a un idioma que las computadoras entienden (números reales). Debido a que el idioma de la computadora tiene esta regla "mágica" de división por cero, la computadora puede accidentalmente resolver el código humano.
El resultado: Dado que sabemos que las computadoras no pueden resolver todos los rompecabezas de enteros, y este truco les permite intentar resolver rompecabezas de enteros usando números reales, significa que la computadora no puede resolver todos los rompecabezas de números reales tampoco. El juego se vuelve indecidible.

La analogía de la función "piso"

Para probar esto, el autor usa un truco ingenioso. Muestra que si tienes esta división "mágica", puedes obligar a la computadora a actuar como una función piso (una función que redondea un número hacia abajo al entero más cercano, como convertir 3.9 en 3).

Una vez que la computadora puede redondear números hacia abajo, puede comenzar a contar enteros. Una vez que puede contar enteros, puede intentar resolver esos rompecabezas de enteros imposibles. Dado que esos rompecabezas son imposibles de resolver en general, todo el sistema de matemáticas de números reales con esta regla de división se vuelve imposible de resolver en general.

Qué significa esto para el mundo real (según el artículo)

El artículo no habla de IA futura ni de usos médicos. Se centra en el estado actual de las pruebas de referencia informáticas (problemas de prueba):

La trampa: Muchos problemas de prueba existentes en la biblioteca SMTLIB (una enorme colección de rompecabezas matemáticos utilizados para probar computadoras) usan división con variables (como x / y). Si y resulta ser cero, estos rompecabezas caen en la trampa "indecidible".
¿La solución? El autor sugiere dos formas de arreglar el libro de reglas:
1. Elegir una respuesta específica: Decidir que dividir por cero siempre es igual a un número específico (como 0 o 1), tal como lo hacen algunos sistemas informáticos con números binarios.
2. Dividir el juego: Crear una nueva categoría separada para problemas donde divides por variables, y mantener la categoría "segura" para problemas donde solo divides por números conocidos (constantes).

La conclusión

El artículo afirma que una regla específica, aparentemente inofensiva, sobre cómo las computadoras manejan la "división por cero" rompe accidentalmente la capacidad de las computadoras para resolver todos los problemas matemáticos que involucran números reales. Convierte un juego resoluble en uno irresoluble al permitir que la computadora resuelva sigilosamente problemas que no se suponía que podía resolver.

Resumen Técnico: La Aritmética No Lineal con División en SMTLIB es Indecidible

Enunciado del Problema
El artículo aborda el estado de decidibilidad de la teoría de la Aritmética Real No Lineal (NRA) tal como se define formalmente en el estándar SMTLIB. Si bien la teoría de los cuerpos reales cerrados (que comprende igualdades y desigualdades sobre polinomios) es un fragmento bien establecido y decidible de la lógica matemática (Tarski [7]), la definición de NRA en SMTLIB extiende esta firma para incluir la división. La cuestión crítica surge del tratamiento de la división por cero. En el estándar SMTLIB, la división se interpreta como se espera para divisores distintos de cero, pero permanece como una función no interpretada cuando el divisor es cero. Específicamente, el axioma $(\forall x, y \in \mathbb{R}) (y \neq 0) \Rightarrow (x = \frac{x}{y} \cdot y)$ permite cualquier valor para $\frac{x}{0}$ siempre que se mantenga el comportamiento estándar en otros lugares. El artículo investiga si este tratamiento específico de la división por cero preserva la decidibilidad de la teoría.

Metodología
El autor emplea una prueba de reducción para demostrar la indecidibilidad. La metodología procede en dos pasos lógicos:

Reducción desde la Aritmética Entera: El artículo establece primero que la aritmética real aumentada con una única función unaria no interpretada es indecidible. Esto se logra axiomatizando la función no interpretada $f$ $f$ para que se comporte como la función parte entera $\lfloor \cdot \rfloor$ $⌊ \cdot ⌋$ utilizando los 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)$
  Al hacer cumplir estos axiomas, cualquier fórmula sobre variables enteras puede ser equisatisfacible con una fórmula sobre variables reales que involucre $f$ . Dado que la aritmética entera es indecidible (el décimo problema de Hilbert [4]), la teoría de aritmética real extendida se vuelve indecidible.
Mapeo a la División por Cero: El artículo luego mapea la función no interpretada $f$ del paso anterior directamente a la operación de división por cero ( $\frac{x}{0}$ ). Al tratar $\frac{x}{0}$ como la función no interpretada, los axiomas requeridos para simular la función parte entera pueden codificarse dentro de la teoría NRA. En consecuencia, la satisfacibilidad de fórmulas enteras arbitrarias puede reducirse a la satisfacibilidad de fórmulas NRA que involucran división por cero.

Contribuciones y Resultados Clave

Prueba de Indecidibilidad: El resultado principal es la demostración de que la teoría SMTLIB de la Aritmética Real No Lineal (NRA) es indecidible. Esto es una consecuencia directa de incluir la división donde el divisor es una función no interpretada en cero.
Mecanismo de Codificación: El artículo proporciona una codificación concreta (Ejemplo 1) que muestra cómo traducir la satisfacibilidad de ecuaciones diofánticas (por ejemplo, $a^3 + b^3 = c^3$ sobre enteros) a fórmulas NRA. Esto se hace afirmando que las variables actúan como enteros mediante la simulación de la función parte entera usando $\frac{x}{0}$ , y luego aplicando las restricciones polinómicas.
Impacto en los Conjuntos de Pruebas Existentes: El análisis revela que, aunque muchos conjuntos de pruebas en la categoría NRA de SMTLIB utilizan división solo con divisores constantes (un fragmento decidible), aquellos que utilizan divisores no constantes caen en el fragmento indecidible recién identificado.

Significado y Afirmaciones
El artículo afirma que este resultado es "inesperado" dado que el fragmento decidible de restricciones polinómicas es un resultado histórico en la lógica matemática. El significado radica en clarificar los límites teóricos del estándar SMTLIB: la inclusión de la división como una función no interpretada en cero altera fundamentalmente el panorama de la decidibilidad, haciendo que la teoría completa sea indecidible.

El autor señala que esta limitación impide la extensión de técnicas completas de eliminación de cuantificadores (como las utilizadas en CAD o enfoques de eliminación de cuantificadores perezosos [3, 5, 6]) a la teoría NRA completa en presencia de división por cero.

Mitigaciones Propuestas
El artículo concluye delineando dos enfoques potenciales para abordar esta indecidibilidad, sin afirmar haber resuelto el problema dentro del estándar actual:

División Total: Asignar un valor específico a la división por cero (similar a la teoría de vectores de bits [1]), aunque esto presenta desafíos en la selección de un valor apropiado.
Separación de Teorías: Mover la división con divisores no constantes a una teoría separada (propuesta como UFNRA) y restringir NRA a restricciones polinómicas más división por constantes no nulas. El autor reconoce que esto requeriría reclasificar los conjuntos de pruebas existentes.