The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness

Este artículo demuestra mediante verificación formal en Lean 4 la imposibilidad de probar la terminación de recursores duplicadores de pasos mediante medidas composicionales globales, identificando que los métodos basados en proyección superan esta barrera y validando un certificado completo de normalización fuerte y confluencia para un fragmento seguro del sistema.

Lo esencial

Imagina que estás intentando probar que un sistema de reglas para ordenar bloques de construcción (como un Lego muy complejo) siempre termina y nunca se queda en un bucle infinito.

Este artículo, escrito por Moses Rahnama, cuenta la historia de un obstáculo invisible que aparece cuando intentas medir el progreso de estas reglas de una manera "global" (mirando todo el bloque de una sola vez), y cómo una técnica diferente logra saltar ese obstáculo.

Aquí tienes la explicación sencilla, usando analogías:

1. El Problema: El "Truco del Duplicador"

Imagina que tienes una regla mágica en tu juego de bloques llamada "Recursor". Esta regla dice:

"Si tienes una torre de altura n, construye una nueva torre que tenga la misma pieza de trabajo s dos veces: una vez al principio y otra vez dentro de la nueva torre."

La regla se ve así: Recursor(s, n) → Pieza(s) + Recursor(s, n-1).

El problema es que la pieza s se duplica. Si s es un bloque gigante, ahora tienes dos bloques gigantes.

2. El Muro de la Orientación Global (El fallo de los métodos directos)

Los investigadores probaron dos formas de medir si el juego termina:

• El Método del Contador Global (La "Báscula"): Imagina que intentas probar que el juego termina pesando todos los bloques. Si duplicas un bloque gigante (s), el peso total de la nueva torre aumenta o se mantiene igual, en lugar de disminuir.
  • La analogía: Es como si intentaras bajar de peso comiendo dos pasteles cada vez que haces ejercicio. No importa cuánto te muevas, si duplicas la comida, nunca pierdes peso.
  • El resultado: El artículo demuestra matemáticamente (y lo verificó una computadora llamada Lean) que es imposible usar este tipo de "báscula global" para probar que el juego termina cuando hay duplicación. La duplicación engaña a la báscula.

3. La Salida: El "Gafas de Rayos X" (El Método Modular)

Entonces, ¿cómo sabemos que el juego termina si la báscula falla? Usamos una técnica llamada Pares de Dependencia (DP).

• La analogía: Imagina que en lugar de pesar toda la torre, te pones unas gafas de rayos X que te permiten ignorar los bloques que no importan para el progreso.
• En nuestro juego, la pieza s (la que se duplica) está atrapada dentro de un contenedor inerte (llamado app). No importa cuánto se duplique, esa pieza s nunca vuelve a ser usada para contar la altura de la torre. Solo importa la parte que cuenta hacia atrás (n).
• El truco: El método modular ignora la pieza duplicada (s) y solo mira la parte que disminuye (n). Al ignorar el "ruido" de la duplicación, ven claramente que la torre se hace más pequeña paso a paso.
• Resultado: ¡El juego termina! La computadora TTT2 lo verificó en menos de un segundo usando este método.

4. La Prueba de Fuego: KO7

Para demostrar esto, los autores crearon un sistema mínimo llamado KO7.

• Es como un laboratorio de pruebas con solo 7 tipos de bloques y 8 reglas.
• Es lo suficientemente pequeño para que una computadora pueda revisar cada detalle, pero lo suficientemente complejo para tener el "truco del duplicador".
• Lo que descubrieron:
  1. Si intentas probarlo mirando todo junto (global), fallas.
  2. Si usas las "gafas de rayos X" (módulo), funciona.
  3. Si quitas la duplicación (haces que la pieza s no se copie), la báscula global vuelve a funcionar. ¡Esto confirma que el duplicador es el único culpable!

5. El "Cofre de Seguridad" (SafeStep)

Aunque el juego termina, tiene un pequeño defecto: a veces, dependiendo de cómo caigan los bloques, podrías llegar a dos estados finales diferentes (no es único).

• Para arreglarlo, los autores crearon una versión "segura" del juego (SafeStep) donde añadieron algunas reglas de seguridad (guardas) para evitar esos conflictos.
• En esta versión segura, demostraron que:
  • Siempre termina.
  • Siempre llega al mismo resultado final (es único).
  • Crearon un "robot normalizador" certificado que puede resolver cualquier configuración de bloques y decirte exactamente cómo quedará al final.

Resumen en una frase

El artículo demuestra que cuando una regla duplica piezas, las herramientas de medición tradicionales se vuelven ciegas (no pueden probar que termina), pero las herramientas inteligentes que ignoran el ruido (métodos modulares) pueden ver claramente que el sistema es seguro y termina, y han construido un robot certificado para resolverlo.

Es como si te dijeran: "No intentes contar cada grano de arena en una tormenta de arena para ver si la tormenta termina; ignora la arena que gira sin sentido y solo cuenta la dirección del viento, y verás que la tormenta se calmará."

Resumen técnico

A continuación presento un resumen técnico detallado del artículo "The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness" de Moses Rahnama (Mina Analytics, febrero de 2026).

1. El Problema: La Barrera de Orientación Global

El artículo aborda un problema fundamental en la teoría de sistemas de reescritura de términos (TRS) de primer orden: la dificultad de probar la terminación (normalización fuerte) en sistemas que contienen recursores con duplicación de pasos (step-duplicating recursors).

• El Escenario: Se considera un sistema con recursión donde un argumento de paso ($s$) se duplica en la regla de reescritura (aparece dos veces en el lado derecho), pero este argumento está "atrapado" dentro de un constructor inerte (como app) que no tiene reglas de reducción.
• La Paradoja: Aunque el sistema es terminante (la recursión avanza porque el contador de recursión disminuye), las medidas de terminación globales y composicionales (que asignan un valor numérico a todo el término sumando las contribuciones de sus subtérminos) fallan.
• La Causa Raíz: Cualquier medida que sea sensible a la duplicación (es decir, que sume el valor de los subtérminos) verá que el lado derecho de la regla duplica el peso del argumento $s$, impidiendo una disminución estricta estricta, a pesar de que la duplicación es semánticamente inerte (no afecta la lógica de recursión).

2. Metodología y Herramientas

El autor utiliza un enfoque híbrido que combina formalización mecánica rigurosa con validación externa:

• Cálculo Testigo (KO7): Se define un sistema de reescritura minimalista llamado KO7 (7 constructores, 8 reglas). Es lo suficientemente pequeño para ser formalizado completamente en un asistente de pruebas, pero lo suficientemente complejo para contener la estructura del problema (el "núcleo" de duplicación).
• Formalización en Lean 4:
  • Se formalizan dos clases de medidas composicionales directas (Tier 1: aditivas; Tier 2: abstractas con axiomas de subtérminos).
  • Se demuestra la imposibilidad de orientar la regla duplicadora con estas medidas.
  • Se prueba la normalización fuerte y la confluencia para una subrelación segura (SafeStep) mediante una medida lexicográfica triple computable.
  • Se verifica la confluencia mediante el Lema de Newman.
• Validación Externa (TTT2/CeTA):
  • Se utiliza la herramienta TTT2 (Tyrolean Termination Tool) para probar la terminación del sistema completo (sin guardas) utilizando el marco de Pares de Dependencia (DP) y el criterio de subtérmino.
  • CeTA certifica independientemente las pruebas generadas por TTT2.

3. Contribuciones Clave

A. Teorema de Imposibilidad Mecanizado

El artículo establece y prueba formalmente que ninguna medida composicional directa (dentro de las clases formalizadas) puede orientar estrictamente la regla del recursor duplicador para todas las instancias de términos.

• Tier 1 (Pesos Aditivos): Si app tiene un peso positivo, la duplicación de $s$ en el lado derecho hace que el valor total aumente o se mantenga igual, violando la terminación.
• Tier 2 (Funciones de Combinación Abstractas): Incluso con funciones de combinación arbitrarias, si se respetan los axiomas de que app domina a sus argumentos, la duplicación impide la orientación estricta.
• Ablación: Se demuestra que si se elimina la duplicación (haciendo el recursor lineal), las medidas simples (como el tamaño) funcionan inmediatamente, confirmando que la duplicación es la causa única de la barrera.

B. La "Escapa" Modular (Dependency Pairs)

El artículo identifica cómo los métodos modulares, específicamente el Marco de Pares de Dependencia (DP) con el criterio de subtérmino, evitan esta imposibilidad:

• Proyección: El método DP proyecta la atención únicamente al tercer argumento del recursor (el contador de recursión $n$), ignorando el argumento duplicado $s$.
• Invisibilidad de la Duplicación: Al tratar app como un constructor y descartar sus argumentos en el análisis de cadenas, la duplicación de $s$ se vuelve invisible para el análisis de terminación. Esto permite demostrar la terminación basándose únicamente en la disminución del contador $\delta(n) \to n$.

C. Certificación Completa del Fragmento Seguro (SafeStep)

Para el sistema restringido (SafeStep), que añade guardas para resolver conflictos de confluencia, el autor entrega una cadena de certificación completa:

1. Normalización Fuerte: Demostrada mediante una medida lexicográfica computable triple: $(\delta\text{-flag}, \kappa_M, \tau)$.
   • $\delta\text{-flag}$: Detecta el patrón de recursión.
   • $\kappa_M$: Orden multiconjunto de Dershowitz-Manna para manejar la duplicación.
   • $\tau$: Tamaño ponderado para resolver empates.
2. Confluencia: Probada aplicando el Lema de Newman (Normalización Fuerte + Confluencia Local). Se descarga completamente la hipótesis de unión local.
3. Normalizador Certificado: Se extrae una función de normalización total y correcta (sound) que garantiza un único forma normal.
4. Calibración Ordinal: Se establece una cota superior mecanizada por debajo de $\varepsilon_0$ (específicamente $\omega^\omega \cdot 2$) y una calibración de límite inferior en $\omega^\omega$.

D. Validación Empírica con TTT2

Se sometió el sistema completo (sin guardas) a TTT2:

• Éxito: Las estrategias basadas en Pares de Dependencia (DP) y Orden de Ruta Lexicográfica (LPO) probaron la terminación en menos de un segundo.
• Fallo: Todas las estrategias de interpretación global/composicional (Polinómica, KBO, Matricial) devolvieron MAYBE (fallo de búsqueda), lo cual es consistente con el teorema de imposibilidad mecanizado.

4. Resultados Principales

1. Existencia de una Barrera: Se ha identificado una frontera precisa entre métodos globales (que fallan) y modulares (que tienen éxito) para recursores con duplicación de pasos en sistemas sin ligadura (binders) y sin memoria externa.
2. Imposibilidad Formal: No existe una medida global composicional que funcione para este patrón de duplicación, independientemente de la complejidad de la medida, siempre que respete la sensibilidad a la duplicación.
3. Éxito de la Descomposición: El método de Pares de Dependencia con proyección es suficiente y necesario para superar la barrera, al "desechar" la masa duplicada irrelevante.
4. Artefacto Certificado: Se proporciona un artefacto de ~7,000 líneas de código en Lean 4 y certificados CeTA que validan la terminación, confluencia y normalización del sistema KO7.

5. Significado e Impacto

• Teórico: El trabajo clarifica las limitaciones de los métodos de ordenación de rutas (Path Orders) y medidas de tamaño globales en presencia de duplicación. Sugiere que la "complejidad" de la terminación en estos sistemas no es inherente a la lógica de recursión, sino a la forma en que las medidas globales "ven" la duplicación sintáctica.
• Práctico: Refuerza la necesidad de utilizar marcos modulares (como DP) en herramientas de terminación automática para sistemas que involucran duplicación de argumentos, incluso cuando la duplicación es semánticamente inocua.
• Metodológico: Demuestra la viabilidad de combinar pruebas de imposibilidad (qué no se puede probar) con pruebas de existencia (qué sí se puede probar) y certificación de normalizadores en un solo marco formalizado.

En resumen, el paper demuestra que la duplicación de pasos crea una "trampa" para las medidas globales, pero que una descomposición modular inteligente (ignorando la duplicación) permite resolver el problema de terminación de manera eficiente y certificada.