Логическое программирование с ограничениями: язык CHR
Constraint Handling Rules
CHR: декларативный язык логического программирования с ограничениями. Применение: от грамматической индукции до верификации. Правила, ограничения, мультиагентные системы.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
Язык логического программирования с ограничениями, работающий параллельно
Concurrent constraint logic programming language
Constraint Handling Rules (CHR) — это декларативный язык программирования, основанный на правилах, разработанный в 1991 году Томом Фрюхвиртом в Европейском исследовательском центре компьютерной промышленности (ECRC) в Мюнхене, Германия. Изначально предназначенный для программирования с ограничениями, CHR находит применение в грамматической индукции, типовых системах, абдуктивном рассуждении, многоагентных системах, обработке естественного языка, компиляции, планировании, пространственно-временном рассуждении, тестировании и верификации. Программа CHR, иногда называемая обработчиком ограничений, представляет собой набор правил, поддерживающих хранилище ограничений — мультимножество логических формул. Выполнение правил может добавлять или удалять формулы из хранилища, тем самым изменяя состояние программы. Порядок, в котором правила "активируются" для данного хранилища ограничений, является недетерминированным согласно своей абстрактной семантике и детерминированным (применение правил сверху вниз) согласно своей уточненной семантике. Хотя CHR является Тьюринг-полным, он редко используется как самостоятельный язык программирования. Скорее, он применяется для расширения языка-хоста возможностями работы с ограничениями. Prolog является наиболее популярным языком-хостом, и CHR включен в несколько реализаций Prolog, таких как SICStus и SWI-Prolog, хотя реализации CHR также существуют для Haskell, Java, C, SQL и JavaScript. В отличие от Prolog, правила CHR многоголовы и выполняются с фиксированным выбором, используя алгоритм прямого распространения.
Constraint Handling Rules (CHR) is a declarative, rule based programming language, introduced in 1991 by Thom Frühwirth at the time with European Computer Industry Research Centre (ECRC) in Munich, Germany. Originally intended for constraint programming, CHR finds applications in grammar induction, type systems, abductive reasoning, multi agent systems, natural language processing, compilation, scheduling, spatial temporal reasoning, testing, and verification. A CHR program, sometimes called a constraint handler, is a set of rules that maintain a constraint store, a multi set of logical formulas. Execution of rules may add or remove formulas from the store, thus changing the state of the program. The order in which rules "fire" on a given constraint store is non deterministic, according to its abstract semantics and deterministic (top down rule application), according to its refined semantics. Although CHR is Turing complete, it is not commonly used as a programming language in its own right. Rather, it is used to extend a host language with constraints. Prolog is by far the most popular host language and CHR is included in several Prolog implementations, including SICStus and SWI Prolog, although CHR implementations also exist for Haskell, Java, C, SQL, and JavaScript. In contrast to Prolog, CHR rules are multi headed and are executed in a committed choice manner using a forward chaining algorithm.
Обзор языков
Конкретный синтаксис программ CHR зависит от языка-хоста, и на самом деле программы встраивают в язык-хост операторы, которые выполняются для обработки некоторых правил. Язык-хост предоставляет структуру данных для представления термов, включая логические переменные. Термы представляют собой ограничения, которые можно рассматривать как «факты» о проблемной области программы. Традиционно в качестве языка-хоста используется Prolog, поэтому используются его структуры данных и переменные. В остальной части этого раздела используется нейтральная математическая нотация, общепринятая в литературе по CHR. Таким образом, программа CHR состоит из правил, которые манипулируют мульти-множеством этих термов, называемым хранилищем ограничений. Правила бывают трех типов: но большинство реализаций используют ленивый алгоритм, называемый LEAPS. Изначальная спецификация семантики CHR была полностью недетерминированной, но так называемая «уточнённая операционная семантика» Duck и др. устранила большую часть недетерминизма, чтобы разработчики приложений могли полагаться на порядок выполнения для производительности и корректности своих программ. Большинство приложений CHR требуют, чтобы процесс переписывания был конфлюэнтным; в противном случае результаты поиска удовлетворяющего назначения будут недетерминированными и непредсказуемыми. Установление конфлюэнтности обычно осуществляется посредством следующих трех свойств:
The concrete syntax of CHR programs depends on the host language, and in fact programs embed statements in the host language that are executed to handle some rules. The host language supplies a data structure for representing terms, including logical variables. Terms represent constraints, which can be thought of as "facts" about the program's problem domain. Traditionally, Prolog is used as the host language, so its data structures and variables are used. The rest of this section uses a neutral, mathematical notation that is common in the CHR literature. A CHR program, then, consists of rules that manipulate a multi set of these terms, called the constraint store. Rules come in three types: but most implementation use a lazy algorithm called LEAPS. The original specification of CHR's semantics was entirely non deterministic, but the so called "refined operation semantics" of Duck et al. removed much of the non determinism so that application writers can rely on the order of execution for performance and correctness of their programs. Most applications of CHRs require that the rewriting process be confluent; otherwise the results of searching for a satisfying assignment will be nondeterministic and unpredictable. Establishing confluence is usually done by way of the following three properties:
Программа CHR является локально конфлюэнтной, если все её критические пары объединимы. Программа CHR называется завершающейся, если в ней нет бесконечных вычислений. Завершающаяся программа CHR является конфлюэнтной, если все её критические пары объединимы.
A CHR program is locally confluent if all its critical pairs are joinable. A CHR program is called terminating if there are no infinite computations. A terminating CHR program is confluent if all its critical pairs are joinable.