Constraint logic programming: Difference between revisions

Revision as of 15:16, 10 February 2010

Revision as of 15:19, 10 February 2010

Line 63:

===Reals===

Constraint logic programming with [[real number]]s uses real expressions as terms. When no functorsfunction symbols are used, terms are expressions over reals, possibly including variables. In this case, each variable can only take a real number as a value.

To be precise, 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)</code> 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 functorsfunction symbols 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 functorsfunction symbols can be combined, leading to terms that are expressions over reals and functorsfunction symbols applied to other terms. Formally, variables and real constants are expressions, as any arithmetic operator over other expressions. Variables, constants (zero-arity-functorsfunction symbols), and expressions are terms, as any functorfunction symbol 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 functorfunction symbol and number of subterms, their equality constraint can be replaced with the equality of subterms.

===Finite domains===