| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
It is beyond the (present) scope of this manual to provide a comprehensive introduction to Lambda Prolog or to its underlying theory. If you are interested learning more about these aspects, one place to look may be the paper
The distribution material also contains several examples of Lambda Prolog code with pointers to papers describing conceptual aspects of the code as relevant. It would be quite useful to try to understand some of these examples in depth before you begin writing your own programs. There is some divergence in the language treated between different implementations of Lambda Prolog, so you may want also to pay attention to the particular rendition of these examples into code for the Teyjus system. If you are already familiar with Lambda Prolog but want to understand the structure of programs in Teyjus, see Program Structure and Syntax in Teyjus.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Gopalan Nadathur on October, 20 2007 using texi2html 1.76.