Content deleted Content added
merged first two paragraphs, detailed description of algo |
Terms and constraints |
||
Line 18:
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.
==Terms and constraints==
Different definitions of terms are used, generating different kinds of constraint logic programming: over trees, reals, or finite domains. A kind of constraint that is always present is the equality of terms. Such constraints must be present, as the interpreter adds <code>t1=t2</code> to the goal whenever a literal <code>P(...t1...)</code> is replaced with the body of a clause whose rewritten head is <code>P(...t2...)</code>.
===Tree terms===
In the basic case of constraint logic programming, terms are variables, constants, and functors applied to other terms. In this case, the only considered constraints are equality or disequality between terms. Equality is particularly important, as constraints <code>t1=t2</code> are often generated by the intepreter.
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.
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.
In this form of constraint satisfaction, variable values are terms.
===Reals===
Constraint logic programming with [[real numbers]] uses real expressions as terms. When no functors are used, terms are expressions over reals, possibly including variables. In this case, each variable can only take a real number as a value.
Precisely, terms are expressions over variables and real constants. Equality between terms is a kind of constraint that is always present, as the interpreter generates equality of terms during execution. As an example, if the first literal of the current goal is <code>A(X+1)</math> and the interpreter has chosen a clause that is <code>A(Y-1):-Y=1</code> after rewriting is variables, the constraints added to the current goal are <code>X+1=Y-1</code> and <math>Y=1</math>. The rules of simplification used for functors are obviously not used: <code>X+1=Y-1</code> is not unsatisfiable just because the first expression is built using <code>+</code> and the second using <code>-</code>.
Reals and functors can be combined, leading to terms that are expressions over reals and functors applied to other terms. Formally, variables and real constants are expressions, as any arithmetic operator over other expressions. Variables, constants (zero-arity-functors), and expressions are terms, as any functor applied to terms. In other words, terms are built over expressions, while expressions are built over numbers and variables. In this case, variables ranges over real numbers ''and terms''. In other words, a variable can take a real number as a value, while another takes a term.
Equality of two terms can be simplified using the rules for tree terms if none of the two terms is a real expression. For example, if the two terms have the same functor and number of subterms, their equality constraint can be replaced with the equality of subterms.
==Reference==
| |||