Comparative Semantics for Flow Control in Logic Programming without Logic

摘要

The paper studies semantic issues concerning control flow notions in logic programming languages by exploring a two-stage approach. The first stage considers solely uninterpreted (or schematic) elementary actions, rather than operations such as unification, substitution generation or refutation. Accordingly, logic is absent at this first stage. It provides a comparative survey of the semantics of a variety of control flow notions in (uninterpreted) logic programming languages including notions such as don't know versus don't care nondeterminism, the cut operator, and/or parallel logic programming, and the commit operator. In all cases considered, it develops operational and denotational models, and proves their equivalence. A central tool both in the definitions and in the equivalence proofs is Banach's theorem on (the uniqueness of) fixed points of contracting functions on complete metric spaces. The second stage of the approach proceeds by interpreting the elementary actions, first as arbitrary state transformations, and next by suitably instantiating the sets of states and of state transformations (and by articulating the way in which a logic program determines a set of recursive procedure declarations). The paper concentrates on the first stage. For the second stage, only a few hints are included. Furthermore, references to papers which supply details for the languages Prolog, Concurrent Prolog and Guarded Horn Clauses are provided.