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

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

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

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

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

Обзор языка

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

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

Правила упрощения имеют вид $h_{1},\dots ,h_{n}\Longleftrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$ . Когда они совпадают с головами $h_{1},\dots ,h_{n}$ и охранники $g_{1},\dots ,g_{m}$ держись, правила упрощения могут переписать головы в тело $b_{1},\dots ,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

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

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

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

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

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

 % X leq Y means variable X is less-or-equal to variable Y 
 reflexivity  @ X leq X <=> true.
 antisymmetry @ X leq Y, Y leq X <=> X = Y.
 transitivity @ X leq Y, Y leq Z ==> X leq Z.
 idempotence  @ 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. (с совпадением Такое ограничение равенства считается встроенным и реализуется как унификация , которая обычно обрабатывается базовой системой Пролога.
Транзитивность — это правило распространения . В отличие от упрощения, оно ничего не удаляет из хранилища ограничений; вместо этого, когда факты формы X ≤ Y и Y ≤ Z (с тем же значением для Y ) находятся в хранилище, третий факт X ≤ Z. может быть добавлен
Наконец, идемпотентность — это правило симпагации , комбинированное упрощение и распространение. Когда он находит повторяющиеся факты, он удаляет их из хранилища. Могут возникать дубликаты, поскольку хранилища ограничений представляют собой несколько наборов фактов.

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

A leq B, B leq C, C leq A

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

Текущие ограничения	Правило, применимое к ограничениям	Вывод из применения правил
`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 была полностью недетерминированной, но так называемая «уточненная семантика операций» Duck et al. удалена большая часть недетерминированности, так что авторы приложений могут полагаться на порядок выполнения для производительности и правильности своих программ. ^[5]^[14]

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

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

См. также

Ссылки

^ Том Фрювирт. Знакомство с правилами упрощения . Внутренний отчет ECRC-LP-63, ECRC, Мюнхен, Германия, октябрь 1991 г., представлен на семинаре Logisches Programmieren, Гузен/Берлин, Германия, октябрь 1991 г., и семинаре по переписыванию и ограничениям, Дагштуль, Германия, октябрь 1991 г.
^ Перейти обратно: ^а ^б Том Фрювирт. Теория и практика правил обработки ограничений . Специальный выпуск по программированию логики с ограничениями (П. Стаки и К. Марриотт, ред.), Журнал логического программирования , том 37 (1-3), октябрь 1998 г. два : 10.1016/S0743-1066(98)10005-5
^ Даль, Вероника и Дж. Эмилио Мираллес. « Грамматики матки: решение ограничений для индукции грамматики ». Материалы 9-го семинара по правилам обработки ограничений. том. Технический отчет CW. Том. 624. 2012.
^ Алвес, Сандра и Марио Флоридо. « Вывод типа с использованием правил обработки ограничений ». Электронные заметки по теоретической информатике 64 (2002): 56–72.
^ Перейти обратно: ^а ^б ^с Снейерс, Джон; Ван Верт, Питер; Шрийверс, Том; Де Конинк, Лесли (2009). «Со временем: Правила обработки ограничений – обзор исследований CHR в период с 1998 по 2007 год» (PDF) . Теория и практика логического программирования . 10 : 1.arXiv : 0906.4474 . дои : 10.1017/S1471068409990123 . S2CID 11044594 .
^ Фрювирт, Том (2009). Правила обработки ограничений . Издательство Кембриджского университета. ISBN 978-0521877763 .
^ Перейти обратно: ^а ^б Снейерс, Джон; Шрийверс, Том; Демоэн, Барт (2009). «Вычислительная мощность и сложность правил обработки ограничений» (PDF) . Транзакции ACM в языках и системах программирования . 31 (2): 1–42. дои : 10.1145/1462166.1462169 . S2CID 2691882 .
^ «CHR: Библиотека правил обработки ограничений» . Гитхаб . 5 сентября 2021 г.
^ Перейти обратно: ^а ^б ^с Питер Ван Верт; Питер Вилле; Том Писатели; Барт Демоэн. «CHR для императивных основных языков» . Правила обработки ограничений: текущие темы исследований . Спрингер.
^ «Конвертер CHR2 в SQL» . Гитхаб . 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. дои : 10.1007/978-3-540-27775-0_7 . ISBN 978-3-540-22671-0 . Архивировано из оригинала (PDF) 4 марта 2011 г. Проверено 23 декабря 2014 г.

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

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

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

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

[chrtheorypractice-2] Перейти обратно: ^а ^б Том Фрювирт. Теория и практика правил обработки ограничений . Специальный выпуск по программированию логики с ограничениями (П. Стаки и К. Марриотт, ред.), Журнал логического программирования , том 37 (1-3), октябрь 1998 г. два : 10.1016/S0743-1066(98)10005-5

[3] Даль, Вероника и Дж. Эмилио Мираллес. « Грамматики матки: решение ограничений для индукции грамматики ». Материалы 9-го семинара по правилам обработки ограничений. том. Технический отчет CW. Том. 624. 2012.

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

[timegoesby-5] Перейти обратно: ^а ^б ^с Снейерс, Джон; Ван Верт, Питер; Шрийверс, Том; Де Конинк, Лесли (2009). «Со временем: Правила обработки ограничений – обзор исследований CHR в период с 1998 по 2007 год» (PDF) . Теория и практика логического программирования . 10 : 1.arXiv : 0906.4474 . дои : 10.1017/S1471068409990123 . S2CID 11044594 .

[chrbook-6] Фрювирт, Том (2009). Правила обработки ограничений . Издательство Кембриджского университета. ISBN 978-0521877763 .

[complexity-7] Перейти обратно: ^а ^б Снейерс, Джон; Шрийверс, Том; Демоэн, Барт (2009). «Вычислительная мощность и сложность правил обработки ограничений» (PDF) . Транзакции ACM в языках и системах программирования . 31 (2): 1–42. дои : 10.1145/1462166.1462169 . S2CID 2691882 .

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

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

[10] «Конвертер CHR2 в SQL» . Гитхаб . 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. дои : 10.1007/978-3-540-27775-0_7 . ISBN 978-3-540-22671-0 . Архивировано из оригинала (PDF) 4 марта 2011 г. Проверено 23 декабря 2014 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]