[ Home
| Overview
| Download
| Language Documentation
| Bug Tracking
| Implementation Documentation
| Links ]
Teyjus - An Implementation of Lambda Prolog
Contents
The Teyjus system is intended to be an efficient and
(eventually)
robust implementation of the language Lambda Prolog that
was designed by Dale Miller and Gopalan Nadathur. Lambda Prolog is a
logic programming language that is based on the intuitionistic theory
of
higher-order hereditary Harrop formulas. This class of formulas
enriches that of Horn clauses---the logical basis of Prolog---with the
possibilities of quantifying over function and (certain occurrences
of) predicate variables, of explicitly representing binding in terms
and of using a fuller complement of connectives and quantifiers. By
systematically exploiting the new features in the underlying logic,
Lambda Prolog provides support at the programming level for
capabilities such as higher-order programming, polymorphic typing,
scoping over names and procedures, modular programming, abstract data
types and the use of lambda terms as data structures.
Much research has been conducted in recent years towards fully
understanding the usefulness of the additions to logic programming
embodied in Lambda Prolog. Two aspects that have received special
attention are the availability of lambda terms for representing
objects and of a suitable set of primitives for manipulating such
representations. These features enable Lambda Prolog to support the
notion of higher-order abstract syntax, a profitable way to
view the syntax of objects whose structures involve binding. Several
detailed studies have, in fact, indicated the utility of this language
in building symbolic systems that manipulate objects such as formulas,
programs, proofs and types. Motivated by such applications, Nadathur
and colleagues have invested extensive effort in understanding the
special implementation challenges posed by the new features of the
language and in devising methods for meeting these well. An outcome of
this research 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.
Teyjus is a word in Sanskrit that,
amongst other things,
means sharpness, edge, brilliance, splendour, vitality, strength, and
majesty. Many of these are properties that the system aspires to in
the long haul. As with all words from a different language, and
especially one with a rich variety of sounds not present in English,
there is a question of what the `right' transliteration for
the name is. One found commonly in Sanskrit to English dictionaries is
tég-as. However, we found it difficult to steer others
to
the right pronounciation using this way of writing the name and, of
course, we would like everyone to pronounce the name correctly! The
way we have chosen to write the name might make the task easier. Here
is some help: try saying `Tey' like you would `Day' except for
replacing the first letter with `D', and `jus' like you would `just'
but for leaving out the last letter. This should get you close;
unfortunately, there is no sound in English exactly like the one the
first `T' is intended to produce.
If you are genuinely interested in getting
the pronounciation right,
you may click here to hear it spoken.
An integral part of the implementation scheme
is an abstract 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 the following additional
features satisfactorily:
The 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 notation has then been deployed systematically
in the low-level steps contained in the abstract machine.
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.
An implementation of Lambda Prolog on stock
hardware based on the
the present ideas envisages four software subsystems: a
compiler, a loader, an emulator for the abstract machine and a user
interface. The function of the compiler is to process any given module
of Lambda Prolog code, to certify its internal consistency and to
ensure that it satisfies a promise determined by an associated
signature and, finally, to translate it into a byte code form
consisting of a `header' part relevant to realizing module interactions
and
a `body' containing sequences of instructions that can be
run on the abstract machine. The purpose of the loader is to read in
byte
code files for modules that need to be used, to
resolve names and absolute addresses using the information in the
header parts of these files and to eventually produce 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 capability of executing such code after it has been
linked. Finally, the user interface allows for a flexibility in the
compilation, loading and use of modules in an interactive session.
The Teyjus system embodies all the above
components and comprises
about 50,000 lines of C code. The functionality outlined above is
realized in its entirety in a development environment. Also supported
is the use of the compiler on the one hand and the loader and emulator
on the other in standalone mode. The system architecture actually
makes byte code files fully portable. Thus, Lambda Prolog modules can
be distributed in byte code form, to be executed later using only the
loader/emulator. Finally, the system includes a disassembler for the
purpose of viewing the results of compilation.
The main strength of Lambda Prolog is in the
capabilities it offers
for representing and manipulating objects whose structures incorporate
binding. Particular examples of such objects are formulas, proofs and
programs. Several systems have been built in the past for reasoning
about such objects. Nuprl,
Coq and Isabelle are
some recent systems that exploit ideas similar to those in Lambda
Prolog for representing formulas and proofs. These systems fall under
the rubric of logical frameworks, in that they provide
mechanisms for specifying a variety of logics and for constructing
proof development systems relative to these. More details about such
systems can be found in the page on logical frameworks
maintained by Frank Pfenning. In contrast to such systems, Lambda
Prolog is a programming language, albeit with special
capabilities. It is, in this sense, more closely related to the
language Elf that
is
based on a theory of dependent types.
Lambda Prolog has received several implementations in
the past. All but one of these implementations have been in the form
of interpreters, the most recent one being the Terzo
interpreter written in Standard ML. The only other implementation
to adopt a compilation approach is Prolog/MALI. There are,
however, significant differences between Teyjus and Prolog/MALI. The
core of the latter implementation is a memory management system called
MALI
that offers functionalities relevant to realizing logic programming
languages. To a first approximation, Lambda Prolog programs are
compiled to C programs that execute MALI commands for creating and
interpreting goal structure. Certain inefficiencies, such as the
copying of entire goal structures, appear to be inherent to this
approach as opposed to the abstract machine based approach used in
Teyjus. There are also differences in the treatment of
specific aspects such as the representation and runtime manipulation
of types, the representation of terms, the realization of
reduction, and the implementation of the scoping
primitives. Finally, Prolog/MALI appears to support a different notion
of
modularity.
The Teyjus system is the result of many years of
research and
development and has benefitted from the involvement of several people
over time. The overall project has been directed by Gopalan Nadathur.
The abstract machine, loader and compilation methods that underlie
this implementation of Lambda Prolog have been designed by Gopalan
Nadathur. Bharat Jayaraman and Keehang Kwon contributed valuable
ideas to the structure of an earlier version of the abstract machine.
The implementation of these three components, and of the concomitant
higher-order unification procedure, in the present system is due to
Gopalan Nadathur. A preliminary version of the loader was implemented
by Guanshan Tong. Dustin Mitchell has modified the low-level
representation of Lambda Prolog types and terms towards realizing
portability and is also responsible for the implementation of the
changed scheme. The disassembler, the front-end for the system and the
implementation of many builtins, especially those dealing with I/O,
are due to him. Finally, he has also undertaken the rationalization
and (re)organization of innumerable components of the project and its
documentation. Shyan-Ming Perng provided initial implementations of
many of the arithmetic and logical builtins and also of routines for
reading and writing terms. Emil Ong is undertaking the porting of the
system to Windows based platforms. Lyn Headley contributed to the
implementation of the builtins.
An indispensable component of the release of a
system of significant
size such as Teyjus is its testing. Dale Miller has patiently used the
system from its first, rough and ready, days, has helped pin-point
several bugs and has also volunteered several suggestions towards
improving its functionality. Others who have provided valuable feedback
of this kind are Amy Felty, Chuck Liang, Frank Pfenning and Jeremie
Wajs.
[ Home
| Overview
| Download
| Language Documentation
| Bug Tracking
| Implementation Documentation
| Links ]
Last updated by gopalan@cs.umn.edu on August 12, 2003