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

редактировать

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

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

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

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

Содержание

1 Обзор языка
- 1.1 Пример программы
2 Выполнение программ CHR
3 См. Также
4 Ссылки
5 Дополнительная литература
6 Внешние ссылки

Обзор языка

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

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

Правила упрощения имеют вид $h 1,…, h n ⟺ g 1,…, g m | b 1,…, bo {\ displaystyle h_ {1}, \ dots, h_ {n} \ Longleftrightarrow g_ {1}, \ dots, g_ {m} \, | \, b_ {1}, \ dots, b_ { о}}$ ${\ displaystyle h_ {1}, \ dots, h_ {n} \ Longleftrightarrow g_ {1}, \ dots, g_ {m} \, | \, b_ {1}, \ dots, b_ { o}}$ . Когда они совпадают с головками $h 1,…, hn {\ displaystyle h_ {1}, \ dots, h_ {n}}$ $h_1, \ dots, h_n$ и guards $g 1,…, Gm {\ displaystyle g_ {1}, \ dots, g_ {m}}$ $g_1, \ dots, g_m$ удерживайте, правила упрощения могут переписать головы в тело $b 1,…, bo {\ displaystyle b_ {1}, \ dots, b_ {o}}$ $b_1, \ dots, b_o$ .
Правила распространения имеют вид $h 1,…, hn ⟹ g 1,…, gm | b 1,…, bo {\ displaystyle h_ {1}, \ dots, h_ {n} \ Longrightarrow g_ {1}, \ dots, g_ {m} \, | \, b_ {1}, \ dots, b_ { о}}$ ${\ displaystyle h_ {1}, \ dots, h_ {n} \ Longrightarrow g_ {1}, \ dots, g_ {m} \, | \, b_ {1}, \ dots, b_ {o}}$ . Эти правила добавляют ограничения в теле к хранилищу, не удаляя заголовки.
Правила Simpagation сочетают в себе упрощение и распространение. Они записываются $h 1,…, h ℓ ∖ h ℓ + 1,…, h n ⟺ g 1,…, g m | b 1,…, bo {\ displaystyle h_ {1}, \ dots, h _ {\ ell} \, \ backslash \, h _ {\ ell +1}, \ dots, h_ {n} \ Longleftrightarrow g_ {1}, \ точки, g_ {m} \, | \, b_ {1}, \ dots, b_ {o}}$ ${\ 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}$ $\ ell$ до $∖ {\ displaystyle \ backslash}$ $\ обратная косая черта$ сохраняются как в правиле распространения; оставшиеся ограничения $n - ℓ {\ displaystyle n- \ ell}$ $n - \ ell$ удаляются.

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

H k ∖ H r ⟺ G | B {\ displaystyle H_ {k} \, \ backslash \, H_ {r} \ Longleftrightarrow G \, | \, B}

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

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

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

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

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

Следующая программа 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

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

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

Рефлексивность - это правило упрощения: оно выражает, что, если факт формы 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 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 и, но в большинстве реализаций используется вызываемый ленивый алгоритм.

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

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

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

См. также

Ссылки

Дополнительная литература

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

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