Constraint logic programming: Difference between revisions

Revision as of 10:44, 16 March 2006

Revision as of 11:46, 16 March 2006

Line 27:

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

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:

The constraints of constraints logic programming are typically of three classes: constraints over terms, constraints over reals, and constraints over finite domains, which are usually interpreted as sets of integers.

* 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

* an element of <math>G</math> is a literal <math>L(t_1,\ldots,t_n)</math>, there exists a clause that, rewritten using new variables, is <math>L(t_1',\ldots,t_n') :- B</math>, <math>G'</math> is <math>G</math> with <math>\{L(t_1,\ldots,t_n)\}</math> replaced by <math>t_1=t_1',\ldots,t_n=t_n',B</math>, and <math>S'=S</math>; in other words, a literal can be replaced by the body of a rewritten clause having the same predicate as the head, adding its body and the equalities of terms to the goal

* <math>S</math> and <math>S'</math> are equivalent according to the specific constraint semantics

A sequence of transitions is a derivation. A goal <math>G</math> can be proved if there exists a derivation from <math>\langle G, \emptyset \rangle</math> to <math>\langle \emptyset, S \rangle</math> for some satisfiable constraint store <math>S</math>. This semantics formalizes the possible evolutions of an interpreter that arbitrarily chooses the literal of the goal to process and the clause to replace literals. In other words, a goal is proved under this semantics if there exists a sequence of choices of literals and clauses, among the possibly many ones, that lead to an empty goal and satisfiable store.

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.

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.

==Terms and constraints==