Reglas de manejo de restricciones

Lenguaje de programación de lógica de restricciones concurrentes

Constraint Handling Rules ( CHR ) es un lenguaje de programación declarativo basado en reglas , introducido en 1991 por Thom Frühwirth en ese momento en el Centro Europeo de Investigación de la Industria Informática (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 .

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 del almacén, cambiando así el estado del programa. El orden en que las reglas "disparan" en un almacén de restricciones determinado 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 utiliza para ampliar un idioma anfitrión con restricciones. Prolog es, con diferencia, el lenguaje anfitrión más popular y CHR está incluido en varias implementaciones de Prolog, incluidas 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 tienen múltiples encabezados y se ejecutan de 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 lenguaje anfitrión que se ejecutan para manejar algunas reglas. El idioma 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 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 de CHR.

Entonces, un programa CHR 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]

• Las reglas de simplificación tienen la forma . Cuando coinciden con las cabezas y los guardias se mantienen, las reglas de simplificación pueden reescribir las cabezas en el cuerpo . ${\displaystyle h_{1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$ ${\displaystyle h_{1},\dots ,h_{n}}$ ${\displaystyle g_{1},\dots ,g_{m}}$ ${\displaystyle b_{1},\dots ,b_{o}}$
• Las reglas de propagación tienen la forma . Estas reglas añaden las restricciones del cuerpo a la tienda, sin quitar las cabezas. ${\displaystyle h_{1},\dots ,h_{n}\Longrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$
• Las reglas de simulación combinan simplificación y propagación. Están 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 las guardias deben ser verdaderas. Las restricciones anteriores se mantienen, como en una regla de propagación; las restricciones restantes se eliminan. ${\displaystyle h_{1},\dots ,h_{\ell }\,\backslash \,h_{\ell +1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}}$ ${\displaystyle \ell }$ ${\displaystyle \backslash }$ ${\displaystyle n-\ell }$

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

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

donde cada uno de es una conjunción de restricciones: y contiene restricciones CHR, mientras que las guardias están integradas. Sólo uno de debe estar vacío. ${\displaystyle H_{k},H_{r},G,B}$ ${\displaystyle H_{k},H_{r}}$ ${\displaystyle B}$ ${\displaystyle G}$ ${\displaystyle H_{k},H_{r}}$

El idioma anfitrión también debe definir restricciones integradas sobre los términos. Las protecciones de las reglas son restricciones integradas, por lo que ejecutan eficazmente el código del lenguaje anfitrión. La teoría de restricciones incorporada debe incluir al menos true(la restricción que siempre se cumple), fail(la restricción que nunca se cumple y se utiliza para señalar el fracaso) y la igualdad de términos, es decir, la unificación . ^[7] Cuando el idioma 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 continúa comparando reglas con la tienda y aplicándolas, hasta que no coincidan más reglas (éxito) o hasta que failse derive la restricción. En el primer caso, un programa de lenguaje anfitrión puede leer el almacén de restricciones para buscar datos de interés. La coincidencia 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. ^[9]

Programa de ejemplo

El siguiente programa CHR, en sintaxis Prolog, contiene cuatro reglas que implementan un solucionador para una restricción 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 a  la reflexividad de la variable Y  @  X  leq  X  <=>  true .  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 maneras. 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 se encuentra en la tienda un hecho de la forma X ≤ X , éste puede ser eliminado.
• La antisimetría también es una regla de simplificación, pero con dos cabezas . Si se pueden encontrar dos hechos de la forma X ≤ Y e Y ≤ X en la tienda (con X e Y coincidentes ), entonces se pueden reemplazar con un único hecho X = Y. Esta restricción de igualdad se considera incorporada y se implementa como una unificación que normalmente 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 hay en la tienda hechos de la forma X ≤ Y e Y ≤ Z (con el mismo valor para Y ), se puede agregar un tercer hecho X ≤ Z.
• La idempotencia, finalmente, es una regla de simpatía , una simplificación y propagación combinadas. Cuando encuentra datos duplicados, los elimina del almacén. Pueden ocurrir duplicados porque los almacenes de restricciones son conjuntos múltiples de hechos.

dada la consulta

A leq B, B leq C, C leq A

pueden ocurrir las siguientes transformaciones:

La regla de transitividad añade A leq C. Luego, aplicando la regla de antisimetría , A leq Cy C leq Ase eliminan y se reemplazan por A = C. Ahora la regla de antisimetría pasa a ser 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 = Cse devuelve la respuesta: CHR ha inferido correctamente que las tres variables deben referirse al mismo objeto.

Ejecución de programas de la CDH

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 diferido 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 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 confluente localmente si todos sus pares críticos son conectables .
• Un programa CHR se llama terminación si no hay cálculos infinitos.
• Un programa CHR que termina es confluente si todos sus pares críticos son conectables .

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 de negocio
• Reescritura

Referencias

1. Thom Frühwirth. Introducción a las 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.
2. Thom Frühwirth. Teoría y práctica de reglas de manejo de restricciones . Número especial sobre programación lógica con 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
3. Dahl, Verónica y J. Emilio Miralles. "Gramáticas de ú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.
4. Alves, Sandra y Mário Florido. "Inferencia de tipos utilizando reglas de manejo de restricciones". Apuntes electrónicos en informática teórica 64 (2002): 56-72.
5. 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 la 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. S2CID  11044594.
6. Frühwirth, Thom (2009). Reglas de manejo de restricciones . Prensa de la Universidad de Cambridge. ISBN 978-0521877763.
7. 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 . 31 (2): 1–42. doi :10.1145/1462166.1462169. S2CID  2691882.
8. "CHR: biblioteca de reglas de manejo de restricciones". GitHub . 5 de septiembre de 2021.
9. Peter Van Weert; Pieter Wuille; Tom Schrijvers; Bart Demoen. "CHR para idiomas anfitriones imperativos". Reglas de manejo de restricciones: temas de investigación actuales . Saltador.
10. "Convertidor de CHR2 a SQL". GitHub . 15 de marzo de 2021.
11. CHR.js: un transpilador de CHR para JavaScript
12. Miranker, Daniel P. (13 al 17 de julio de 1987). "TREAT: Un algoritmo de mejor combinación para sistemas de producción de IA" (PDF) . AAAI'87: Actas de la sexta conferencia nacional sobre inteligencia artificial . Seattle, Washington: Asociación para el Avance de la Inteligencia Artificial, AAAI. págs. 42–47. ISBN 978-0-262-51055-4.
13. Leslie De Koninck (2008). Control de ejecución de reglas de manejo de restricciones (PDF) (tesis doctoral). Universidad Católica de Lovaina . págs. 12-14.
14. Pato, Gregory J.; Stuckey, Peter J.; García de la Banda, María ; Holzbaur, cristiano (2004). "La semántica operativa refinada de las reglas de manejo de restricciones" (PDF) . Programación Lógica . Apuntes de conferencias sobre informática. vol. 3132, págs. 90-104. doi :10.1007/978-3-540-27775-0_7. ISBN 978-3-540-22671-0. 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 de la CDH
• La lista de correo de la CDH
• El sistema KULeuven CHR
• WebCHR: una interfaz web de la CHR