A Dataflow Semantics for Constraint Logic Programs

This paper introduces an alternative operational model for constraint logic programs. First, a transition system is introduced, which is used to define a trace semantics T. Next, an equivalent fixpoint semantics F is defined: a dataflow graph is assigned to a program, and a consequence operator on tuples of sets of constraints is given whose least fixpoint determines one set of constraints for each node of the dataflow graph. To prove that F and T are equivalent, an intermediate semantics O is used, which propagates a given set of constraints through the paths of the dataflow graph. Possible applications of F (and O) are discussed: in particular, its incrementality is used to define a parallel execution model for clp's based on asynchronous processors assigned to the nodes of the program graph. Moreover, O is used to formalize the Intermittent Assertion Method of Burstall [Bur74] for constraint logic programs.