Content deleted Content added
m →The constraint store: simplified sentence |
→Overview: an example + separate section for semantics |
||
Line 5:
==Overview==
Formally, constraint logic programs are like regular logic programs, but the body of
B(X,1):-X<0.
B(X,Y):-X=1, Y>0.
A(X,Y):-X>0, B(X,Y).
Like in regular logic programming, evaluating a goal such as <code>A(X,1)</code> requires evaluating the body of the last clause with <code>Y=1</code>. Like in regular logic programming, this in turn requires proving the goal <code>B(X,1)</code>. Contrarily to regular logic programming, the constraint <code>X>0</code> in the body of the last clause is also required to be satisfied by the solution. On the other hand, the value of <code>X</code> is not determined at this point. As a result, whether this constraint will be satisfied cannot yet be determined. Rather than proceeding in the evaluation of <code>B(X,1)</code> and then checking whether the resulting value of <code>X</code> is positive afterwards, the interpreter stores the constraint <code>X>0</code> and then proceed in the evaluation of <code>B(X,1)</code>; this way, the interpreter can check whether the constraint <code>X>0</code> is unsatisfiable during the evaluation of <code>B(X,1)</code> rather than afterwards.
In general, the evaluation of a constraint logic program proceeds like for a regular logic program, but constraint encountered during evaluation are placed in a set called constraint store. As an example, the evaluation of the goal <code>A(X,1)</code> proceeds by evaluating the body of the first clause with <code>Y=1</code>; this evaluation adds <code>X>0</code> to the constraint store and requires the goal <code>B(X,1)</code> to be proved. While trying to prove this goal, the second clause is applicable, but its evaluation adds <code>X<0</code> to the constraint store; this addition makes the constraint store unsatisfiable, and the interpreter backtracks, removing the last addition from the constraint store. The evaluation of the third clause adds <code>X=1</code> and <code>Y>0</code> to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution <code>X=1, Y=1</code>.
==Semantics==
The semantics of constraint logic programs can be defined in terms of a virtual interpreter that maintains a pair <math>\langle G,S \rangle</math> during execution. The first element of this pair is called current goal; the second element is called constraint store. The ''current goal'' contains the literals the interpreter is trying to prove; constraints and equality of terms are considered literals, so they can occur in the goal; the ''constraint store'' contains all constraints the interpreter has assumed satisfiable so far.
| |||