A proposal for modules in λprolog

Abstract

Higher-order hereditary Harrop formulas, the underlying logical foundation of λ Prolog [NM88], are more expressive than first-order Horn clauses, the logical foundation of Prolog. In particular, various forms of scoping and abstraction are supported by the logic of higher- order hereditary Harrop formulas while they are not supported by first- order Horn clauses. Various papers have argued that the scoping and abstraction available in this richer logic can be used to provide for modular programming [Mil89b], abstract data types [Mil89a], and state encapsulation [HM90]. None of these papers, however, have dealt with the problems of programming-in-the-large, that is, the essentially linguistic problems of putting together various different textual sources of code found, say, in different files on a persistent store into one logic program. In this paper, I propose a module system for λ Prolog and shall focus mostly on its static semantics.