Implementation techniques for scoping constructs in logic programming

Introducing universal quantifiers and some forms of implications into goals provides for scoping constructs in logic programming. We address the new implementation problems raised by the addition of these logical symbols. The presence of mixed sequences universal and existential quantifiers in goals requires unification to respect this ordering, a problem we solve by using a scheme for tagging constants and variables. A few changes to existing WAM (Warren Abstract Machine) instructions suffice to implement this scheme. Implication in goals cause new program clauses to be introduced, and the implementation must therefore accommodate a dynamically changing set of program clauses. A naive asserting and retracting of program clauses is an unsatisfactory solution to this problem in view of backtracking. Further, when an implication goal is surrounded by existential quantifiers, the introduced program clauses may have to be parameterized by the bindings for these existential variables, thus requiring program clauses to be treated as program closures. We use a hash-table for efficient access to the clauses and a new kind of record, called an implication point record, to manage the interaction between backtracking and dynamic nesting of implication goals. New instructions for the WAM are proposed for compiling quantifiers and implications in goals.