(K. Kwon) A Structured Presentation of a Closure-Based Compilation Method for a Scoping Notion in Logic Programming

Abstract: We present a systematic reconstruction of a compilation method for an extension to logic programming that permits procedure definitions to be given a scope. At a logical level, this possibility is realized by permitting implications to be embedded in goals. Program clauses that appear in the antecedents of such implications may contain variables that are bound by external quantifiers, leading to non-local variables in procedure declarations. In compiling programs in this extended language, there is, therefore, a need to consider the addition to given programs of program clauses that are parameterized by bindings for some of their variables. A proposed approach to dealing with this aspect uses a closure representation for clauses. This representation separates an instance of a clause with parameterized bindings into a skeleton part that is fixed at compile-time and an environment that maintains the part that is dynamically determined. A development of this implementation scheme is provided here by starting with an abstract interpreter for the language and then refining this to arrive at an interpreter that uses the closure representation for clauses. The abstract state machine formalism of Gurevich is used in specifying the interpreters that are of interest at the two different stages. We also justify this refinement by showing that the essential notion of a computation is preserved by the refinement and thus the refinement is a correct one.

Keywords: closure, compilation, embedded implication, logic programming, scoping