💻 computer science

Non-Termination of Logic Programs Using Patterns

Este artículo adapta un enfoque de reescritura de términos para la detección de la no terminación sin bucles a la programación lógica mediante la introducción de una nueva técnica de despliegue que genera patrones que representan conjuntos infinitos de secuencias de reescritura finitas, lo cual es evaluado experimentalmente utilizando la herramienta NTI.

Autores originales: Etienne Payet

Publicado 2026-08-10

📖 3 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Etienne Payet

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 estás observando a un robot intentar resolver un rompecabezas. A veces, el robot se queda atrapado en un bucle: hace el paso A, luego el paso B, luego el paso A de nuevo, otra vez, para siempre. Es como un hámster corriendo en una rueda; se está moviendo, pero no llega a ninguna parte. En el mundo de la informática, específicamente en un campo llamado Programación Lógica, estos robots son programas que intentan responder preguntas siguiendo un conjunto de reglas. Si un programa se queda atrapado en un bucle, nunca termina su trabajo, lo cual es un error que los programadores quieren detectar.

Pero existe un tipo de problema más complicado. A veces, un programa no se queda atrapado en un círculo repetitivo y ordenado. En su lugar, da un paso, luego un paso ligeramente diferente, luego un paso que parece casi igual pero no lo es del todo, y continúa así para siempre sin repetir jamás el mismo patrón exacto. Es como un bailarín que nunca repite un movimiento pero que tampoco deja de bailar. Esto se llama no terminación por no bucle (non-looping non-termination). Detectar estas secuencias infinitas y no repetitivas es un desafío increíble porque no hay un "bucle" obvio al cual señalar. Detectar estos bucles infinitos y no repetitivos es un gran desafío para los científicos de la computación que quieren demostrar que un programa eventualmente se detendrá o encontrar el punto de inicio específico que causa que se ejecute infinitamente.

Este artículo presenta una nueva y astuta forma de atrapar estos esquivos bucles infinitos no repetitivos. El autor, Etienne Payet, ha construido una herramienta llamada NTI que actúa como un detective superpoderoso para programas lógicos. En lugar de intentar observar al programa ejecutarse paso a paso (lo que tomaría una eternidad), la herramienta utiliza una técnica llamada desplegado (unfolding). Piensa en el desplegado como si estuvieras aplanando una compleja grulla de origami para ver el patrón de los pliegues debajo. Al aplanar las reglas del programa, la herramienta crea "patrones": planos abstractos que describen no solo un camino específico, sino una familia infinita de posibles caminos que el programa podría tomar.

El principal descubrimiento del artículo es que, mediante el uso de estos planos, específicamente una versión simplificada llamada "patrones simples", la herramienta puede demostrar matemáticamente que un programa se ejecutará para siempre sin quedarse atrapado en un bucle simple. El autor probó esto en 41 programas lógicos diferentes que se sabía que eran complicados. Su herramienta identificó con éxito los caminos infinitos y no repetitivos en muchos de ellos, incluyendo cuatro programas que ninguna otra herramienta existente había sido capaz de probar como no terminantes antes. Sin embargo, el artículo es honesto sobre sus límites: la herramienta no resolvió todos los casos, y para algunos programas, se quedó trabada o agotó el tiempo de espera tras ejecutarse durante 10 segundos. El autor sugiere que, si bien su método es una poderosa adición nueva al kit del detective, no es una varita mágica que resuelve todos los misterios todavía. Planean hacer la herramienta más inteligente en el futuro, con la esperanza de atrapar incluso más de estos complicados bucles infinitos no repetitivos.

Resumen Técnico: No Terminación de Programas Lógicos Mediante Patrones

Planteamiento del Problema
Este artículo aborda la detección automática de la no terminación en programas lógicos (LPs). Mientras que gran parte de la investigación existente se centra en la detección de bucles (secuencias de reescritura finitas que pueden repetirse indefinidamente), este trabajo se dirige a la no terminación sin bucles. Estas son secuencias de reescritura infinitas que no incorporan ningún bucle, lo que las hace inherentemente no periódicas y difíciles de detectar. El autor señala que tales secuencias pueden surgir de programas lógicos simples, y que los métodos estándar de detección de bucles a menudo fallan al identificarlas. La motivación es doble: teórica (estudiar formas notables de secuencias infinitas) y práctica (ayudar a los programadores a identificar consultas que se ejecutan indefinidamente).

Metodología
El autor adapta un enfoque introducido originalmente para la reescritura de términos por Emmes et al. (2012) al dominio de la programación lógica. La metodología central consiste en definir una nueva técnica de despliegue (unfolding) que genera "patrones" que describen conjuntos potencialmente infinitos de secuencias de reescritura finitas.

Definiciones de Patrones:
- Sustituciones de Patrones: Definidas como pares $\theta = (\sigma, \mu)$ , denotados como $\sigma \star \mu$ , que describen un conjunto de sustituciones $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$ .
- Términos de Patrón: Pares $(s, \theta)$ que describen el conjunto $\{s\theta(n) \mid n \in \mathbb{N}\}$ .
- Reglas de Patrón: Pares de términos de patrón $(p, q)$ que describen un conjunto de reglas binarias $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$ .
Corrección y Despliegue:
- Una regla de patrón se considera correcta con respecto a un programa $P$ si el conjunto de reglas que describe es un subconjunto del despliegue binario de $P$ ($binunf(P)$).
- El autor introduce un nuevo operador de despliegue $T^\pi_{P,B}$ que computa reglas de patrón a partir de un programa $P$ y un conjunto base de reglas de patrón correctas $B$ . Este operador utiliza un algoritmo de unificación para términos de patrón para combinar reglas, efectivamente "desplegando" el programa más rápido que el despliegue binario tradicional al capturar subconjuntos infinitos de $binunf(P)$ en representaciones finitas.
Patrones Simples y Unificación:
- Para hacer que el enfoque sea automatizable, el autor restringe el dominio a términos de patrón simples, donde las sustituciones siguen una estructura específica que involucra contextos unarios.
- Se proporciona un algoritmo de unificación para estos términos simples. Este mapea términos de patrón simples a términos sobre una firma especializada $\Upsilon$ (usando símbolos unarios $c_{a,b}$ para representar incrustaciones repetidas) y aplica algoritmos de unificación clásicos (por ejemplo, Robinson, Martelli-Montanari).
- El algoritmo se demuestra parcialmente correcto: si termina con éxito, produce un unificador más general (mgu) para las secuencias de patrones de entrada.
Criterios de No Terminación:
- Criterio General (Teorema 3): Adaptado de Emmes et al., establece que si el despliegue de patrones contiene una regla de la forma $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ donde $\sigma'$ conmuta con $\sigma$ y $\mu$ , entonces existe una cadena infinita.
- Criterio Especial (Teorema 5): Una condición más fácilmente verificable para las reglas de patrón especiales (un subconjunto de las reglas simples). Si tal regla existe en el despliegue, el artículo demuestra la existencia de una cadena infinita comenzando desde instancias específicas del lado izquierdo de la regla.

Contribuciones Clave
El artículo presenta cuatro contribuciones primarias:

Nueva Técnica de Despliegue: Un método para producir reglas de patrón correctas para la programación lógica, ofreciendo una presentación más compacta que las nueve reglas de inferencia utilizadas en la reescritura de términos y eliminando la necesidad de estrategias de aplicación complejas.
Términos de Patrón Simples y Unificación: La definición de una forma restringida de términos de patrón ("simples") y un algoritmo de unificación correspondiente demostrado como correcto.
Condición Suficiente Automatizable: Una condición fácilmente verificable (Teorema 5) para detectar la no terminación sin bucles a partir de reglas de patrón simples.
Implementación (NTI): La implementación de este enfoque en una herramienta llamada NTI.

Resultados Experimentales
El autor evaluó NTI en 41 programas lógicos derivados de Sistemas de Reescritura de Términos (TRS) no terminantes sin bucles de la Base de Datos de Problemas de Terminación (TPDB).

Éxito: La herramienta demostró con éxito la no terminación para 36 de los 41 programas. Notablemente, tuvo éxito en 4 programas (marcados con † en las tablas) que no habían sido demostrados como no terminantes por ningún otro analizador de TRS en la Competición Internacional de Terminación hasta 2024.
Fallo: El enfoque falló en 5 programas, principalmente debido a la incompletitud del algoritmo de unificación al usar la "elección natural" para los representantes de términos (como se discute en el Ejemplo 12) o la restricción a patrones simples (Ejemplo 9).
Rendimiento: Los tiempos de ejecución fueron generalmente bajos (menos de 300ms para los casos exitosos), aunque algunos casos complejos resultaron en tiempos de espera agotados (timeouts).

Significancia y Reivindicaciones
El autor afirma que su enfoque es la única herramienta que participa en la Competición Internacional de Terminación capaz de refutar la terminación de programas lógicos. Señala que existe otro enfoque por Payet (2024) para demostrar la no terminación sin bucles, pero este aborda una clase diferente de no bucle y es incapaz de refutar la terminación de los programas específicos probados en este artículo (Tablas 1 y 2). Por el contrario, el enfoque de Payet (2024) puede refutar la terminación de programas donde este método falla. Así, ambos enfoques se presentan como complementarios.

El artículo concluye modestamente, reconociendo que el algoritmo de unificación es actualmente incompleto y que la restricción a patrones simples limita su alcance (por ejemplo, al fallar en programas que requieren contextos de 1-variable). Se planea un trabajo futuro para abordar la completitud, extender el despliegue inicial de patrones (Prop. 2) y adaptar el enfoque a los TRS para una comparación directa con Emmes et al. (2012).

Más como este