[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2. Overview of Teyjus

The Teyjus system is intended to be an efficient and (eventually) robust implementation of the language Lambda Prolog. The new features present in this language pose significant implementation challenges. Nadathur and colleagues have invested considerable effort towards understanding these challenges and in devising methods for meeting these well. An outcome of their work has been the description of an abstract machine for Lambda Prolog. The Teyjus system is based on these ideas and includes a portable, C-based, emulator for the abstract machine and a compiler for translating Lambda Prolog programs into byte code that can be run using a realization of the abstract machine.

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 the following additional features satisfactorily:

The Lambda Prolog abstract machine that has been developed includes devices for treating all these aspects well. The solution to the problem of changing signatures is based on an elegant scheme for tagging constants and variables and using these tags in unification. To realize changing program contexts, a fast method has been designed for adding and removing code that is capable also of dealing with backtracking. The code that needs to be added may sometimes contain global variables and this possibility has been dealt with by an adaptation to logic programming of the idea of a closure. To facilitate a sensible representation of lambda terms, a new notation has been designed for these terms that utilizes the scheme of de Bruijn for eliminating names and that additionally supports an incremental calculation of reduction substitutions. This work was carried out concurrently with the first complete development of the so-called explicit substitution notations and the Lambda Prolog abstract machine represents, to our knowledge, the only systematic deployment of such a notation in a low-level implementation task. A method has been devised for the purpose of representing suspended unification problems that has several interesting features. For example, based on the observation that new such problems arise out of incremental changes to old ones, the scheme is designed to support sharing while still making it possible to rapidly reinstate a previous unification problem upon backtracking. The treatment of higher-order unification itself includes compilation and prioritizes deterministic computations while delaying the truly non-deterministic parts. This approach makes it possible, for instance, to realize a generalization of first-order unification in a completely deterministic fashion. The technique that is adopted for propagating types at run-time uses information already present during compilation to reduce substantially the effort to be expended dynamically. Using this approach, virtually no new computation is required relative to a monomorphic subset of the language that is similar to Prolog. Finally, towards supporting modular programming, a method has been designed for realizing module interactions that permits separate compilation. The actual addition and removal of modules of code can be achieved by methods developed for handling scoping over program clauses. However, these methods have been embellished by efficient devices for determining if a block of code will be redundant in a given context and also by mechanisms for realizing information hiding.

The Teyjus implementation of Lambda Prolog that is based on these various ideas utilizes four subsystems: a compiler, a loader, an abstract machine emulator and a user interface. The compiler translates each Lambda Prolog module into a `header' containing information necessary for realizing module interactions and a `body' consisting of sequences of instructions that can eventually be run on the abstract machine. Based on the particular use of such a module, the loader reads in its bytecode file, resolves names and absolute addresses using the information in the header and eventually produces a structure consisting of a block of code together with information for linking this code into a program context when needed. The emulator provides the means for executing such code after it has been linked. Finally, the user interface provides flexibility in the use of the compiler, the loader and the abstract machine.

The full functionality of the system outlined above is realized in the development environment that corresponds to the executable `teyjus'. The system also provides for the use of the compiler on the one hand and the loader and emulator on the other as standalone components. These are given by the executables `tjcc' and `tjsim'. Finally, for those who want to view the results of compilation, a disassembler is also provided in the executable `tjdis'.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Gopalan Nadathur on October, 20 2007 using texi2html 1.76.