Constraint logic programming: Difference between revisions

Revision as of 06:37, 20 June 2007

Revision as of 12:46, 23 July 2007

Line 21:

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 and may also contain some constraints it is trying to satisfy; 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 proceeds by removing the first element from the current goal and analyzing it. The details of this analysis are explainexplained below, but in the end this analysis may produce a successful termination or a failure. This analysis may involve [[Recursion|recursive call]]s and addition of new literals to the current goal and new constraint to the constraint store. The interpreter backtracks if a failure is generated. A successful termination is generated when the current goal is empty and the constraint store is satisfiable.

The details of the analysis of a literal removed from the goal is as follows. After having removed this literal from the front of the goal, it is checked whether it is a constraint or 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 (variables not occurring in the goal): the result is called a ''fresh variant'' of the clause; the body of the fresh variant 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 fresh variant head is placed in front of the goal as well.