Lolli: A Linear Logic Programming Language

Based on the web page by Josh Hodas, written 26 July 1995. Recent updates by Dale Miller.

Table of Contents


Introduction

Lolli is a logic programming language based on a fragment of linear logic. As such it allows the programmer to exercise a significant degree of control over the pattern of use of certain program clauses (or resources) during proof search. The language was designed by Josh Hodas and Dale Miller and is described in the papers listed below.

See also: Overview of linear logic programming, by Dale Miller. Accepted as a chapter in the book Linear Logic in Computer Science, edited by Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Phil Scott. Cambridge University Press. (PostScript, DVI, PDF). An older survey article is also available.

Hodas has implemented a version of Lolli for version 0.93 of Standard ML of New Jersey and released it in 1992. Version 0.701 of Lolli is available with the source code for the interpreter and examples of Lolli sources.

It seems that the most active implementation effort on Lolli now is being done on the language and compiler called LLP at Kobe University.


Motivations for the Development of Lolli

One way to understand Lolli is as a refinement of the logic of the language lambdaProlog. The language lambdaProlog extends the logic of horn clauses by allowing the use of implication not just in clauses, but also in goals. (This is just one of several significant ways that lambdaProlog extends Prolog. It also offers higher-order unification, arbitrarily scoped quantifiers, and types, to name just a few of its features.) The meaning of the goal D =) G is based on the bottom-up reading of the standard rule for proving an implication formula in intuitionistic logic:

Gamma ---) D=)G IFF Gamma, D ---) G

That is, the system should first load the clause D into the current program, and then try to prove the goal G using the augmented program.

There are two important differences between implication goals in lambdaProlog and the use of assert in Prolog. First, whereas any logic variables contained in a clause added using assert are automatically closed with a universal quantifier, the variables in a clause added using an implication are not. So, the interpreter must be prepared to deal with live logic variables in the program. Second, regardless of whether the goal G suceeds or fails, the assumed clause is discharged as soon as the proof attempt is finished. Thus the assumption is scoped only over the subordinate goal.

While the use of intuitionistic implications to augment the goal language has been used to great success, two papers published in 1991 showed the limitations of this approach:


Related Systems


An Annotated Bibliography

Validate