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 European Computer-Industry Research Centre (ECRC) en Munich, Alemania. [1] [2] Originalmente pensado para la programación con restricciones , CHR encuentra aplicaciones en la 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 .
Un programa CHR, a veces llamado manejador 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 del almacén, cambiando así el estado del programa. El orden en el que las reglas se "activan" 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 usa para extender un lenguaje anfitrión con restricciones. Prolog es por lejos el lenguaje anfitrión más popular y CHR está incluido en varias implementaciones de Prolog, incluyendo SICStus y SWI-Prolog , aunque también existen implementaciones de CHR para Haskell , [8] Java , C , [9] SQL , [10] y JavaScript. [11] A diferencia de Prolog, las reglas de CHR son multi-encabezadas y se ejecutan de manera de elección comprometida usando un algoritmo de encadenamiento hacia adelante .
La sintaxis concreta de los programas CHR depende del lenguaje anfitrión y, de hecho, los programas incorporan sentencias en el lenguaje anfitrión que se ejecutan para manejar algunas reglas. El lenguaje anfitrión 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, se utiliza Prolog como lenguaje anfitrión, por lo que se utilizan sus estructuras de datos y variables. El resto de esta sección utiliza una notación matemática neutral que es común en la literatura CHR.
Un programa CHR, entonces, consta de reglas que manipulan un conjunto múltiple de estos términos, llamado almacén de restricciones . Las reglas son de tres tipos: [5]
Dado que las reglas de simplificació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 contiene restricciones CHR, mientras que las protecciones están integradas. Solo uno de debe no estar vacío.
El lenguaje anfitrión también debe definir restricciones incorporadas sobre los términos. Las protecciones en las reglas son restricciones incorporadas, por lo que ejecutan efectivamente el código del lenguaje anfitrión. La teoría de restricciones incorporadas 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 un fallo) e igualdad de términos, es decir, unificación . [7] Cuando el lenguaje anfitrión no admite estas características, deben implementarse junto con CHR. [9]
La ejecución de un programa CHR comienza con un almacén de restricciones inicial. Luego, el programa procede a comparar reglas con el almacén y aplicarlas hasta que no haya más reglas que coincidan (éxito) o failse derive la restricción. En el primer caso, un programa en lenguaje anfitrión puede leer el almacén de restricciones para buscar hechos de interés. La comparación se define como una "unificación unidireccional": vincula variables solo en un lado de la ecuación. La comparación de patrones se puede implementar fácilmente como unificación cuando el lenguaje anfitrión la admite. [9]
El siguiente programa CHR, en sintaxis Prolog, contiene cuatro reglas que implementan un solucionador para una restricción de menor o igual . Las reglas están etiquetadas para mayor comodidad (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 pueden leerse de dos maneras. En la lectura declarativa, tres de las reglas especifican los axiomas de un ordenamiento parcial :
Las tres reglas están cuantificadas de manera universal e implícita (los identificadores en mayúsculas son variables en la sintaxis de Prolog). La regla de 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 informático para mantener un almacén de restricciones, una colección de hechos (restricciones) sobre los objetos. El almacén de restricciones no forma parte de este programa, sino que debe proporcionarse por separado. Las reglas expresan las siguientes reglas de cálculo:
Dada la consulta
A leq B, B leq C, C leq A
Pueden ocurrir las siguientes transformaciones:
La regla de transitividad agrega A leq C. Luego, al aplicar la regla de antisimetría , A leq Cy C leq Ase eliminan y se reemplazan por A = C. Ahora la regla de antisimetría se vuelve aplicable en las primeras dos 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 = Cse devuelve la respuesta: CHR ha inferido correctamente que las tres variables deben hacer referencia al mismo objeto.
Para decidir qué regla debe "activarse" en un almacén de restricciones determinado, una implementación de CHR debe utilizar algún algoritmo de coincidencia de patrones . Los algoritmos candidatos incluyen RETE y TREAT, [12] pero la mayoría de las implementaciones utilizan un algoritmo perezoso llamado LEAPS . [13]
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] [14]
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 asignación satisfactoria serán no deterministas e impredecibles. El establecimiento de la confluencia se realiza generalmente mediante las tres propiedades siguientes: [2]