Mechanized Undecidability of Higher-order beta-Matching (Extended Version)

Resumen Técnico: Indecidibilidad Mecanizada del Matching $\beta$ de Orden Superior

Planteamiento del Problema
El artículo aborda el problema de decisión del matching $\beta$ de orden superior dentro del cálculo $\lambda$ simplemente tipado. Dados dos términos $\lambda$ simplemente tipados, $F$ y $N$, donde $N$ no contiene variables libres, el problema consiste en determinar si existe un término $M$ tal que la aplicación $F M$ sea $\beta$-equivalente a $N$. Si bien la indecidibilidad de la unificación $\beta$ de orden superior fue establecida por Huet en la década de 1970, la decidibilidad del matching $\beta$ permaneció abierta hasta que Loader demostró su indecidibilidad en 2003. La prueba de Loader se basó en una reducción de una variante de la $\lambda$-definibilidad, utilizando una maquinaria intrincada para formular restricciones que especifican funciones finitas arbitrarias.

Metodología
El autor presenta una nueva prueba de indecidibilidad que difiere del enfoque de Loader al evitar por completo la $\lambda$-definibilidad. En su lugar, la prueba codifica una forma restringida de reescritura de cadenas, específicamente el Problema $0^+ \Rightarrow^* 1^+$ dentro de sistemas semi-Thue simples, directamente en el matching $\beta$ de orden superior.

La metodología procede a través de los siguientes pasos:

1. Punto de Partida: La reducción comienza con el Problema indecidible $0^+ \Rightarrow^* 1^+$, que pregunta si una secuencia no vacía de $0$s puede transformarse en una secuencia no vacía de $1$s utilizando un conjunto de reglas de reescritura de la forma $ab \Rightarrow cd$. Este problema ya es conocido por ser indecidible y está mecanizado en la Librería de Pruebas de Indecidibilidad de Coq.
2. Estrategia de Codificación: El autor construye términos $\lambda$ simplemente tipados para simular el proceso de reescritura. La codificación captura dos aspectos principales:
   • Expansión de Palabras e Inicialización: Se construyen términos para representar la expansión de una palabra inicial de longitud $n$ y su inicialización con $0$s.
   • Pasos de Reescritura: Los términos representan la aplicación de reglas de reescritura en posiciones específicas dentro de la palabra.
3. Restricciones Sintácticas y Semánticas: Para asegurar que la solución del término $\lambda$ represente fielmente el proceso de reescritura sin soluciones "ad hoc" (por ejemplo, términos que ignoran argumentos o construyen resultados arbitrariamente), el autor emplea restricciones de tipado específicas y comprobaciones de $\beta$-equivalencia.
   • Restricciones Sintácticas: Al utilizar una variable libre $u$ y el término identidad $I$ en contextos específicos (inspirados en Dowek y Urzyczyn), el autor restringe la forma de las posibles soluciones a términos "bien formados". Esto evita que las soluciones introduzcan abstracciones $\lambda$ innecesarias o ignoren los argumentos proporcionados.
   • Restricciones Semánticas: El autor define un conjunto de términos tipados ($G_\star, G_0, G_{ab \Rightarrow cd}$) que actúan como intérpretes para las reglas de reescritura. Estos términos se utilizan en las restricciones de $\beta$-equivalencia para verificar que una solución candidata simula correctamente la transición de una secuencia de $0$s a una secuencia de $1$s.
4. Mecanización: Toda la prueba se ha mecanizado en el Probador Rocq (anteriormente Coq). La mecanización es libre de axiomas y abarca aproximadamente 4,000 líneas de código, cubriendo la definición del cálculo $\lambda$ simplemente tipado, la lógica de reducción y el resultado final de indecidibilidad.

Contribuciones Clave

• Reducción Novedosa: El artículo proporciona una nueva reducción desde el Problema $0^+ \Rightarrow^* 1^+$ al matching $\beta$ de orden superior. Esto evita la compleja maquinaria de la $\lambda$-definibilidad utilizada en pruebas anteriores.
• Simplificación de la Verificación: Debido a la simplicidad de los sistemas semi-Thue subyacentes y la naturaleza estructurada de la codificación, se argumenta que la prueba es más sencilla de verificar en detalle completo en comparación con los enfoques de Loader o Joly.
• Construcción Uniforme: El enfoque identifica una construcción uniforme que demuestra la indecidibilidad de tres problemas relacionados: el matching $\beta$ de orden superior, la inhabitación de tipos de intersección y la $\lambda$-definibilidad. El artículo vincula explícitamente la construcción de matching $\beta$ con las interpretaciones de la teoría de modelos finitos utilizadas en las pruebas de inhabitación de tipos de intersección.
• Reducción Certificada: El trabajo produce una reducción de muchos-a-uno certificada desde el Problema de la Parada al matching $\beta$ de orden superior, dado que la indecidibilidad del problema de reescritura inicial ya está certificada en el Probador Rocq.

Resultados

• Teorema: El matching $\beta$ de orden superior es indecidible.
• Orden de la Indecidibilidad: La reducción construida demuestra la indecidibilidad en el orden de tipo 6. Esto se alinea con el resultado de Loader de que el matching $\beta$ es indecidible en el orden 6. El artículo señala que, aunque Loader conjeturó que el orden 5 podría ser suficiente, ni la técnica de Loader ni el presente enfoque se aplican en el orden 5, dejando la decidibilidad del orden 5 como una pregunta abierta.
• Mecanización: La prueba ha sido contribuida con éxito a la Librería de Pruebas de Indecidibilidad de Coq existente, asegurando que el resultado esté libre de las ambigüedades que a menudo presentan las pruebas manuales.

Significancia
El artículo reclama significancia principalmente a través de la mecanización y simplificación de la prueba de indecidibilidad. Al desplazar el punto de partida de la $\lambda$-definibilidad hacia un problema restringido de reescritura de cadenas, el autor logra una prueba que es más propicia para la verificación formal. El trabajo complementa los resultados mecanizados existentes sobre la unificación $\beta$ de orden superior. Además, el enfoque resalta una profunda conexión estructural entre el matching $\beta$ de orden superior, la inhabitación de tipos de intersección y la $\lambda$-definibilidad, sugiriendo que estos problemas comparten un mecanismo subyacente común para la indecidibilidad basado en la simulación de propiedades de la teoría de modelos finitos mediante términos $\lambda$. El autor enfatiza que la prueba fue desarrollada interactivamente con el asistente de pruebas, apoyándose en un análisis exhaustivo de casos para asegurar la corrección, minimizando así el riesgo de error humano en la compleja construcción lógica.