Constraint logic programming: Difference between revisions

Revision as of 11:38, 31 October 2007

Revision as of 13:49, 31 October 2007

Line 37:

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 intepretersinterpreters 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 one that is simpler to solve. If the constraint store is unsatisfiable, this simplification may detect this unsatisfiability sometimes, but not always.

Line 51:

===Tree terms===

Constraint logic programming with tree terms emulates regular logic programming by storing substitutions as constraints in the constraint store. Terms are variables, constants, and functors applied to other terms. The only considered constraints are equalities and disequalities between terms. Equality is particularly important, as constraints link <code>t1=t2</code> are often generated by the intepreterinterpreter.

A constraint <code>t1=t2</code> can be simplified if both terms are functors applied to other terms. If the two functors are the same and the number of subterms is also the same, this constraint can be replaced with the pairwise equality of subterms. If the terms are composed of different functors or the same functor but on different number of terms, the constraint is unsatisfiable.