Unificación de orden superior

Question

Estoy trabajando en un comprobador de teoremas de orden superior, cuya unificación parece ser el subproblema más difícil.

Si el algoritmo de Huet todavía se considera de última generación, ¿alguien tiene algún vínculo con explicaciones escritas para que las entienda un programador en lugar de un matemático?

¿O incluso algún ejemplo de dónde funciona y el algoritmo de primer orden habitual no?

Answer 1

Estado del arte — sí, por lo que yo sé todos los algoritmos más o menos tomar la misma forma que (sigo la teoría de la programación lógica, aunque mi experiencia es tangencial) proporcionado necesita lleno de orden superior de Huet emparejamiento: los subproblemas como la coincidencia de orden superior (unificación donde se cierra un término) y el cálculo del patrón de Dale Miller son decidibles.

Tenga en cuenta que el algoritmo de Huet es el mejor en el siguiente sentido — es como un algoritmo de semideducción, en el sentido de que encontrará los unificadores si existen, pero no se garantiza que terminen si no lo hacen. Como sabemos que la unificación de orden superior (de hecho, la unificación de segundo orden) es indecidible, no puedes hacer nada mejor que eso.

Explicaciones: Los primeros cuatro capítulos de la tesis doctoral de Conal Elliott, Extensions and Applications of Higher-Order Unification deben encajar en la factura. Esa parte pesa casi 80 páginas, con alguna teoría de tipos densa, pero está bien motivada, y es la cuenta más fácil de leer que he visto.

Ejemplos: El algoritmo de Huet creará los productos para este ejemplo: [X (o), Y (succ (0))]; que necesariamente confundirá un algoritmo de unificación de primer orden.

Answer 2

Un ejemplo de unificación de orden superior (realmente de segundo orden) es: f 3 == 3 + 3, donde == es módulo alfa, beta y conversión de eta (pero no asigna ningún significado a "+"). Hay cuatro soluciones:

\ x -> x + x 
\ x -> x + 3 
\ x -> 3 + x 
\ x -> 3 + 3 

Por el contrario, la unificación/coincidencia de primer orden no daría ninguna solución.

HOU es muy útil cuando se utiliza con HOAS (de orden superior sintaxis abstracta), para codificar idiomas con enlace variable evitando al mismo tiempo la complejidad de captura de variables, etc.

Mi primer contacto con el tema fue el papel de "Probar y aplicar transformaciones de programa expresadas con patrones de segundo orden "por Gerard Huet y Bernard Lang. Según recuerdo, este documento fue "escrito para ser entendido por un programador". Y una vez que comprenda la coincidencia de segundo orden, HOU no está mucho más lejos. Un resultado clave de Huet es que el caso flexible/flexible (variables como encabezado de un término y el único caso que no aparece en el emparejamiento) siempre se puede resolver.

Answer 3

Añadiría a la lista de lectura un capítulo en el volumen 2 de el Manual de razonamiento automatizado. Este capítulo probablemente sea más accesible para el principiante y finaliza con λΠ-calculus donde comienza el papel Conal Elliott .

Un pre-impresión se encuentra aquí:

de orden superior Unificación y Correspondencia de
Gilles Dowek, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps

papel

Conal Elliott es más formal y concerntrated en una variante, y también introduce un cálculo λΠΣ al final, que también tiene tipos suma además de tipos de productos.

adiós

Answer 4

También hay de Tobias Nipkow 1993 papel Functional Unification of Higher-Order Patterns (sólo 11 páginas, 4 de los cuales son bibliografía y el apéndice de código). El resumen:

el desarrollo completo de un algoritmo de unificación para los llamados patrones de orden superior, una subclase de $ \ lambda $ -Condiciones, se presenta. El punto de partida es una formulación de unificación por transformación, el resultado es un programa funcional directamente ejecutable. En un paso de desarrollo final, el resultado se adapta a $ \ lambda $ -terms en la notación de Bruijn. Los algoritmos funcionan tanto para términos simplemente tipeados como sin tipo.