Constraint logic programming: Difference between revisions

Revision as of 23:04, 16 March 2006

Revision as of 23:37, 16 March 2006

Line 19:

==Semantics==

The semantics of constraint logic programs can be defined in terms of a virtual interpreter that maintains a pair <math>\langle G,S \rangle</math> during execution. The first element of this pair is called current goal; the second element is called constraint store. The ''current goal'' contains the literals the interpreter is trying to prove; it can also contain constraints and equalityequalities of terms are considered literals, so they can occur in the goal; the ''constraint store'' contains all constraints the interpreter has assumed satisfiable so far.

Initially, the current goal is the goal and the constraint store is empty. The interpreter proceed by removing the first element from the current goal and analyzing it. This analysis may end up in a [[Recursion|recursive call]] or a failure; the interpreter backtracks in the second case. It may also generate an addition of new literals to the current goal and an addition of new constraint to the constraint store. The interpreter stops when the current goal is empty and the constraint store is satisfiable.

Line 27:

Some checks are done during these operations. In particular, the constraint store is checked for consistency every time a new constraint is added to it. In principle, whenever the constraint store is unsatisfiable the algorithm could backtrack. However, checking unsatisfiability at each step would be inefficient. For this reason, an incomplete satisfiability checker may be used instead.

In practice, incomplete satisfiabilty is checked simplifying the constraint

The interpreter stops when the current goal is empty and the constraint store is not detected unsatisfiable.

store, that is, rewriting it into an equivalent but simpler form. Such a

simplification can sometimes but not always prove unsatisfiability of an

unsatisfiable constraint store.

The interpreter stops when the current goal is empty and the constraint store is not detected unsatisfiable. The result of execution is the current set of (simplified) constraints. This set may include constraints such as <math>X=2</math> that force variables to a specific value, but may also include constraints like <math>X>2</math> that only bound variables without giving them a specific value.

Formally, the semantics of constraint logic programming is defined in terms of ''derivations''. A transition is a pair of pairs goal/store, noted <math>\langle G,S \rangle \rightarrow \langle G',S' \rangle</math>. Such a pair states the possibility of going from state <math>\langle G,S \rangle</math> to state <math>\langle G',S' \rangle</math>. Such a transition is possible if:

Formally, the semantics of constraint logic programming is defined in terms of ''derivations''. A transition is a pair of pairs goal/store, noted <math>\langle G,S \rangle \rightarrow \langle G',S' \rangle</math>. Such a pair states the possibility of going from state <math>\langle G,S \rangle</math> to state <math>\langle G',S' \rangle</math>. Such a transition is possible ifin three possible cases:

* an element of <math>G</math> is a constraint <math>C</math>, <math>G'=G \backslash \{C\}</math> and <math>S'=S \cup \{C\}</math>; in other words, a constraint can be moved from the goal to the constraint store

Line 39 ⟶ 44:

Actual intepreters process the goal elements in a [[LIFO]] order: elements are added in the front and processed from the front. They also choose the clause of the second rule according to the order in which they are written, and rewrite the constraint store when it is modified.

The third possible kind of transition is a replacemenet of the constraint store with an equivalent one. This replacement is limited to those done by specific methods, such as [[constraint propagation]]. The semantics of constraint logic programming is parametric not only to the kind of constraints used but also to the method for rewriting the constraint store. The specific methods used in practice replace the constraint store with a simpler ones. This simplification may prove the unsatisfiability of the constraint store. However, this this may not happen even if the constraint store is unsatisfiable.

A slightly different semantics for constraint logic programming exist, in which the equality of two literals is considered a constraint, and <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math> is added to the constraint store in the second of the rules above.

A slightly different semantics for constraint logic programming exist, in which the equality of two literals is considered a constraint,. andSuch a constraint <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math> is addeddefined equivalent to the constraintpairwise storeequality inof theterms second<math>t_1=t_1',\ldots,t_n=t_n'</math>. When a literal of the rulesgoal is replaced with the body of a rewritten clause (second rule above), such an equality is added to the constraint store rather than in the goal.

==Terms and constraints==