Constraint logic programming: Difference between revisions

Revision as of 00:00, 17 March 2006

Revision as of 00:09, 17 March 2006

Line 19:

==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; it can also contain constraints and equalities of terms; the ''constraint store'' contains all constraints the interpreter has assumed satisfiable so far.

Initially, the current goal is the goal and the constraint store is empty. The interpreter proceed by removing the first element from the current goal and analyzing it. ThisThe details of this analysis mayare endexplain upbelow, but in athe end it may produce [[Recursion|recursive call]] or a failure; the interpreter backtracks in the second case. It may also generate an addition of new literals to the current goal and an addition of new constraint to the constraint store. The interpreter stops when the current goal is empty and the constraint store is satisfiable.

EachThe stepdetails of the algorithmanalysis of a literal removed from the goal is as follows. TheAfter firsthaving removed this literal from the front of the goal, it is consideredchecked andwhether removedit fromis thea currentconstraint goalor a literal. If it is a constraint, it is added to the constraint store. If it is a literal, a clause whose head has the same predicate of the literal is chosen; the clause is rewritten by replacing its variables with new variables (what is important is that these new variables do not already occur in the goal); the body of the clause is then placed in front of the goal; the equality of each argument of the literal with the corresponding one of the rewritten clause head is placed in front of the goal as well.

Initially, the current goal is the goal and the constraint store is empty. The interpreter proceed by removing the first element from the current goal and analyzing it. This analysis may end up in a [[Recursion|recursive call]] or a failure; the interpreter backtracks in the second case. It may also generate an addition of new literals to the current goal and an addition of new constraint to the constraint store. The interpreter stops when the current goal is empty and the constraint store is satisfiable.

Each step of the algorithm is as follows. The first literal of the goal is considered and removed from the current goal. If it is a constraint, it is added to the constraint store. If it is a literal, a clause whose head has the same predicate of the literal is chosen; the clause is rewritten by replacing its variables with new variables (what is important is that these new variables do not already occur in the goal); the body of the clause is then placed in front of the goal; the equality of each argument of the literal with the corresponding one of the rewritten clause head is placed in front of the goal as well.

Some checks are done during these operations. In particular, the constraint store is checked for consistency every time a new constraint is added to it. In principle, whenever the constraint store is unsatisfiable the algorithm could backtrack. However, checking unsatisfiability at each step would be inefficient. For this reason, an incomplete satisfiability checker may be used instead.