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

Правила обработки ограничений
Под влиянием
Парадигма	Программирование логики ограничений
Разработано	Том Фрювирт
Впервые появился	1991 г.
Пролог

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

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

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

Обзор языка [ править ]

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

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

Правила упрощения имеют форму . Когда они совпадают с головами и держателями охранников , правила упрощения могут переписать головы в тело . ${\ 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}}$
Правила распространения имеют форму . Эти правила добавляют ограничения в теле к магазину, не убирая головы. $h_{1},\dots ,h_{n}\Longrightarrow g_{1},\dots ,g_{m}\,|\,b_{1},\dots ,b_{o}$
Правила Simpagation сочетают в себе упрощение и распространение. Они написаны . Чтобы сработало правило упрощения, хранилище ограничений должно соответствовать всем правилам в голове, а охранники должны выполняться. Эти ограничения , которые были представлены сохраняются, как в правиле распространения; остальные ограничения снимаются. $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(ограничение, которое никогда не выполняется и используется для сигнализации отказа) и равенство условий, т. Е. Унификацию . ^[6] Если основной язык не поддерживает эти функции, они должны быть реализованы вместе с CHR. ^[7]

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

Пример программы [ править ]

Следующая программа 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  <=>  истина .

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

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

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

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

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

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

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 должна использовать некоторый алгоритм сопоставления с образцом . Алгоритмы кандидатов включают сплетение и угощения , но и максимально использовать реализацию по ленивому алгоритму называется LEAPS . ^[10]

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

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

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

См. Также [ править ]

Ограниченное программирование
Программирование логики ограничений
Логическое программирование
Системы производственных правил
Механизмы бизнес-правил
Перезапись

Ссылки [ править ]

^ Thom Frühwirth. Введение в правила упрощения . Внутренний отчет ECRC-LP-63, ECRC Мюнхен, Германия, октябрь 1991 г., представлен на семинаре Logisches Programmieren, Гузен / Берлин, Германия, октябрь 1991 г. и семинаре по переписыванию и ограничениям, Дагштуль, Германия, октябрь 1991 г.
^ a b Том Фрювирт. Теория и практика правил обработки ограничений . Специальный выпуск по программированию логики в ограничениях (П. Стаки и К. Марриотт, ред.), Журнал логического программирования, том 37 (1-3), октябрь 1998 г. doi : 10.1016 / S0743-1066 (98) 10005-5
↑ Даль, Вероника и Дж. Эмилио Мираллес. « Грамматики матки: решение ограничений для индукции грамматики ». Труды 9-го семинара по правилам обработки ограничений. т. Технический отчет CW. Vol. 624.2012.
^ a b c Снейерс, Джон; Ван Верт, Питер; Шрайверс, Том; Де Конинк, Лесли (2009). «Время идет: Правила обработки ограничений - обзор исследований CHR за период с 1998 по 2007 год» (PDF) . Теория и практика логического программирования . 10 : 1. arXiv : 0906.4474 . DOI : 10.1017 / S1471068409990123 .
^ Frühwirth, Thom (2009). Правила обработки ограничений . Издательство Кембриджского университета. ISBN 0521877768.
^ a b Снейерс, Джон; Шрайверс, Том; Демоэн, Барт (2009). «Вычислительная мощность и сложность правил обработки ограничений» (PDF) . ACM Trans. Программа. Lang. Syst . 31 (2).
^ a b c Питер Ван Верт; Питер Уилле; Том Шрайверс; Барт Демоэн. «CHR для императивных языков хоста» . Правила обработки ограничений - текущие темы исследований . Springer.
^ https://github.com/awto/chr2sql
^ CHR.js - Транспилятор CHR для JavaScript
^ Лесли Де Конинк (2008). Контроль выполнения для правил обработки ограничений (PDF) (кандидатская диссертация). Katholieke Universiteit Leuven . С. 12–14.
^ Дак, Грегори Дж .; Стаки, Питер Дж .; Гарсиа де ла Банда, Мария; Хольцбаур, Кристиан (2004). «Усовершенствованная операционная семантика правил обработки ограничений» (PDF) . Логическое программирование : 90–104. Архивировано из оригинального (PDF) 04 марта 2011 года . Проверено 23 декабря 2014 .

Дальнейшее чтение [ править ]

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

Внешние ссылки [ править ]

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

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

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

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

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

[chrbook-5] Frühwirth, Thom (2009). Правила обработки ограничений . Издательство Кембриджского университета. ISBN 0521877768.

[complexity-6] Снейерс, Джон; Шрайверс, Том; Демоэн, Барт (2009). «Вычислительная мощность и сложность правил обработки ограничений» (PDF) . ACM Trans. Программа. Lang. Syst . 31 (2).

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

[8] ttps://github.com/awto/chr2sql

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

[10] Лесли Де Конинк (2008). Контроль выполнения для правил обработки ограничений (PDF) (кандидатская диссертация). Katholieke Universiteit Leuven . С. 12–14.

[11] Дак, Грегори Дж .; Стаки, Питер Дж .; Гарсиа де ла Банда, Мария; Хольцбаур, Кристиан (2004). «Усовершенствованная операционная семантика правил обработки ограничений» (PDF) . Логическое программирование : 90–104. Архивировано из оригинального (PDF) 04 марта 2011 года . Проверено 23 декабря 2014 .

[1]