Правила обработки ограничений

Правила обработки ограничений (CHR)
Парадигмы	Логика ограничений , декларативная
Разработано	Том Фрювирт
Впервые появился	1991 ; 33 года назад ( 1991 )
Веб-сайт	правила-обработки-ограничений.org
Под влиянием
	Пролог

Язык программирования логики параллельных ограничений

Правила обработки ограничений ( CHR ) — декларативный язык программирования на основе правил , представленный в 1991 году Томом Фрювиртом в то время в Европейском исследовательском центре компьютерной промышленности (ECRC) в Мюнхене, Германия. ^[1]^[2] Первоначально предназначенный для программирования ограничений , CHR находит применение в индукции грамматики , ^[3] системах типов , ^[4] абдуктивных рассуждениях , многоагентных системах , обработке естественного языка , компиляции , планировании , пространственно-временных рассуждениях , тестировании и верификации .

Программа CHR, иногда называемая обработчиком ограничений , представляет собой набор правил, которые поддерживают хранилище ограничений , мультимножество логических формул. Выполнение правил может добавлять или удалять формулы из хранилища, тем самым изменяя состояние программы. Порядок, в котором правила «срабатывают» в данном хранилище ограничений, является недетерминированным , ^[5] согласно его абстрактной семантике и детерминированным (применение правил сверху вниз), согласно его уточненной семантике . ^[6]

Хотя CHR является полным по Тьюрингу , ^[7] он обычно не используется как язык программирования сам по себе. Скорее, он используется для расширения основного языка с ограничениями. Prolog на сегодняшний день является самым популярным основным языком, и CHR включен в несколько реализаций Prolog, включая SICStus и SWI-Prolog , хотя реализации CHR также существуют для Haskell , ^[8] Java , C , ^[9] SQL , ^[10] и JavaScript. ^[11] В отличие от Prolog, правила CHR являются многоголовыми и выполняются в манере обязательного выбора с использованием алгоритма прямой цепочки .

Обзор языка

Конкретный синтаксис программ CHR зависит от языка хоста, и на самом деле программы встраивают операторы в язык хоста, которые выполняются для обработки некоторых правил. Язык хоста предоставляет структуру данных для представления терминов , включая логические переменные. Термины представляют ограничения, которые можно рассматривать как «факты» о проблемной области программы. Традиционно в качестве языка хоста используется Prolog, поэтому используются его структуры данных и переменные. Остальная часть этого раздела использует нейтральную математическую нотацию, которая распространена в литературе по CHR.

Программа CHR, таким образом, состоит из правил, которые манипулируют множественным набором этих терминов, называемым хранилищем ограничений . Правила бывают трех типов: ^[5]

Правила упрощения имеют вид . Когда они соответствуют головам и держателям , правила упрощения могут переписать головы в тело . $h_{1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$ $h_{1},\точки ,h_{n}$ $g_{1},\dots ,g_{m}$ $b_{1},\точки ,b_{o}$
Правила распространения имеют вид . Эти правила добавляют ограничения в теле к хранилищу, не удаляя головы. $h_{1},\dots ,h_{n}\Longrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$
Правила симпагации объединяют упрощение и распространение. Они записываются . Для срабатывания правила симпагации хранилище ограничений должно соответствовать всем правилам в заголовке, а защитные условия должны быть истинными. Ограничения перед сохраняются, как в правиле распространения; оставшиеся ограничения удаляются. $h_{1},\dots ,h_{\ell }\,\backslash \,h_{\ell +1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$ $\ell$ $\backslash$ $n-\ell$

Поскольку правила упрощения включают упрощение и распространение, все правила CHR следуют формату

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

где каждый из является конъюнкцией ограничений: и содержат ограничения CHR, в то время как охранники встроены. Только один из должен быть непустым. $H_{k},H_{r},G,B$ $H_{k},H_{r}$ $B$ $G$ $H_{k},H_{r}$

Хост-язык также должен определять встроенные ограничения для терминов. Охранники в правилах являются встроенными ограничениями, поэтому они эффективно выполняют код хост-языка. Теория встроенных ограничений должна включать по крайней мере true(ограничение, которое всегда выполняется), fail(ограничение, которое никогда не выполняется и используется для сигнализации об отказе) и равенство терминов, т. е. унификацию . ^[7] Если хост-язык не поддерживает эти функции, они должны быть реализованы вместе с CHR. ^[9]

Выполнение программы CHR начинается с начального хранилища ограничений. Затем программа продолжает сопоставлять правила с хранилищем и применять их, пока не будет больше совпадений правил (успех) или failне будет получено ограничение. В первом случае хранилище ограничений может быть считано программой на хост-языке для поиска интересующих фактов. Сопоставление определяется как «односторонняя унификация»: оно связывает переменные только с одной стороны уравнения. Сопоставление с образцом может быть легко реализовано, когда как унификация поддерживается хост-языком. ^[9]

Пример программы

Следующая программа CHR в синтаксисе Prolog содержит четыре правила, которые реализуют решатель для ограничения «меньше или равно» . Правила помечены для удобства (метки необязательны в CHR).

 % X leq Y означает, что переменная X меньше или равна переменной Y  рефлексивность  @  X  leq  X  <=>  true .  антисимметрия  @  X  leq  Y ,  Y  leq  X  <=>  X  =  Y .  транзитивность  @  X  leq  Y ,  Y  leq  Z  ==>  X  leq  Z .  идемпотентность  @  X  leq  Y  \  X  leq  Y  <=>  true .

Правила можно читать двумя способами. В декларативном прочтении три правила определяют аксиомы частичного порядка :

Рефлексивность: X ≤ X
Антисимметрия: если X ≤ Y и Y ≤ X , то X = Y
Транзитивность: если X ≤ Y и Y ≤ Z , то X ≤ Z

Все три правила неявно универсально квантифицированы (идентификаторы в верхнем регистре являются переменными в синтаксисе Пролога). Правило идемпотентности является тавтологией с логической точки зрения, но имеет цель во втором чтении программы.

Второй способ прочитать вышеизложенное — это компьютерная программа для поддержки хранилища ограничений, набора фактов (ограничений) об объектах. Хранилище ограничений не является частью этой программы, но должно поставляться отдельно. Правила выражают следующие правила вычислений:

Рефлексивность — это правило упрощения : оно выражает, что если в хранилище обнаружен факт вида X ≤ X , то его можно удалить.
Антисимметрия также является правилом упрощения, но с двумя головками . Если в хранилище можно найти два факта вида X ≤ Y и Y ≤ X (с совпадающими X и Y ), то их можно заменить одним фактом X = Y . Такое ограничение равенства считается встроенным и реализуется как унификация , которая обычно обрабатывается базовой системой Prolog.
Транзитивность — это правило распространения . В отличие от упрощения, она ничего не удаляет из хранилища ограничений; вместо этого, когда в хранилище находятся факты вида X ≤ Y и Y ≤ Z (с одинаковым значением для Y ), может быть добавлен третий факт X ≤ Z.
Идемпотентность, наконец, является правилом симпагации , комбинированным упрощением и распространением. Когда он находит дублирующиеся факты, он удаляет их из хранилища. Дубликаты могут возникать, поскольку хранилища ограничений являются множественными наборами фактов.

Учитывая запрос

А, В, С, С, А

могут произойти следующие преобразования:

Текущие ограничения	Правило, применимое к ограничениям	Вывод из применения правила
`A leq B, B leq C, C leq A`	транзитивность	`A leq C`
`A leq B, B leq C, C leq A, A leq C`	антисимметрия	`A = C`
`A leq B, B leq A, A = C`	антисимметрия	`A = B`
`A = B, A = C`	никто

Правило транзитивности добавляет A leq C. Затем, применяя правило антисимметрии , A leq Cи C leq Aудаляются и заменяются на A = C. Теперь правило антисимметрии становится применимым к первым двум ограничениям исходного запроса. Теперь все ограничения CHR устранены, поэтому никакие дальнейшие правила не могут быть применены, и A = B, A = Cвозвращается ответ: CHR правильно вывел, что все три переменные должны ссылаться на один и тот же объект.

Реализация программ CHR

Чтобы решить, какое правило должно «сработать» на данном хранилище ограничений, реализация CHR должна использовать некоторый алгоритм сопоставления шаблонов . Алгоритмы-кандидаты включают RETE и TREAT, ^[12] но большинство реализаций используют ленивый алгоритм, называемый LEAPS . ^[13]

Первоначальная спецификация семантики CHR была полностью недетерминированной, но так называемая «усовершенствованная семантика операций» Дака и др. устранила большую часть недетерминизма, так что разработчики приложений могут полагаться на порядок выполнения для производительности и правильности своих программ. ^[5]^[14]

Большинство приложений CHR требуют, чтобы процесс переписывания был конфлюэнтным ; в противном случае результаты поиска удовлетворяющего назначения будут недетерминированными и непредсказуемыми. Установление конфлюэнтности обычно осуществляется с помощью следующих трех свойств: ^[2]

Программа CHR локально конфлюэнтна, если все ее критические пары являются объединяемыми .
Программа CHR называется завершающейся, если нет бесконечных вычислений.
Завершающая программа CHR является конфлюэнтной, если все ее критические пары являются соединяемыми .

Смотрите также

Ссылки

^ Том Фрювирт. Введение в правила упрощения . Внутренний отчет ECRC-LP-63, ECRC Мюнхен, Германия, октябрь 1991 г., представленный на семинаре Logisches Programmieren, Гозен/Берлин, Германия, октябрь 1991 г. и семинаре по переписыванию и ограничениям, Дагштуль, Германия, октябрь 1991 г.
^ ab Thom Frühwirth. Теория и практика правил обработки ограничений . Специальный выпуск по программированию логики ограничений (редакторы P. Stuckey и K. Marriott), Journal of Logic Programming , том 37(1-3), октябрь 1998 г. doi :10.1016/S0743-1066(98)10005-5
^ Даль, Вероника и Дж. Эмилио Мираллес. «Womb grammars: Constraint resolver for grammar induction». Труды 9-го семинара по правилам обработки ограничений. т. Технический отчет CW. Т. 624. 2012.
^ Алвес, Сандра и Марио Флоридо. «Вывод типа с использованием правил обработки ограничений». Electronic Notes in Theoretical Computer Science 64 (2002): 56-72.
^ abc Sneyers, Jon; Van Weert, Peter; Schrijvers, Tom; De Koninck, Leslie (2009). "As time go by: Constraint Handling Rules – A Survey of CHR Research between 1998 and 2007" (PDF) . Теория и практика логического программирования . 10 : 1. arXiv : 0906.4474 . doi :10.1017/S1471068409990123. S2CID 11044594.
^ Frühwirth, Thom (2009). Правила обработки ограничений . Cambridge University Press. ISBN 978-0521877763.
^ ab Sneyers, Jon; Schrijvers, Tom; Demoen, Bart (2009). «Вычислительная мощность и сложность правил обработки ограничений» (PDF) . ACM Transactions on Programming Languages and Systems . 31 (2): 1–42. doi :10.1145/1462166.1462169. S2CID 2691882.
^ "CHR: Библиотека правил обработки ограничений". GitHub . 5 сентября 2021 г.
^ abc Питер Ван Верт; Питер Вилле; Том Шрийверс; Барт Демоен. «CHR для императивных принимающих языков». Правила обработки ограничений: текущие темы исследований . Спрингер.
^ "Конвертер CHR2 в SQL". GitHub . 15 марта 2021 г.
^ CHR.js — CHR-транспилятор для JavaScript
^ Миранкер, Дэниел П. (13–17 июля 1987 г.). «TREAT: Лучший алгоритм соответствия для систем производства искусственного интеллекта» (PDF) . AAAI'87: Труды шестой Национальной конференции по искусственному интеллекту . Сиэтл, Вашингтон: Ассоциация по развитию искусственного интеллекта, AAAI. стр. 42–47. ISBN 978-0-262-51055-4.
^ Лесли Де Конинк (2008). Управление выполнением правил обработки ограничений (PDF) (кандидатская диссертация). Католический университет Левена . стр. 12–14.
^ Дак, Грегори Дж.; Стаки, Питер Дж.; Гарсия де ла Банда, Мария ; Хольцбаур, Кристиан (2004). «Усовершенствованная операционная семантика правил обработки ограничений» (PDF) . Логическое программирование . Конспект лекций по информатике. Том 3132. С. 90–104. doi :10.1007/978-3-540-27775-0_7. ISBN 978-3-540-22671-0. Архивировано из оригинала (PDF) 2011-03-04 . Получено 2014-12-23 .

Дальнейшее чтение

Кристиансен, Хеннинг. «CHR-грамматики». Теория и практика логического программирования 5.4-5 (2005): 467-501.

Внешние ссылки

Официальный сайт
Библиография CHR
Список рассылки CHR
Система KULeuven CHR
WebCHR: веб-интерфейс CHR

[1] Том Фрювирт. Введение в правила упрощения . Внутренний отчет ECRC-LP-63, ECRC Мюнхен, Германия, октябрь 1991 г., представленный на семинаре Logisches Programmieren, Гозен/Берлин, Германия, октябрь 1991 г. и семинаре по переписыванию и ограничениям, Дагштуль, Германия, октябрь 1991 г.

[chrtheorypractice-2] Thom Frühwirth. Теория и практика правил обработки ограничений . Специальный выпуск по программированию логики ограничений (редакторы P. Stuckey и K. Marriott), Journal of Logic Programming , том 37(1-3), октябрь 1998 г. doi :10.1016/S0743-1066(98)10005-5

[3] Даль, Вероника и Дж. Эмилио Мираллес. «Womb grammars: Constraint resolver for grammar induction». Труды 9-го семинара по правилам обработки ограничений. т. Технический отчет CW. Т. 624. 2012.

[4] Алвес, Сандра и Марио Флоридо. «Вывод типа с использованием правил обработки ограничений». Electronic Notes in Theoretical Computer Science 64 (2002): 56-72.

[timegoesby-5] Sneyers, Jon; Van Weert, Peter; Schrijvers, Tom; De Koninck, Leslie (2009). "As time go by: Constraint Handling Rules – A Survey of CHR Research between 1998 and 2007" (PDF) . Теория и практика логического программирования . 10 : 1. arXiv : 0906.4474 . doi :10.1017/S1471068409990123. S2CID 11044594.

[chrbook-6] Frühwirth, Thom (2009). Правила обработки ограничений . Cambridge University Press. ISBN 978-0521877763.

[complexity-7] Sneyers, Jon; Schrijvers, Tom; Demoen, Bart (2009). «Вычислительная мощность и сложность правил обработки ограничений» (PDF) . ACM Transactions on Programming Languages and Systems . 31 (2): 1–42. doi :10.1145/1462166.1462169. S2CID 2691882.

[8] "CHR: Библиотека правил обработки ограничений". GitHub . 5 сентября 2021 г.

[imperative-9] Питер Ван Верт; Питер Вилле; Том Шрийверс; Барт Демоен. «CHR для императивных принимающих языков». Правила обработки ограничений: текущие темы исследований . Спрингер.

[10] "Конвертер CHR2 в SQL". GitHub . 15 марта 2021 г.

[11] CHR.js — CHR-транспилятор для JavaScript

[12] Миранкер, Дэниел П. (13–17 июля 1987 г.). «TREAT: Лучший алгоритм соответствия для систем производства искусственного интеллекта» (PDF) . AAAI'87: Труды шестой Национальной конференции по искусственному интеллекту . Сиэтл, Вашингтон: Ассоциация по развитию искусственного интеллекта, AAAI. стр. 42–47. ISBN 978-0-262-51055-4.

[13] Лесли Де Конинк (2008). Управление выполнением правил обработки ограничений (PDF) (кандидатская диссертация). Католический университет Левена . стр. 12–14.

[14] Дак, Грегори Дж.; Стаки, Питер Дж.; Гарсия де ла Банда, Мария ; Хольцбаур, Кристиан (2004). «Усовершенствованная операционная семантика правил обработки ограничений» (PDF) . Логическое программирование . Конспект лекций по информатике. Том 3132. С. 90–104. doi :10.1007/978-3-540-27775-0_7. ISBN 978-3-540-22671-0. Архивировано из оригинала (PDF) 2011-03-04 . Получено 2014-12-23 .