Constraint Handling Rules ( CHR ) es un lenguaje de programación declarativo basado en reglas , introducido en 1991 por Thom Frühwirth en ese momento con el Centro Europeo de Investigación de la Industria de la Computación (ECRC) en Munich, Alemania. [1] [2] Originalmente destinado a la programación de restricciones , CHR encuentra aplicaciones en inducción gramatical , [3] sistemas de tipos , [4] razonamiento abductivo , sistemas multiagente , procesamiento del lenguaje natural , compilación , programación , razonamiento espacio-temporal , pruebas y verificación .
Paradigmas | Lógica de restricción , declarativa |
---|---|
Diseñada por | Thom Frühwirth |
Apareció por primera vez | 1991 |
Influenciado por | |
Prólogo |
Un programa CHR, a veces llamado controlador de restricciones , es un conjunto de reglas que mantienen un almacén de restricciones , un conjunto múltiple de fórmulas lógicas. La ejecución de reglas puede agregar o eliminar fórmulas de la tienda, cambiando así el estado del programa. El orden en el que las reglas "disparan" en un almacén de restricciones dado es no determinista , [5] de acuerdo con su semántica abstracta y determinista (aplicación de reglas de arriba hacia abajo), de acuerdo con su semántica refinada . [6]
Aunque CHR es Turing completo , [7] no se usa comúnmente como lenguaje de programación por derecho propio. Más bien, se utiliza para ampliar un idioma anfitrión con restricciones. Prolog es, con mucho, el lenguaje host más popular y CHR se incluye en varias implementaciones de Prolog, incluidas SICStus y SWI-Prolog , aunque también existen implementaciones de CHR para Haskell , Java , C , [8] SQL , [9] y JavaScript. [10] A diferencia de Prolog, las reglas de CHR son de múltiples encabezados y se ejecutan de una manera de elección comprometida utilizando un algoritmo de encadenamiento directo .
Descripción general del idioma
La sintaxis concreta de los programas CHR depende del idioma anfitrión y, de hecho, los programas incorporan declaraciones en el idioma anfitrión que se ejecutan para manejar algunas reglas. El lenguaje principal proporciona una estructura de datos para representar términos , incluidas las variables lógicas . Los términos representan restricciones, que pueden considerarse como "hechos" sobre el dominio del problema del programa. Tradicionalmente, Prolog se utiliza como lenguaje principal, por lo que se utilizan sus estructuras de datos y variables. El resto de esta sección utiliza una notación matemática neutra que es común en la literatura de la CDH.
Un programa CHR, entonces, consta de reglas que manipulan un conjunto múltiple de estos términos, llamado almacenamiento de restricciones . Hay tres tipos de reglas: [5]
- Las reglas de simplificación tienen la forma . Cuando coinciden con las cabezas y los guardias mantener, las reglas de simplificación pueden reescribir las cabezas en el cuerpo .
- Las reglas de propagación tienen la forma . Estas reglas agregan las restricciones en el cuerpo a la tienda, sin quitar las cabezas.
- Las reglas de simplificación combinan la simplificación y la propagación. Estan escritos. Para que se active una regla de simulación, el almacén de restricciones debe coincidir con todas las reglas en la cabeza y los guardias deben mantenerse verdaderos. La restricciones antes de la se mantienen, como en una regla de propagación; el restante se eliminan las restricciones.
Dado que las reglas de simpagación incluyen la simplificación y la propagación, todas las reglas de CHR siguen el formato
donde cada uno de es una conjunción de restricciones: y contienen restricciones de CHR, mientras que los guardias están incorporados. Solo uno de no debe estar vacío.
El idioma anfitrión también debe definir restricciones integradas sobre los términos. Las protecciones en las reglas son restricciones integradas, por lo que ejecutan de manera efectiva el código del idioma del host. La teoría de la restricción incorporada debe incluir al menos true
(la restricción que siempre se cumple), fail
(la restricción que nunca se cumple y se usa para señalar fallas) e igualdad de términos, es decir, unificación . [7] Cuando el idioma anfitrión no admite estas funciones, deben implementarse junto con CHR. [8]
La ejecución de un programa CHR comienza con un almacenamiento de restricciones inicial. Luego, el programa procede comparando reglas con la tienda y aplicándolas, hasta que no coincidan más reglas (éxito) o fail
se derive la restricción. En el primer caso, un programa de lenguaje anfitrión puede leer el almacén de restricciones para buscar hechos de interés. El emparejamiento se define como "unificación unidireccional": vincula variables solo en un lado de la ecuación. La coincidencia de patrones se puede implementar fácilmente como unificación cuando el idioma anfitrión lo admite. [8]
Programa de ejemplo
El siguiente programa CHR, en la sintaxis de Prolog, contiene cuatro reglas que implementan un solucionador para una restricción menor o igual . Las reglas están etiquetadas por conveniencia (las etiquetas son opcionales en CHR).
% X leq Y significa que la variable X es menor o igual que la variable Y reflexividad @ X leq X <=> verdadero . antisimetría @ X leq Y , Y leq X <=> X = Y . transitividad @ X leq Y , Y leq Z ==> X leq Z . idempotencia @ X leq Y \ X leq Y <=> verdadero .
Las reglas se pueden leer de dos formas. En la lectura declarativa, tres de las reglas especifican los axiomas de un ordenamiento parcial :
- Reflexividad: X ≤ X
- Antisimetría: si X ≤ Y e Y ≤ X , entonces X = Y
- Transitividad: si X ≤ Y e Y ≤ Z , entonces X ≤ Z
Las tres reglas están implícitamente cuantificadas universalmente (los identificadores en mayúsculas son variables en la sintaxis de Prolog). La regla de la idempotencia es una tautología desde el punto de vista lógico, pero tiene un propósito en la segunda lectura del programa.
La segunda forma de leer lo anterior es como un programa de computadora para mantener un almacén de restricciones, una colección de hechos (restricciones) sobre objetos. El almacén de restricciones no forma parte de este programa, pero debe suministrarse por separado. Las reglas expresan las siguientes reglas de cálculo:
- La reflexividad es una regla de simplificación : expresa que, si un hecho de la forma X ≤ X se encuentra en la tienda, puede ser eliminado.
- La antisimetría también es una regla de simplificación, pero con dos cabezas . Si dos hechos de la forma X ≤ Y y Y ≤ X se pueden encontrar en la tienda (a juego con X y Y ), entonces pueden ser sustituidas con el solo hecho de X = Y . Dicha restricción de igualdad se considera incorporada y se implementa como una unificación que generalmente es manejada por el sistema Prolog subyacente.
- La transitividad es una regla de propagación . A diferencia de la simplificación, no elimina nada del almacén de restricciones; en cambio, cuando los hechos de la forma X ≤ Y e Y ≤ Z (con el mismo valor para Y ) están en el almacén, se puede agregar un tercer hecho X ≤ Z.
- La idempotencia, finalmente, es una regla de simpagación , una combinación de simplificación y propagación. Cuando encuentra hechos duplicados, los elimina de la tienda. Pueden producirse duplicados porque los almacenes de restricciones son conjuntos de hechos múltiples.
Dada la consulta
A leq B, B leq C, C leq A
pueden ocurrir las siguientes transformaciones:
Limitaciones actuales | Regla aplicable a las restricciones | Conclusión de la aplicación de reglas |
---|---|---|
A leq B, B leq C, C leq A | transitividad | A leq C |
A leq B, B leq C, C leq A, A leq C | antisimetría | A = C |
A leq B, B leq A, A = C | antisimetría | A = B |
A = B, A = C | ninguno |
La transitividad regla añade A leq C
. Luego, mediante la aplicación de la antisimetría regla, A leq C
y C leq A
se retira y se sustituye por A = C
. Ahora, la regla antisimetría se vuelve aplicable a las dos primeras restricciones de la consulta original. Ahora se eliminan todas las restricciones de CHR, por lo que no se pueden aplicar más reglas y A = B, A = C
se devuelve la respuesta : CHR ha inferido correctamente que las tres variables deben hacer referencia al mismo objeto.
Ejecución de programas CHR
Para decidir qué regla debe "activarse" en un almacén de restricciones dado, una implementación de CHR debe utilizar algún algoritmo de coincidencia de patrones . Algoritmos candidatos incluyen RETE y TREATS , pero la mayoría del uso de una aplicación perezoso algoritmo llamado LEAPS . [11]
La especificación original de la semántica de CHR era completamente no determinista, pero la llamada "semántica de operación refinada" de Duck et al. eliminó gran parte del no determinismo para que los escritores de aplicaciones puedan confiar en el orden de ejecución para el rendimiento y la corrección de sus programas. [5] [12]
La mayoría de las aplicaciones de los CHR requieren que el proceso de reescritura sea confluente ; de lo contrario, los resultados de la búsqueda de una tarea satisfactoria serán no deterministas e impredecibles. El establecimiento de la confluencia generalmente se realiza mediante las siguientes tres propiedades: [2]
- Un programa CHR es localmente confluente si todos sus pares críticos se pueden unir .
- Un programa CHR se llama terminando si no hay cálculos infinitos.
- Un programa CHR de terminación es confluente si todos sus pares críticos se pueden unir .
Ver también
- Programación de restricciones
- Programación lógica de restricciones
- Programación lógica
- Sistema de producción (informática)
- Motores de reglas comerciales
- Reescritura
Referencias
- ^ Thom Frühwirth. Presentación de reglas de simplificación . Informe interno ECRC-LP-63, ECRC Munich, Alemania, octubre de 1991, presentado en el Workshop Logisches Programmieren, Goosen / Berlín, Alemania, octubre de 1991 y en el Workshop on Rewriting and Constraints, Dagstuhl, Alemania, octubre de 1991.
- ^ a b Thom Frühwirth. Teoría y práctica de las reglas de manejo de restricciones . Número especial sobre programación lógica de restricciones (P. Stuckey y K. Marriott, Eds.), Journal of Logic Programming, Vol 37 (1-3), octubre de 1998. doi : 10.1016 / S0743-1066 (98) 10005-5
- ^ Dahl, Veronica y J. Emilio Miralles. " Gramáticas del útero: resolución de restricciones para la inducción gramatical ". Actas del Noveno Taller sobre Reglas de Manejo de Restricciones. vol. Informe técnico CW. Vol. 624, 2012.
- ^ Alves, Sandra y Mário Florido. " Inferencia de tipos usando reglas de manejo de restricciones ". Notas electrónicas en informática teórica 64 (2002): 56-72.
- ^ a b c Sneyers, Jon; Van Weert, Peter; Schrijvers, Tom; De Koninck, Leslie (2009). "A medida que pasa el tiempo: Reglas de manejo de restricciones - Una encuesta de la investigación de CHR entre 1998 y 2007" (PDF) . Teoría y práctica de la programación lógica . 10 : 1. arXiv : 0906,4474 . doi : 10.1017 / S1471068409990123 .
- ^ Frühwirth, Thom (2009). Reglas de manejo de restricciones . Prensa de la Universidad de Cambridge. ISBN 0521877768.
- ^ a b Sneyers, Jon; Schrijvers, Tom; Demoen, Bart (2009). "El poder computacional y la complejidad de las reglas de manejo de restricciones" (PDF) . Transacciones ACM sobre lenguajes y sistemas de programación (TOPLAS) . 31 (2).
- ^ a b c Peter Van Weert; Pieter Wuille; Tom Schrijvers; Bart Demoen. "CHR para lenguajes anfitriones imperativos" . Reglas de manejo de restricciones: temas de investigación actuales . Saltador.
- ^ https://github.com/awto/chr2sql
- ^ CHR.js: un transpilador CHR para JavaScript
- ^ Leslie De Koninck (2008). Control de ejecución para reglas de manejo de restricciones (PDF) (tesis doctoral). Katholieke Universiteit Leuven . págs. 12-14.
- ^ Duck, Gregory J .; Stuckey, Peter J .; García de la Banda, María; Holzbaur, Christian (2004). "La semántica operativa refinada de las reglas de manejo de restricciones" (PDF) . Programación lógica : 90-104. Archivado desde el original (PDF) el 4 de marzo de 2011 . Consultado el 23 de diciembre de 2014 .
Otras lecturas
- Christiansen, Henning. " Gramáticas CHR ". Teoría y práctica de la programación lógica 5.4-5 (2005): 467-501.
enlaces externos
- Página web oficial
- Bibliografía CHR
- La lista de correo de CHR
- El sistema KULeuven CHR
- WebCHR: una interfaz web de CHR