Robert J. Simmons: HomeResearch

Substructural logic programming

This page collects work done by me and others on substructural logic programming. It focuses on forward-chaining substructural logic programming in which logic programming rules act roughly like rewriting rules - there are lot of interesting potential connections between forward-chaining substructural logic programming and rewriting logic semantics. This is distinct from backward-chaining or goal-oriented logic programming in substructural logics.

A closely related project is the Security Protocol Specification Language MSR; Cervesato and Scedrov's 2009 journal paper "Relating State-Based and Process-Based Concurrency through Linear Logic," mentioned in the list of papers below, describes the connection. Reasoning about substructural logic programs is one of the goals of the Meta-CLF project (and one of the goals of my thesis!). Because the Meta-CLF project page reviews work on this topic, I am only reviewing papers that discuss the specification or implementation of substructural logic programming languages.

Papers


Papers are listed in roughly chronological order.

Presentation


This is the presentation of Linear Logical Algorithms from ICALP. I let myself fall slightly out of practice and was a bit under the weather when I recorded this; consider it an experiment, given that the presentation doesn't quite make sense without narration attached to the slides.

Oops! There seems to be a problem with viewing these slides...

Lollimon


Lollimon is an experimental programming language that supports forward and backward chaining linear logical programming. It was originally described in the paper Monadic concurrent linear logic programming. The Linear Logical Algorithms paper describes a fragment of the Lollimon language, and so every LLA can be run in Lollimon. Note that Lollimon most definitely does not support the run-time guarantees described in the Linear Logical Algorithms paper.

The following commands will allow you to check out and build Lollimon. These instructions assume you have Ocaml installed on your system.

shell> cvs -d :pserver:guest_lf@cvs.concert.cs.cmu.edu:/cvsroot login
(press Enter if prompted for a password - no password is necessary)
shell> cvs -d :pserver:guest_lf@cvs.concert.cs.cmu.edu:/cvsroot checkout lollimon
shell> cd lollimon
shell> make

If everything goes correctly, you can then run the examples as follows. Starting Lollimon will cause you to enter Lollimon's top-level environment.

shell> ./lollimon
LolliMon>#load "examples/linlogalg/spantree.lo"
[Loading file /Users/rjsimmon/Repos/lollimon/examples/linlogalg/spantree.lo]
Looking for 4 solutions to query: edge a b => edge a c => edge a d => edge b c => edge b e => edge d e => vertex a -o vertex b -o vertex c -o vertex d -o vertex e -o {! (tree X Y)}
Attempt 1, Solution 1 with [X := d; Y := e]
Attempt 1, Solution 2 with [X := a; Y := b]
Attempt 1, Solution 3 with [X := a; Y := c]
Attempt 1, Solution 4 with [X := a; Y := d]
Success.
spantree.lo is Ok.
[Closing file /Users/rjsimmon/Repos/lollimon/examples/linlogalg/spantree.lo]
LolliMon>#quit
shell>

In this case, the four lines "Attempt 1, solution N" tell us that Lollimon's execution of the linear logical algorithm for spanning trees on the five-element undirected graph from the ICALP talk computed the spanning tree (a,b), (a,c), (a,d), (d,e).

In this manner, you can run all of the examples from the presentation and the ICALP paper, and most from the technical report. See the "README" file in the "lollimon/examples/linlogalg" directory.