Constraint logic programming: Difference between revisions

Revision as of 15:14, 10 February 2010

Revision as of 15:16, 10 February 2010

Line 53:

===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 function symbols 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 interpreter. Equality constraints on terms can be simplified, that is solved, via [[unification]]:

A constraint <code>t1=t2</code> can be simplified if both terms are functorsfunction symbols applied to other terms. If the two functorsfunction symbols 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 functorsfunction symbols or the same functor but on different number of terms, the constraint is unsatisfiable.

If one of the two terms is a variable, the only allowed value the variable can take is the other term. As a result, the other term can replace the variable in the current goal and constraint store, thus practically removing the variable from consideration. In the particular case of equality of a variable with itself, the constraint can be removed as always satisfied.