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.

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]

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

?- 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)