Unificación de orden superior
Estoy trabajando en un probador de teoremas de orden superior, de los cuales la 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 enlace a explicaciones del mismo que estén escritas para ser entendidas por 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 lo hace?
4 answers
Estado del arte - sí, hasta donde sé que todos los algoritmos más o menos toman la misma forma que la de Huet (sigo la teoría de la programación lógica, aunque mi experiencia es tangencial) siempre que necesita coincidencia completa de orden superior: subproblemas como la coincidencia de orden superior (unificación donde un término está cerrado), y el cálculo de patrones 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 semi-decisión, en que encontrará los unificadores si existen, pero no se garantiza que terminarán si no lo hacen. Ya que sabemos que la unificación de orden superior (de hecho, la unificación de segundo orden) es indecidible, no se puede hacer mejor que eso.
Explicaciones: Los primeros cuatro capítulos de la tesis doctoral de Conal Elliott, Extensiones y Aplicaciones de Unificación de Orden Superior deberían ajustarse a la ley. Esa parte pesa casi 80 páginas, con alguna teoría de tipos densos, pero está bien motivada, y es la más cuenta legible que he visto.
Ejemplos: El algoritmo de Huet obtendrá los bienes para este ejemplo: [X(o), Y(succ(0))]; lo que por necesidad desconcertará a un algoritmo de unificación de primer orden.
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2009-12-24 13:05:19
Un ejemplo de unificación de orden superior (realmente coincidencia de segundo orden) es: f 3 == 3 + 3, donde == es módulo alfa, beta y eta-conversión (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 usa con HOAS (sintaxis abstracta de orden superior), para codificar lenguajes con enlace de variables mientras se evita la complejidad de la captura de variables, etc.
Mi primera la exposición al tema fue el artículo "Probando y Aplicando Transformaciones de Programas Expresadas con Patrones de Segundo Orden" de Gerard Huet y Bernard Lang. Según recuerdo, este documento fue "escrito para ser entendido por un programador". Y una vez que entiendas 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 cabeza de un término, y el único caso que no aparece en la coincidencia) siempre es solucionable.
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2010-03-23 23:27:48
Añadiría a la lista de lectura un capítulo en el volumen 2 de the Handbook of Automated Reasoning (en inglés). Este capítulo es probablemente más accesible para el principiante y termina con λΠ-cálculo donde Comienza el papel de Conal Elliott.
Un preprint se encuentra aquí:
Unificación y Coincidencia de Orden Superior
Gilles Dowek, 2001
http://www.lsv.fr/~dowek / Publi / unification.ps
El documento 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
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2017-06-13 01:24:02
También está el documento de Tobias Nipkow de 1993 Functional Unification of Higher-Order Patterns (solo 11 páginas, 4 de las cuales son bibliografía y apéndice de código). El resumen:
Se presenta el desarrollo completo de un algoritmo de unificación para los llamados patrones de orden superior, una subclase de términos lamb\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 desarrollo final paso el resultado se adapta a los términos lamb \ lambda$en la notación de de Bruijn. Los algoritmos funcionan tanto para términos simplemente mecanografiados como sin mecanografiar.
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2016-06-07 20:00:04