Constraint logic programming: Difference between revisions

Revision as of 23:37, 16 March 2006

Revision as of 23:47, 16 March 2006

Line 32:

unsatisfiable constraint store.

The interpreter stopshas proved the goal 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 in three possible cases:

Line 46:

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.

The result of evaluating a goal against a constraint logic program is defined if the goal is proved. In this case, there exists a derivation from the initial pair to a pair where the goal is empty. The constraint store of this second pair is considered the result of the evaluation. This is because the constraint store contains all constraints assumed satisfiable to prove the goal. In other words, the goal is proved for all variable evaluations that satisfy these constraints.

A slightly different semantics for constraint logic programming exist, in which the equality of two literals is considered a constraint. Such a constraint <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math> is defined equivalent to the pairwise equality of terms <math>t_1=t_1',\ldots,t_n=t_n'</math>. When a literal of the goal 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.