A Lolli interpreter written in lambda Prolog

In a paper (listed below) Josh Hodas and I presented Prolog interpreters for propositional Lolli and commented that to get interpreters for quantificational versions of Lolli, a lambda Prolog interpreter could easily be written.

I've packaged that interpreter up into the following pieces of code.

The module lollisig.mod provides the basic signature for the Lolli language. Notice that to minimize the coding here, we are using the type o for both the type of lambda Prolog's formulas and Lolli's formulas. Usually, this double use of a type is a bad idea: with our modest ambitions here, it doesn't seem to cause any problems.

The module llinterp.mod is the actual Lolli interpreter rewritten into lambda Prolog syntax. The main interpretation feature it provides is the Input-Output modeel of resouces consumption, used to lazily divide resources when intepreting a tensor (multiplicative conjunction) or in backchaining.

This code can now be used as follows.

Load and use both lollisig.mod and llinterp.mod.
In another module, write a module containing Lolli code, just as you would for lambda Prolog except that us import lollisig.mod (so you can use the extra logical constants in Lolli, and you make the top-level connective of all clauses be the symbol <-. This is how the Lolli interpreter will find the Lolli program. Notice that you will have to write atomic facts in your Lolli program not as just A. but as A <- one.
Now load and use this code. To query a Lolli goal, use the go G query.

For example, consider the module gaps.mod written in this rendition of Lolli. The follow session with lambda Prolog (the SML-LP 0.1 implementation).

> elp
Standard ML of New Jersey, Version 0.93, February 15, 1993
Elp, Version 0.1x, Built: Mon Mar 13 15:03:35 EST 1995
?- load "lollisig", load "llinterp".
[reading file ./lollisig.mod]
 ....
[closed file ./lollisig.mod]
[reading file ./llinterp.mod]
 ....
[closed file ./llinterp.mod]
solved

yes
?- use "llinterp".
?- load "gaps".
[reading file ./gaps.mod]
 ....
[closed file ./gaps.mod]
solved

yes
?- use "gaps".
?- exrel N R, go (rel R nil).

R = whom :: mary :: believes :: that :: bob :: married :: nil,
N = 1.
;

R = whom :: bob :: married :: nil,
N = 2.
;
no more solutions
?-

Notice the way this last query was written: the query (exrel N R) is executed as a regular lambda Prolog query and (rel R nil) is executed as a Lolli query.

This version of the Lolli intepreter supports few non-logical features: only the is, read, write, and nl predicates are supported.

References: Lolli has a homepage. See also the paper

Logic Programming in a Fragment of Intuitionistic Linear Logic by Joshua S. Hodas and Dale Miller. Journal of Information and Computation, 110(2):327-365, 1 May 1994. (Postscript), (Abstract). Prolog code from this paper is available. An earlier version of this paper appeared in LICS'91.

Dale Miller (dale@saul.cis.upenn.edu)