💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

Este artículo en desarrollo introduce una táctica de coincidencia de patrones automática para Autosubst que aborda sus limitaciones actuales en el manejo de reglas de tipado, relaciones de reducción y soluciones no únicas, tal como se demuestra mediante evaluaciones en los desafíos POPLMark y POPLMark Reloaded.

Autores originales: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

Publicado 2026-07-15

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

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 intentando resolver un rompecabezas gigante y mágico donde cada pieza tiene una etiqueta oculta. En el mundo de la informática, estas etiquetas se llaman "índices de De Bruijn". Son una forma ingeniosa de llevar la cuenta de las variables en el código, pero son notoriamente complicadas. Piensa en ellas como un juego de sillas musicales donde las sillas (las variables) siguen cambiando de nombre cada vez que alguien se sienta. Si intentas encajar una pieza del rompecabezas (una regla) en un hueco (un objetivo), las piezas a menudo parecen diferentes aunque sean en realidad las mismas, solo que llevan sombreros distintos.

Durante mucho tiempo, una herramienta llamada Autosubst ha sido el héroo de esta historia. Es como un robot superinteligente que puede decirte instantáneamente si dos piezas del rompecabezas son iguales, incluso si sus etiquetas han sido barajadas. Lo logra utilizando un conjunto de reglas mágicas (llamadas $\sigma$ -cálculo) para normalizar las piezas hasta que se vean idénticas. Si solo quieres comprobar si dos cosas son iguales, este robot es perfecto.

El Problema: La Trampa del "Apply"
Sin embargo, hay un inconveniente. Cuando intentas usar estas piezas del rompecabezas para resolver un problema aplicando una regla (como usar un botón de "Aplicar" en un videojuego), el robot se queda bloqueado. Es excelente diciendo "Sí, estas son iguales", pero es pésimo diciendo "Aquí tienes cómo encajar esta regla en este hueco específico".

¿Por qué? Porque a veces, una regla puede encajar en un hueco de múltiples maneras, y el robot no sabe cuál es la "correcta" sin ayuda. En el pasado, los programadores humanos tenían que hacer el trabajo pesado. Tenían que reescribir sus reglas de formas extrañas e indirectas o adivinar manualmente las etiquetas faltantes solo para que el robot funcionara. Era como intentar forzar una pieza cuadrada en un hueco redondo lijando la pieza tú mismo, en lugar de simplemente encontrar la herramienta adecuada.

La Nueva Idea: Una Táctica de Adivinación Inteligente
Este artículo presenta una nueva herramienta llamada as_apply. Piensa en esto como un nuevo brazo robótico, ligeramente más aventurero, diseñado para agarrar esas piezas del rompecabezas e intentar meterlas en los huecos, incluso cuando las etiquetas no coinciden perfectamente a primera vista.

En lugar de rendirse o pedir al humano que reescriba todo, esta nueva táctica utiliza un conjunto de heurísticas (que son básicamente conjeturas educadas basadas en patrones que ha visto antes). Mira el hueco, mira la regla y dice: "¡Apuesto a que si muevo estas etiquetas solo un poquito, encajarán!".

Cómo Funciona (El Truco de Magia)
El proceso ocurre en dos pasos:

Preparación: El robot primero limpia las piezas del rompecabezas usando las reglas fiables de la antigua Autosubst para que queden lo más ordenadas posible.
El Juego de Adivinación: Luego intenta encajar las piezas. Si las piezas no coinciden perfectamente, no entra en pánico. En su lugar, intenta algunos trucos específicos:
- Comprueba si el desajuste es solo un simple "desplazamiento" (como mover una variable un lugar hacia arriba).
- Comprueba si la pieza faltante es solo una "identidad" (no hacer nada).
- Busca patrones comunes que suelen ocurrir en estos rompecabezas.

Si una de estas conjeturas funciona, rellena las etiquetas faltantes y continúa. Si falla, retrocede y prueba una conjetura diferente.

Lo que el Artículo Dice (y lo que No Dice)
Los autores son muy cuidadosos de no exagerar sus logros. Admiten que esto no es una varita mágica que resuelve todos los posibles rompecabezas posibles.

No es perfecto: El artículo establece explícitamente que, a veces, un rompecabezas puede tener múltiples soluciones, y este robot podría elegir la incorrecta. Es posible construir un ejemplo complicado donde el robot adivine mal, incluso si existe una respuesta correcta.
Es un "Trabajo en Progreso": Los autores describen esto como un método de "trabajo en progreso". No pretenden haber resuelto toda la teoría de la correspondencia para siempre.
Los Resultados: Probaron esta nueva táctica en dos desafíos famosos y difíciles llamados POPLMark y POPLMark Reloaded. Estos son como las "Olimpiadas" de demostrar cosas sobre lenguajes de programación.
- En el desafío POPLMark (642 líneas de código), usaron la nueva táctica 15 veces.
- En el desafío POPLMark Reloaded (683 líneas de código), la usaron 10 veces.
- En cada uno de estos casos, la táctica resolvió el objetivo con éxito.

El Veredicto
El artículo sugiere que, si bien esta táctica tiene límites teóricos (podría confundirse con rompecabezas muy extraños o adversos), funciona sorprendentemente bien en el mundo real. Permite a los programadores dejar de reescribir sus reglas de formas extrañas e indirectas y simplemente escribirlas de forma natural.

Los autores se muestran optimistas pero cautelosos. Sugieren que este enfoque podría reemplazar la vieja y torpe forma de hacer las cosas en muchos casos prácticos, pero saben que aún queda trabajo por hacer para asegurar que el robot nunca, jamás, elija la solución incorrecta. Actualmente están trabajando para determinar exactamente qué tipos de rompecabezas puede resolver este robot con un 100% de certeza, y cuáles podrían seguir requiriendo que un humano verifique el trabajo.

En resumen: es una herramienta nueva, ingeniosa y útil que hace que el desordenado trabajo de encajar piezas sea mucho más fácil, aunque no esté lista del todo para ser la única herramienta en la caja.

Resumen Técnico: Una Táctica para el Coincidencia de Patrones en Autosubst

Planteamiento del Problema
El artículo aborda una limitación específica en el marco de trabajo Autosubst, un generador de código para el asistente de pruebas Rocq (anteriormente Coq) que automatiza el razonamiento sobre términos de de Bruijn y la sustitución mediante el $\sigma$ -cálculo. Si bien Autosubst automatiza con éxito la comprobación de igualdad para objetivos sin suposiciones mediante la táctica asimpl, falla cuando los usuarios intentan aplicar suposiciones (por ejemplo, reglas de tipado o lemas) a un objetivo mediante tácticas estándar como apply o eapply.

En estos escenarios, el usuario debe unificar un objetivo con una suposición módulo $\sigma$ -equivalencia. Sin embargo, la automatización de Autosubst no está diseñada para realizar coincidencias contra suposiciones. En consecuencia, los usuarios se ven obligados a emplear soluciones de trabajo engorrosas, tales como:

Formular reglas en formas indirectas (utilizando variables meta nuevas en lugar de términos de sustitución directos).
Introducir lemas auxiliares para cerrar la brecha entre el objetivo y la suposición.
Transformar manualmente los objetivos o instanciar explícitamente variables existenciales durante las pruebas.

La dificultad central radica en que la coincidencia $\sigma$ (coincidencia hasta $\sigma$ -equivalencia) no es única; un único problema de coincidencia puede admitir múltiples soluciones, no todas las cuales satisfacen las premisas del contexto. Además, la coincidencia de segundo orden para el $\lambda\sigma$ -cálculo completo es indecidible e, incluso sin la reducción $\beta$ , las soluciones no son necesariamente únicas.

Metodología
Los autores proponen una táctica heurística en fase de desarrollo llamada as_apply, implementada en el lenguaje Ltac de Rocq, para automatizar la coincidencia de patrones módulo $\sigma$ -equivalencia. La táctica opera en dos fases principales:

Preprocesamiento:
- Tanto el objetivo como la conclusión de la suposición objetivo se normalizan con respecto al $\sigma$ -cálculo utilizando la táctica existente asimpl.
- Las variables cuantificadas en la suposición se reemplazan con variables existenciales (evars).
- Las premisas de la suposición se convierten en subobjetivos para ser resueltos tras la fase de coincidencia.
- La táctica gestiona las conversiones entre operaciones de renombramiento explícito (p. ej., $s\langle\xi\rangle$ ) y operaciones de instanciación ( $s[\xi]$ ) utilizando substify y renamify.
Fase de Coincidencia:
- La táctica construye un conjunto de ecuaciones de coincidencia $M = \{s_i =_\sigma t_i\}$ entre los términos del objetivo y los términos de la suposición instanciados.
- Procesa las ecuaciones de izquierda a derecha mediante un procedimiento parcial, $\sigma_{min}$ , que intenta realizar la coincidencia módulo el fragmento $\sigma_{min}$ (un subconjunto de reglas $\sigma$ que caracteriza la instanciación y la composicionalidad).
- Heurísticas: Si $\sigma_{min}$ $σ_{min}$ falla al encontrar una coincidencia, la táctica aplica un conjunto de heurísticas que capturan patrones comunes en desarrollos formales. Estas incluyen:
  - El manejo de ecuaciones de la forma $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ mediante la instanciación de lo desconocido con una sustitución elevada ( $?s \mapsto s[\Uparrow\sigma]$ ).
  - El manejo de casos que involucran sustituciones de identidad o estructuras de variables específicas.
- Tras aplicar las sustituciones, la táctica renormaliza la suposición. El éxito se determina si el objetivo y la suposición se vuelven sintácticamente iguales.

La táctica se ha generalizado para soportar el lenguaje de entrada completo del compilador Autosubst, incluyendo múltiples tipos inductivos mutuos, sustituciones de vectores y renombramientos de primera clase.

Contribuciones Clave

Introducción de as_apply: Una táctica heurística diseñada para reemplazar apply/eapply en desarrollos basados en Autosubst, permitiendo la coincidencia módulo $\sigma$ -equivalencia en presencia de suposiciones.
Generalización: Extensión de la lógica de coincidencia para cubrir toda la sintaxis soportada por Autosubst, incluyendo ligadores complejos y operaciones de renombramiento.
Evaluación Empírica: Aplicación de la táctica a bancos de pruebas estándar, específicamente los desafíos POPLMark y POPLMark Reloaded.

Resultados
Los autores evaluaron as_apply en las soluciones de los desafíos POPLMark (642 líneas) y POPLMark Reloaded (683 líneas).

Frecuencia de Uso: La táctica se utilizó 15 veces en la solución de POPLMark B y 10 veces en la solución de POPLMark Reloaded.
Efectividad: En todos los casos probados, as_apply resolvió con éxito los objetivos previstos.
Simplificación: El uso de la táctica eliminó la necesidad de las formulaciones de reglas indirectas, los lemas auxiliares y las transformaciones manuales de objetivos que caracterizaban a las soluciones anteriores.
Limitaciones: Los autores reconocen que as_apply no es $\sigma$ -completa y no es un decisor. Debido a que la coincidencia $\sigma$ puede tener múltiples soluciones, la naturaleza heurística de la táctica significa que teóricamente podría seleccionar una solución incorrecta cuando existe una correcta, aunque no se observaron tales fallos en los casos de estudio.

Significancia y Reivindicaciones
El artículo sostiene que, si bien el problema teórico de la coincidencia $\sigma$ es inherentemente difícil (soluciones no únicas, indecidibilidad en el $\lambda\sigma$ completo), un enfoque pragmático y heurístico puede recuperar un alto nivel de automatización en la práctica. La significancia reside en reducir la carga manual de los usuarios que trabajan con la sintaxis de de Bruijn, permitiéndoles enunciar reglas de tipado y lemas en sus formas directas y naturales, en lugar de en formas indirectas adaptadas a las limitaciones del motor de unificación del asistente de pruebas.

Los autores mantienen la modestia sobre el estado actual del trabajo, calificándolo como "Trabajo en Progreso". Señalan que la táctica actual depende de heurísticas debido al potencial de soluciones infinitas o múltiples. El trabajo futuro apunta a identificar el fragmento $\sigma'$ más grande para el cual se cumple un criterio de unicidad, lo que potencialmente conduciría a una táctica de coincidencia con garantías probadas.

Más como este