Content deleted Content added
m Robot: change redirected category Concurrent programming to Concurrent computing |
→Description: wikilink entailment using AWB |
||
Line 9:
In constraint logic programming, the goals in the current goal are evaluated sequentially, usually proceeding in a [[LIFO (computing)|LIFO]] order in which newer goals are evaluated first. The concurrent version of logic programming allows for evaluating goals in [[Parallel computing|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 [[Guard (computing)|guards]] to clauses. Guards require a syntactic extension: a clause of concurrent constraint logic programming is written as <code>H :- G | B</code> where <code>G</code> 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 and equated.
Line 24:
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 <code>H:-G|B</code> of a clause can be used to rewrite a goal <code>A</code> is as follows. First, it is checked whether <code>A</code> and <code>H</code> have the same predicate. Second, it is checked whether there exists a way for equating <math>A</math> with <math>H</math> 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 <code>H :- G:D|B</code>. This clause is used to rewrite a literal only if <code>G</code> is entailed by the constraint store and <code>D</code> is consistent with it. In this case, both <code>G</code> and <code>D</code> are added to the constraint store.
| |||