Конкурентное логическое программирование с ограничениями

Введение

Одновременное логическое программирование с ограничениями – это версия логического программирования с ограничениями, ориентированная главным образом на программирование параллельных процессов, а не (или в дополнение к) решению задач об удовлетворении ограничениям. Цели в логическом программировании с ограничениями вычисляются параллельно; следовательно, параллельный процесс программируется как вычисление цели интерпретатором. Синтаксически, программы одновременной логики ограничений похожи на последовательные программы, за исключением того, что клаузы включают охранные условия – это ограничения, которые могут блокировать применимость клаузы при определенных условиях. Семантически, одновременное логическое программирование с ограничениями отличается от своих последовательных версий тем, что вычисление цели предназначено для реализации параллельного процесса, а не для поиска решения задачи. Наиболее заметно, это различие влияет на поведение интерпретатора, когда применимо несколько клауз: последовательное логическое программирование с ограничениями рекурсивно перебирает все клаузы, а одновременное логическое программирование с ограничениями выбирает только одну. Это наиболее явный эффект заданной направленности интерпретатора, который никогда не пересматривает ранее принятое решение. Другие последствия этого – семантическая возможность наличия цели, которую нельзя доказать, при этом всё вычисление не завершается неудачей, и особый способ сопоставления цели и заголовка клаузы. Правила обработки ограничений можно рассматривать как форму одновременного логического программирования с ограничениями, но они используются для программирования упростителей или решателей ограничений, а не параллельных процессов.

Описание

В программировании с логикой ограничений цели текущей цели оцениваются последовательно, обычно в порядке LIFO, при котором новые цели оцениваются первыми. Параллельная версия логического программирования позволяет оценивать цели параллельно: каждая цель оценивается процессом, и процессы выполняются одновременно. Эти процессы взаимодействуют посредством хранилища ограничений: один процесс может добавить ограничение в хранилище, а другой проверить, следует ли это ограничение из хранилища. Добавление ограничения в хранилище выполняется как в обычном программировании с логикой ограничений. Проверка следования ограничения осуществляется с помощью охранных условий. Охранным условиям требуется синтаксическое расширение: пункт конкурентного логического программирования с ограничениями записывается как H : G | B, где G — это ограничение, называемое охранным условием пункта. Грубо говоря, новый вариант этого пункта может быть использован для замены литерала в цели только в том случае, если охранное условие следует из хранилища ограничений после добавления в него уравнения литерала и заголовка пункта. Точное определение этого правила более сложное и приведено ниже. Основное различие между неконкурентным и конкурентным программированием с ограничениями заключается в том, что первое ориентировано на поиск, а второе — на реализацию конкурентных процессов. Это различие влияет на возможность отмены выбора, допустимость незавершающихся процессов и способ уравнивания целей и заголовков пунктов. Первое семантическое различие между обычным и конкурентным логическим программированием с ограничениями касается условия, при котором для доказательства цели можно использовать более одного пункта. Неконкурентное логическое программирование пытается переписать цель, перебирая все возможные пункты: если цель не может быть доказана заменой ее телом нового варианта пункта, то проверяется другой пункт, если он существует. Это связано с тем, что цель состоит в доказательстве цели: перебираются все возможные способы ее доказательства. С другой стороны, конкурентное логическое программирование с ограничениями направлено на программирование параллельных процессов. В общем случае конкурентного программирования, если процесс делает выбор, этот выбор не может быть отменен. Конкурентная версия логического программирования с ограничениями реализует процессы, позволяя им делать выбор, но фиксируя его после принятия. Технически, если для переписывания литерала в цели можно использовать более одного пункта, неконкурентная версия последовательно перебирает все пункты, а конкурентная версия выбирает один произвольный пункт: в отличие от неконкурентной версии, другие пункты никогда не будут пробоваться. Эти два различных способа обработки множественного выбора часто называют «неопределенностью незнания» и «неопределенностью безразличия». При переписывании литерала в цели рассматриваются только те пункты, чье охранное условие следует из объединения хранилища ограничений и уравнения литерала с заголовком пункта. Охранные условия позволяют определить, какие пункты вообще не следует рассматривать. Это особенно важно, учитывая фиксацию выбора одного пункта в конкурентном логическом программировании с ограничениями: как только пункт выбран, этот выбор больше никогда не будет пересмотрен. Без охранных условий интерпретатор мог бы выбрать «неправильный» пункт для переписывания литерала, в то время как другие «правильные» пункты существуют. В неконкурентном программировании это менее важно, поскольку интерпретатор всегда перебирает все возможности. В конкурентном программировании интерпретатор фиксируется на одной возможности, не перебирая другие. Второй эффект различия между неконкурентной и конкурентной версиями заключается в том, что конкурентное логическое программирование с ограничениями специально разработано для того, чтобы процессы могли выполняться без завершения. Незавершающиеся процессы часто встречаются в конкурентной обработке; конкурентная версия логического программирования с ограничениями реализует их, не используя условие неудачи: если для переписывания цели не применимо ни одного пункта, процесс, оценивающий эту цель, останавливается, а не приводит к неудаче всей оценки, как в неконкурентном логическом программировании с ограничениями. В результате процесс, оценивающий цель, может быть остановлен из-за отсутствия доступных пунктов для продолжения, но при этом другие процессы продолжают выполняться. Синхронизация между процессами, решающими различные цели, достигается с помощью охранных условий. Если цель не может быть переписана, потому что все пункты, которые можно было бы использовать, имеют охранное условие, которое не следует из хранилища ограничений, процесс, решающий эту цель, блокируется до тех пор, пока другие процессы не добавят ограничения, необходимые для следования охранного условия хотя бы одного из применимых пунктов. Эта синхронизация подвержена взаимным блокировкам: если все цели заблокированы, новые ограничения не будут добавлены, и, следовательно, ни одна цель никогда не будет разблокирована. Третий эффект различия между конкурентным и неконкурентным логическим программированием заключается в способе уравнивания цели с заголовком нового варианта пункта. Операционно это делается путем проверки, можно ли уравнять переменные в заголовке с термами таким образом, чтобы заголовок был равен цели. Это правило отличается от соответствующего правила для логического программирования с ограничениями тем, что оно разрешает добавлять только ограничения вида переменная=терм, где переменная является одной из переменных заголовка. Это ограничение можно рассматривать как форму направленности, поскольку цель и заголовок пункта обрабатываются по-разному. Точнее, правило, определяющее, можно ли использовать новый вариант H : G | B пункта для переписывания цели A, следующее. Во-первых, проверяется, имеют ли A и H один и тот же предикат. Во-вторых, проверяется, существует ли способ уравнять A и H с учетом текущего хранилища ограничений; в отличие от обычного логического программирования, это делается с использованием односторонной унификации, которая разрешает только переменной заголовка быть равной терму. В-третьих, охранное условие проверяется на следование из хранилища ограничений и уравнений, сгенерированных на втором шаге; охранное условие может содержать переменные, которые не упоминаются в заголовке пункта: эти переменные интерпретируются экзистенциально. Этот метод определения применимости нового варианта пункта для замены цели можно компактно выразить следующим образом: текущее хранилище ограничений следует, что существует оценка переменных заголовка и охранного условия такая, что заголовок равен цели и охранное условие следует. На практике следование может проверяться неполным методом. Расширением синтаксиса и семантики конкурентного логического программирования является атомарное добавление ограничений. Когда интерпретатор использует пункт, его охранное условие добавляется в хранилище ограничений. Однако также добавляются ограничения тела. Из-за фиксации выбора этого пункта интерпретатор не откатывается, если ограничения тела несовместимы с хранилищем. Этого можно избежать с помощью атомарного добавления ограничений, которое является вариантом, в котором пункт содержит своего рода «второе охранное условие», которое проверяется только на согласованность. Такой пункт записывается как H : G : D | B. Этот пункт используется для переписывания литерала только в том случае, если G следует из хранилища ограничений и D согласовано с ним. В этом случае и G, и D добавляются в хранилище ограничений.

In constraint logic programming, the goals in the current goal are evaluated sequentially, usually proceeding in a LIFO order in which newer goals are evaluated first. The concurrent version of logic programming allows for evaluating goals in parallel: every goal is evaluated by a process, and processes run concurrently. These processes interact via the constraint store: a process can add a constraint to the constraint store while another one checks whether a constraint is entailed by the store. Adding a constraint to the store is done like in regular constraint logic programming. Checking entailment of a constraint is done via guards to clauses. Guards require a syntactic extension: a clause of concurrent constraint logic programming is written as H : G | B where G is a constraint called the guard of the clause. Roughly speaking, a fresh variant of this clause can be used to replace a literal in the goal only if the guard is entailed by the constraint store after the equation of the literal and the clause head is added to it. The precise definition of this rule is more complicated, and is given below. The main difference between non concurrent and concurrent constraint logic programming is that the first is aimed at search, while the second is aimed at implementing concurrent processes. This difference affects whether choices can be undone, whether processes are allowed not to terminate, and how goals and clause heads are equated. The first semantical difference between regular and concurrent constraint logic programming is about the condition when more than one clause can be used for proving a goal. Non concurrent logic programming tries all possible clauses when rewriting a goal: if the goal cannot be proved while replacing it with the body of a fresh variant of a clause, another clause is proved, if any. This is because the aim is to prove the goal: all possible ways to prove the goal are tried. On the other hand, concurrent constraint logic programming aims at programming parallel processes. In general concurrent programming, if a process makes a choice, this choice cannot be undone. The concurrent version of constraint logic programming implements processes by allowing them to take choices, but committing to them once they have been taken. Technically, if more than one clause can be used to rewrite a literal in the goal, the non concurrent version tries in turn all clauses, while the concurrent version chooses a single arbitrary
clause: contrary to the non concurrent version, the other clauses will never be tried. These two different ways for handling multiple choices are often called "don't know nondeterminism" and "don't care nondeterminism". When rewriting a literal in the goal, the only considered clauses are those whose guard is entailed by the union of the constraint store and the equation of the literal with the clause head. The guards provide a way for telling which clauses are not to be considered at all. This is particularly important given the commitment to a single clause of concurrent constraint logic programming: once a clause has been chosen, this choice will be never reconsidered. Without guards, the interpreter could choose a "wrong" clause to rewrite a literal, while other "good" clauses exist. In non concurrent programming, this is less important, as the interpreter always tries all possibilities. In concurrent programming, the interpreter commits to a single possibility without trying the other ones. A second effect of the difference between the non concurrent and the concurrent version is that concurrent constraint logic programming is specifically designed to allow processes to run without terminating. Non terminating processes are common in general in concurrent processing; the concurrent version of constraint logic programming implements them by not using the condition of failure: if no clause is applicable for rewriting a goal, the process evaluating this goal stops instead of making the whole evaluation fail like in non concurrent constraint logic programming. As a result, the process evaluating a goal may be stopped because no clause is available to proceed, but at the same time the other processes keep running. Synchronization among processes that are solving different goals is achieved via the use of guards. If a goal cannot be rewritten because all clauses that could be used have a guard that is not entailed by the constraint store, the process solving this goal is blocked until the other processes add the constraints that are necessary to entail the guard of at least one of the applicable clauses. This synchronization is subject to deadlocks: if all goals are blocked, no new constraints will be added and therefore no goal will ever be unblocked. A third effect of the difference between concurrent and non concurrent logic programming is in the way a goal is equated to the head of a fresh variant of a clause. Operationally, this is done by checking whether the variables in the head can be equated to terms in such a way the head is equal to the goal. This rule differs from the corresponding rule for constraint logic programming in that it only allows adding constraints in the form variable=term, where the variable is one of the head. This limitation can be seen as a form of directionality, in that the goal and the clause head are treated differently. Precisely, the rule telling whether a fresh variant H: G|B of a clause can be used to rewrite a goal A is as follows. First, it is checked whether A and H have the same predicate. Second, it is checked whether there exists a way for equating with given the current constraint store; contrary to regular logic programming, this is done under one sided unification, which only allows a variable of the head to be equal to a term. Third, the guard is checked for entailment from the constraint store and the equations generated in the second step; the guard may contain variables that are not mentioned in the clause head: these variables are interpreted existentially. This method for deciding the applicability of a fresh variant of a clause for replacing a goal can be compactly expressed as follows: the current constraint store entails that there exists an evaluation of the variables of the head and the guard such that the head is equal to the goal and the guard is entailed. In practice, entailment may be checked with an incomplete method. An extension to the syntax and semantics of concurrent logic programming is the atomic tell. When the interpreter uses a clause, its guard is added to the constraint store. However, also added are the constraints of the body. Due to commitment to this clause, the interpreter does not backtrack if the constraints of the body are inconsistent with the store. This condition can be avoided by the use of atomic tell, which is a variant in which the clause contain a sort of "second guard" that is only checked for consistency. Such a clause is written H : G:D|B. This clause is used to rewrite a literal only if G is entailed by the constraint store and D is consistent with it. In this case, both G and D are added to the constraint store.

История

Изучение параллельного логического программирования с ограничениями началось в конце 1980-х годов, когда Майкл Дж. Махер интегрировал некоторые принципы параллельного логического программирования в логическое программирование с ограничениями. Теоретические свойства параллельного логического программирования с ограничениями позднее изучались различными авторами, включая Мартина Ринарда и Виджай А. Сарасват.