algorithm - keywords - meta tags seo 2018

Unificación de orden superior

Question

Estoy trabajando en un probador 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 vanguardia, ¿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

Agregaría a la lista de lectura un capítulo en el volumen 2 del Manual de razonamiento automatizado. Este capítulo es probablemente más accesible para el principiante y termina con el cálculo λΠ-donde se inicia el papel de Conal Elliott.

Una preimpresión se encuentra aquí:

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

El papel de Conal Elliott es más formal y se refiere a una variante, y también introduce un cálculo λΠΣ al final, que también tiene tipos de suma además de los tipos de producto.

Adiós

Answer 2

Estado del arte: sí, por lo que sé, todos los algoritmos toman más o menos la misma forma que los de Huet (sigo la teoría de la programación lógica, aunque mi experiencia es tangencial) siempre que necesite una coincidencia total de orden superior: subproblemas como mayor -correspondencia de orden (unificación donde se cierra un término) y cálculo de 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 terminará 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 de doctorado de Conal Elliott, Extensiones y aplicaciones de la unificación de orden superior deberían encajar. 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 presentará los productos para este ejemplo: [X (o), Y (succ (0))]; que necesariamente confundirá un algoritmo de unificación de primer orden.

Answer 3

También está el documento de 1993 de Tobias Nipkow Unificación funcional de patrones de orden superior (solo 11 páginas, 4 de las cuales son bibliografía y apéndice de código). El abstracto:

Se presenta el desarrollo completo de un algoritmo de unificación para los llamados patrones de orden superior , una subclase de $ / lambda $ -terms. 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.

Answer 4

Un ejemplo de unificación de orden superior (realmente concordancia 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 (sintaxis abstracta de orden superior), para codificar idiomas con encuadernación variable, evitando la complejidad de la captura variable, etc.

Mi primera exposición al tema fue el documento "Probar y aplicar las transformaciones del 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.