Reglas de manejo de restricciones

Constraint Handling Rules ( CHR ) es un lenguaje de programación declarativo basado en reglas , introducido en 1991 por Thom Frühwirth en ese entonces con el Centro Europeo de Investigación de la Industria Informática (ECRC) en Múnich, 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 , planificació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 las reglas puede agregar o eliminar fórmulas del almacén, cambiando así el estado del programa. El orden en que las reglas se "activan" en un almacén de restricciones dado es no determinista , ^{[ 5 ]} según su semántica abstracta y determinista (aplicación de reglas de arriba hacia abajo), según 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, con mucho, 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 de múltiples cabezas 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 instrucciones en dicho lenguaje que se ejecutan para gestionar ciertas reglas. El lenguaje anfitrión proporciona una estructura de datos para representar términos , incluidas 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 anfitrión, por lo que se emplean sus estructuras de datos y variables. El resto de esta sección utiliza una notación matemática neutral, común en la literatura sobre CHR.

Un programa CHR, entonces, consiste en reglas que manipulan un multiconjunto de estos términos, llamado almacén de restricciones . Las reglas vienen en tres tipos: ^{[ 5 ]}

• Las reglas de simplificación tienen la forma${\displaystyle h_{1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$Cuando coinciden las cabezas${\displaystyle h_{1},\dots ,h_{n}}$y los guardias${\displaystyle g_{1},\dots ,g_{m}}$sostén, las reglas de simplificación pueden reescribir las cabezas en el cuerpo${\displaystyle b_{1},\dots ,b_{o}}$.
• Las reglas de propagación tienen la forma${\displaystyle h_{1},\dots ,h_{n}\Longrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$Estas reglas agregan las restricciones del cuerpo al almacén, sin eliminar las cabeceras.
• Las reglas de simpagación combinan simplificación y propagación. Están escritas${\displaystyle h_{1},\dots ,h_{\ell }\,\backslash \,h_{\ell +1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$Para que se active una regla de simpagación, el almacén de restricciones debe coincidir con todas las reglas en la cabecera y las condiciones deben ser verdaderas.${\displaystyle \ell }$restricciones antes de la${\displaystyle \backslash }$se conservan, como en una regla de propagación; los restantes${\displaystyle n-\ell }$Se eliminan las restricciones.

Dado que las reglas de simpagación engloban la simplificación y la propagación, todas las reglas CHR siguen el formato

${\displaystyle H_{k}\,\backslash \,H_{r}\Longleftrightarrow G\,|\,B}$

donde cada uno de${\displaystyle H_{k},H_{r},G,B}$es una conjunción de restricciones:${\displaystyle H_{k},H_{r}}$y${\displaystyle B}$contienen restricciones CHR, mientras que los guardas${\displaystyle G}$están integrados. Solo uno de${\displaystyle H_{k},H_{r}}$debe no estar vacío.

El lenguaje anfitrión también debe definir restricciones integradas sobre los términos. Las condiciones en las reglas son restricciones integradas, por lo que ejecutan efectivamente el código del lenguaje anfitrión. La teoría de restricciones integradas debe incluir al menos true(la restricción que siempre se cumple), fail(la restricción que nunca se cumple y se usa para indicar 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. A continuación, el programa procede comparando reglas con dicho almacén y aplicándolas hasta que no haya más coincidencias (éxito) o failse derive la restricción. En el primer caso, el almacén de restricciones puede ser leído por un programa en lenguaje anfitrión 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 lo admite. ^{[ 9 ]}

% 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 . 

A leq B, B leq C, C leq A

Para decidir qué regla debe "activarse" en un almacén de restricciones dado, una implementación de CHR debe usar algún algoritmo de coincidencia de patrones . Los algoritmos candidatos incluyen RETE y TREAT , ^{[ 12 ]} pero la mayoría de las implementaciones usan un algoritmo perezoso llamado LEAPS . ^{[ 13 ]}

La especificación original de la semántica de CHR era completamente no determinista, pero la denominada "semántica de operación refinada" de Duck et al. eliminó gran parte del no determinismo, de modo que los desarrolladores de aplicaciones pueden 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 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 generalmente se realiza a través de las siguientes tres propiedades: ^{[ 2 ]}

• Un programa CHR es localmente confluente si todos sus pares críticos son unibles .
• Un programa CHR se considera terminante si no hay cálculos infinitos.
• Un programa CHR que está terminando es confluente si todos sus pares críticos son unibles .

• Programación con restricciones
• Programación lógica con restricciones
• Programación lógica
• Sistema de producción (informática)
• Motores de reglas de negocio
• Reescritura

• Christiansen, Henning. " Gramáticas CHR ". Teoría y práctica de la programación lógica 5.4-5 (2005): 467-501.

• Sitio web oficial
• Bibliografía de CHR
• La lista de correo de CHR
• El sistema CHR de la KU Leuven
• WebCHR: una interfaz web de CHR