Algebraic and logical semantics for CLP languages with dynamic scheduling

AbstractThe first logic programming languages, such as Prolog, used a fixed left-to-right atom scheduling rule. Unfortunately, this meant that programs written in a clean, declarative style were often very inefficient, only terminated when certain inputs were fully instantiated or “ground,” and (if negation was used) produced wrong results. For this reason, nearly all recent logic programming languages provide more flexible scheduling in which computation generally proceeds left-to-right but in which some calls are dynamically “delayed” until their arguments are sufficiently instantiated to allow the call to run efficiently. Despite the increasing practical importance of logic programming languages with dynamic scheduling, relatively little attention has been paid to their semantics. We lift the standard algebraic and logical soundness and completeness results for success and finite failure for constraint logic programs to constraint logic programming languages with dynamic scheduling. The proofs are quite simple and essentially rely on treating the delayed calls as part of the answer constraint