AbstractMachine
An integral part of the scheme that has been used for implementing Teyjus is a virtual machine that is capable of realizing the operations that arise in typical Lambda Prolog programs efficiently. As with other logic programming languages, unification and backtracking are intrinsic to Lambda Prolog and the Warren Abstract Machine (WAM) provides a basic structure for treating these aspects well. However, an extensive embellishment of this framework is needed for realizing several additional features satisfactorily:
-
The language contains primitives that can alter the name space and the definitions of procedures in the course of execution. This means, in particular, that unification has to pay attention to changing signatures and that the solution to each (sub)goal has to be relativized to the relevant program context.
-
In contrast to other languages, lambda terms are used in Lambda Prolog as data structures. A representation must therefore be provided for these terms that permits their structures to be examined and compared in addition to supporting reduction operations efficiently.
-
Higher-order unification is used in an intrinsic way in the language. This operation is conceptually more complex than the unification operation of Prolog and a practical way of supporting it must be found. In doing this, it may sometimes be necessary to delay the solution of unification problems. For this reason, a mechanism must be devised for representing unification problems explicitly.
-
In addition to having a role in determining program correctness, types could be relevant to the dynamic behavior of programs. A scheme must therefore be designed for reducing the runtime impact of types and this must be augmented by a good mechanism for carrying types along into computatations when this cannot be avoided.
-
Programming in the language is done relative to modules. In realizing this feature, it is necessary to support certain operations for composing different modules. Moreover, if modularity is to be genuine, a mechanism must be devised for realizing separate compilation.
Work carried out by Gopalan Nadathur, Bharat Jayaraman and Keehang Kwon culminated in late 1997 in the design of a virtual machine that included devices for treating all these aspects well. The solution to the problem of changing signatures was based on an elegant scheme for tagging constants and variables and using these tags in unification. To realize changing program contexts, a fast method was designed for adding and removing code that is capable also of dealing with backtracking behaviour. The code that needs to be added may sometimes contain global variables and this possibility was dealt with by an adaptation to logic programming of the idea of a closure. To facilitate a sensible representation of lambda terms, an explicit substitution calculus called the suspension calculus was designed and deployed in the low-level steps for manipulating lambda term that are contained in the abstract machine. This abstract machine handled full higher-order unification, an operation that is characterized by its branching behaviour. Techniques were developed for treating such branching and also for compiling unification steps and for prioritizing deterministic parts of the unification computation. In treating types, ideas were introduced for utilizing information available at compile time about their structure to substantially reduce the effort expended at runtime in creating and analyzing types. Finally, towards supporting modular programming, a method was designed for realizing separate compilation with one of the module interaction mechanisms known as module importation. This mechanism also required the addition and removal of blocks of code. Techniques for dealing with changing program contexts in the core language could be used to implement this aspect. However, these methods had to be embellished with new mechanisms for avoiding redundancy in the added code, something that could only be determined at runtime.
Much has been learned from experimenting with the first version of Teyjus and this has led to a substantial redesign of the abstract machine and the modules system. The most significant change was a decision to orient computation around a deterministic and terminating fragment of higher-order unification known as pattern unification. This choice considerably simplifies the internal structure of the virtual machine and its instruction set, and also has the consequence of obviating almost all runtime computations over types. These aspects are explored in the (forthcoming) doctoral thesis of Xiaochu Qi, and the new abstract machine is substantially the outcome of her work. Zach Snow has implemented the compiler module that realizes the type analysis complementing this new machine structure. Studies on the practical consequences of choices in lambda term representation by Chuck Liang, Gopalan Nadathur and Xiaochu Qi unearthed improvements in such representation and these have also been incorporated in the new abstract machine. The last major change relates to the modularity mechanisms. The module interaction facility for which we had earlier developed a separate compilation technique is actually a costly one at the programming level. We have since understood a programming paradigm by which an alternative, efficient interaction mechanism known as module accumulation can provide virtually all the useful capabilities of module importation. We have now also succeeded in adapting the separate compilation method for importation to accumulation; this adaptation is a result of the efforts of Steven Holte and Gopalan Nadathur.