Unification of Deterministic Higher-Order Patterns (Full Version)

Resumen Técnico: Unificación de Patrones de Orden Superior Deterministas

Enunciado del Problema
Este artículo aborda el problema de unificación para una clase específica de términos $\lambda$ de tipos simples conocida como Patrones de Orden Superior Deterministas (DHPs). Mientras que la unificación de orden superior estándar es indecidible e infinitaria (potencialmente produciendo infinitos unificadores incomparables), y la unificación de primer orden es decidible y unitaria, los DHPs ocupan una posición intermedia única. Los DHPs, introducidos por Yokoyama et al., se definen de tal manera que su problema de coincidencia es determinista (existe como máximo una sustitución). Sin embargo, a diferencia de los patrones de orden superior de Miller o la Unificación de Funciones como Constructores (FCU) de Libal y Miller, el problema de unificación para los DHPs no es unitario; los conjuntos completos mínimos de unificadores (MCSUs) pueden ser infinitos. El desafío central es desarrollar un procedimiento de unificación correcto y completo para esta clase que maneje la naturaleza potencialmente infinitaria del espacio de soluciones, manteniendo al mismo tiempo las propiedades estructurales que hacen que la coincidencia sea determinista.

Metodología
Los autores proponen un sistema de inferencia correcto y completo para calcular conjuntos completos de unificadores (CSUs) para DHPs. La metodología se basa en los siguientes fundamentos técnicos:

1. Representación de Términos: El procedimiento opera sobre términos $\lambda$ de tipos simples en forma normal larga $\beta\eta$, utilizando una formulación libre de $\beta\eta$ para simplificar la aplicación de sustituciones y evitar la reducción $\beta$ explícita durante las demostraciones.
2. Definición de DHPs: Un término es un DHP si, para cada subtérmino de la forma $x_n.y(t_m)$ donde $y$ es una variable libre:
   • Cada argumento $t_i$ contiene al menos una variable ligada de $x_n$ (asegurando una coincidencia determinista).
   • Los argumentos están "expandidos" (sus formas normales $\eta$ no son abstracciones).
   • Los argumentos son distintos bajo la relación de "subtérmino expandido" (restricción local), evitando que un argumento sea un subtérmino de orden superior de otro.
3. Sistema de Inferencia: El procedimiento de unificación es un sistema de inferencia no determinista que opera sobre pares de DHPs. Extiende el marco de la unificación completa de orden superior (Huet) pero introduce optimizaciones específicas para DHPs:
   • Resolución Flex-Flex: A diferencia de la unificación completa de orden superior, que requiere vinculaciones parciales para pares flex-flex (pares donde ambas cabezas son variables libres), el sistema DHP resuelve estos de la manera "más general". Las reglas (ff=) y (ff̸=) construyen unificadores manteniendo solo argumentos iguales o combinando argumentos sin introducir variables libres, respectivamente.
   • Proyección e Imitación: El sistema utiliza reglas de imitación y proyección, pero las restringe para asegurar que los términos resultantes permanezcan dentro de la clase DHP. Notablemente, las proyecciones en DHPs deben resultar en cabezas que sean símbolos de función o variables ligadas, no variables libres.
   • Estrategia para Minimalidad: Para asegurar que el conjunto calculado de unificadores sea mínimo (ortogonal), los autores definen estrategias que priorizan las reglas (rem) y (var) y calculan nombres de variables frescas de manera determinista.

Contribuciones y Resultados Clave

• Corrección y Completitud: El artículo demuestra que el sistema de inferencia es correcto (las derivaciones exitosas producen unificadores válidos) y completo (para cualquier unificador $\delta$, existe una derivación que produce un unificador $\theta$ tal que $\theta$ es más general que $\delta$).
• Minimalidad: Los autores demuestran que, bajo estrategias específicas (óptimas localmente y deterministas en variables frescas), el sistema de inferencia produce un Conjunto Completo Mínimo de Unificadores (MCSU). Esto es significativo porque, en la unificación de orden superior general, los conjuntos mínimos no están garantizados de ser ortogonales o finitos.
• Espacios de Soluciones Infinitos: El artículo proporciona ejemplos (por ejemplo, los Ejemplos 10 y 13) que muestran que los MCSUs para DHPs pueden ser infinitos. En consecuencia, el sistema de inferencia no está garantizado de terminar, y la decidibilidad del problema de unificación DHP sigue siendo una pregunta abierta.
• Generalización de FCU: El método generaliza la FCU de Libal y Miller al eliminar la "restricción global" (que impide que un argumento de variable libre sea un subtérmino de cualquier argumento de variable en todo el problema). Al eliminar esto, el sistema maneja un conjunto estrictamente mayor de términos, pero pierde la propiedad unitaria de la FCU.

Significado y Afirmaciones
Los autores sitúan este trabajo como una investigación necesaria en una clase de términos donde la coincidencia permanece determinista, pero la unificación pierde la propiedad unitaria, saltando inmediatamente a problemas infinitarios. El significado radica en:

1. Subrutinas Prácticas: Los DHPs se definen como una clase de términos en lugar de una restricción dependiente del problema (como la restricción global de la FCU). Esto hace que los DHPs sean más fáciles de utilizar como subrutina en demostración automática de teoremas o programación lógica, ya que no es necesario verificar restricciones globales para determinar si un término está en el ámbito.
2. Perspectiva Teórica: El trabajo aclara la frontera entre la coincidencia determinista y la unificación unitaria, mostrando que la transición de la unificación unitaria a la infinitaria puede ocurrir sin pasar por una etapa finitaria.
3. Simulación de FCU: Los autores afirman que su enfoque puede simular la FCU; si un problema FCU tiene un unificador más general, el sistema de inferencia lo encontrará mediante una derivación finita y determinista.

El artículo concluye señalando que, aunque el sistema de inferencia es de ramificación finita, su no terminación impide una demostración de decidibilidad. El trabajo futuro requeriría representaciones ingeniosas de conjuntos infinitos de unificadores (por ejemplo, utilizando gramáticas regulares) para manejar eficazmente los escenarios de ramificación infinita.