Survey about LambdaProlog

Gopalan Nadathur
Email: gopalan@cs.duke.edu

Appeared in Volume 7/2, May 1994

Keywords: functions.

I conducted a survey on lambdaProlog usage a while ago and this is a summary of the results.

For those of you who would like to look at the detailed responses to the survey, these are available by anonymous ftp from Duke. To get the file containing them, you have to ftp to cs.duke.edu, and get the file called responses from the directory pub/gopalan/lpsurvey. The file is in the form of an emacs mail file.

As a follow-up to several responses, I had asked for and received references to relevant publications. These references are also available by ftp in the same directory as the file references. The references in the summary below are to entries in this file.

The survey requested information concerning the kind of use being made of the lambdaProlog language, the particular implementations that had been used and other aspects that were thought to be relevant. Seventeen responses were received and the important aspects of these response are summarized below.

(1) Implementation Used/Being Used

Several people (9) had used lp2.6/lp2.7 in the past but most have either partially or completely moved to using eLP or Prolog/Mali. Nine of the respondents were using eLP (or the related SML version) and eight were using Prolog/Mali. Several of those who had used eLP and had switched to Prolog/Mali indicated that the reason for doing so was that the latter system was significantly faster.

(2) Use in Teaching

At least five individuals indicated a significant use of lambdaProlog in instruction.

(a) lambdaProlog is progressively taking the place of Prolog in the LP courses of Yves Bekkers and Olivier Ridoux from INRIA Rennes, both as a typed version of Prolog and for itself. These courses are offered to fourth and fifth year students at the Univ. of Rennes and to fifth year students at INSA at Rennes and the Ecole de Mines in Sophia Antipolis. It is also used in Ph.D. courses.

(b) The language and its integration of polymorphic typing, modules and higher-order unification has been the topic of discussion in two graduate seminars offered by Bharat Jayaraman at SUNY, Buffalo. It has also been useful in exposing the power and usefulness of higher-order unification.

(c) Gary Leavens has used it in an advanced graduate course in the semantics of programming languages at the Univ. of Iowa and found it a useful vehicle for discussing LP, type checking and operational semantics.

(d) Dale Miller is using it as the principal language in a Logic and Computation course for third year (undergraduate) students in the cognitive science program at the Univ. of Pennsylvania. He has developed a draft monograph on lambdaProlog for this course which will hopefully be available for wider, but informal, circulation in Summer 1994.

(3) Uses in Research/System Building

Not surprisingly, most of the reported uses of lambdaProlog were in the role of a metalanguage. Subcategorization is difficult without too many 'editorial' decisions and so is not attempted. The uses reported by individuals is summarized below.

(a) Yves Bekkers, Pascal Brisset and Olivier Ridoux (IRISA, France) have used it in studies in automated deduction and in constraint LP. They also plan to use it in a multi- paradigm framework as an implementation language for other languages. A particular point of note is that the Prolog/Mali compiler is developed in lambdaProlog itself.

(b) Catherine Belleannee (IRISA, France) reported uses of lambdaProlog in understanding sequent calculi and in implementing formula manipulation tasks.

(c) Amy Felty (Bell Labs, Murray Hills) has used lambdaProlog in many significant projects related to the specification of logics [Fel89, FM88, Fel93a, FM89], the implementation of theorem provers, proof transformation systems and equality reasoners based on higher-order rewriting [Fel89, Fel91a, Fel92a, Fel92b], the design of data structures for partial natural deduction proofs to support interactive theorem proving [TBK92], the implementation of interpreters for extended LP languages [Fel93b] and the development of translators from object-level syntax to higher-order syntax [Fel93c, Fel93d].

(d) Ian Green (U. Edinburgh) has experimented with higher-order unification with application to inductive theorem proving and program optimization.

(e) John Hannan (Penn State) has used lambdaProlog as a means for implementing a variety of programming tasks related to functional programs [Han90]. These tasks have exploited lambda terms as data structures for representing such programs, the notion of higher-order abstract syntax and the abilities for introducing and discharging hypotheses and eigenvariables.

(f) Masateru Harao (Japan) has used it in constructing a small module system for knowledge representation as part of an undergraduate project.

(g) James Harland (U. Melbourne, Australia) has used it to examine ideas pertaining to language design.

(h) Jan Heering (CWI, Amsterdam) has used it to perform operational experiments with higher-order algebraic specifications [Hee92a, Hee92b]. One particular use mentioned was as a 'calculator' for polymorphic higher-order matching problems.

(i) Gary Leavens (Iowa State) has used it in prototyping language designs and, in particular, to test out type inference rules.

(j) Chuck Liang (U Penn) has implemented some aspects of the Boyer-Moore theorem prover and theorem proving methods such as Knuth-Bendix completion in lambdaProlog.

(k) Dale Miller (UPenn) has written several reasonably complex programs in lambdaProlog. Several of these programs have been developed to test out research ideas related to type checkers, evaluators, compilers, theorem provers and unification procedures. Research students working with him typically use lambdaProlog as their main programming language. Several relevant references are listed.

(l) Fernando Pereira (Bell Labs, Murray Hills) has used it in testing out semantic theories of natural language features such as quantification and anaphora [Per91]. He has also used it as a HOU calculator in testing out analyses of ellipsis [DSP91].

(m) Frank Pfenning (CMU) reported several significant uses. He has used it in understanding type reconstruction for the polymorphic lambda calculus [Pfe88], as the central representation language and metalanguage in a toolkit for constructing programming environments [LPRS88, PE88], developing a theory of higher-order explanation-based generalization [DP89, DP92] and for introducing controlled forward reasoning into LP [DP91]. Tim Freeman has also developed a MellowCard documentation browser in eLP/ESS.

(n) Laurent Thery (Computer Lab, Univ. of Cambridge) has used it to implement theorem provers which has then been used to experiment with ideas of user interface [TBK92].

(4) Language/System Design and Implementation Efforts

(a) The group at IRISA/INRIA continues to work on improving performance (of Prolog/Mali), constructing an interpreter and making the system more flexible. They are also looking at extensions to the language based on linear logic, constraints and extended types.

(b) Amy Felty, Elsa Gunter and Frank Pfenning are developing an interpreter for lambdaProlog in Standard ML. Amy Felty (with collaborators) is interested in the following language issues: providing a principled means for naming dynamically generated constants so that they can be parsed and printed during an interactive session, extended string manipulation capabilities and adding streams for file and other kinds of I/O.

(c) The group at Duke (Kwon, Nadathur and Wilson) and SUNY, Buffalo (Jayaraman) continues their implementation effort. The design of the abstract machine for lambdaProlog is complete. An emulator for this machine is now being built and a compiler that translates lambdaProlog programs into instructions executable on this machine is being developed. This implementation effort has brought language and system issues such as the module system and debuggers into focus. These are to be looked at carefully in the near future.

(5) Gripes

Not too many were mentioned (I believe largely out of politeness). There was one request for better documentation of existing systems and another for improved I/O facilities.

Gopalan Nadathur
Computer Science Dept.
Duke Univ., Box 90129
Durham, NC 27708-0129, USA
Email: gopalan@cs.duke.edu