Правила обработки ограничений - Constraint Handling Rules

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

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

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

Обзор языка

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

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

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

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

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

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

Основной язык также должен определять встроенные ограничения терминов. Стражи в правилах - это встроенные ограничения, поэтому они эффективно выполняют код основного языка. Встроенная теория ограничений должна включать как минимум true(ограничение, которое всегда выполняется), fail(ограничение, которое никогда не выполняется и используется для сигнализации отказа) и равенство условий, т. Е. Унификацию . Если основной язык не поддерживает эти функции, они должны быть реализованы вместе с CHR.

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

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

Следующая программа CHR в синтаксисе Prolog содержит четыре правила, которые реализуют решатель для ограничения « меньше или равно» . Правила помечены для удобства (метки в 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 ), то они могут быть заменены одним фактом Х = Y . Такое ограничение равенства считается встроенным и реализуется как объединение , которое обычно обрабатывается базовой системой Prolog.
• Транзитивность - это правило распространения . В отличие от упрощения, он ничего не удаляет из хранилища ограничений; вместо этого, когда в магазине есть факты в форме X ≤ Y и Y ≤ Z (с тем же значением Y ), может быть добавлен третий факт X ≤ Z.
• Идемпотентности, наконец, это simpagation правило, комбинированное упрощение и распространение. Когда он находит повторяющиеся факты, он удаляет их из магазина. Дубликаты могут возникать, потому что хранилища ограничений - это множественные наборы фактов.

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

A leq B, B leq C, C leq A

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

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

Выполнение программ CHR

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

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

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

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

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

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

использованная литература

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

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

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

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