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 contributions 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.
- Monadic concurrent linear logic programming,
Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins, PPDP 2005.
This was an initial ambitious attempt to make a logic programming language combining both forward-chaining and backward-chaining based on Watkins et al.'s logical framework CLF. It introduced the Lollimon implementation; instructions for downloading and running Lollimon can be found at the bottom of this page. (Again, I didn't have anything to do with Lollimon, but there didn't seem to be instructions anywhere else on the web for how to download and run it!) The paper is available from the ACM Digital Library and Frank Pfenning's web page.
- Linear Logical Algorithms,
Robert J. Simmons and Frank Pfenning, ICALP 2008.
This paper defines a relatively restricted . Frank wrote up a short note, titled On Linear Inference, that discusses the philosophical basis for the style of forward-chaining we use in this paper.
The extended abstract published in ICALP 2008 is owned by Springer; the content in that extended abstract is also covered in the CMU tech report, which has the official CMU tech report number CMU-CS-08-104 but didn't ever quite make it into the official CMU tech report archive, I believe.
-
Celf – A Logical Framework for Deductive and Concurrent Systems (System Description),
Anders Schack-Nielsen and Carsten Schürmann,
IJCAR 2008.
Describes Celf.
-
Relating State-Based and Process-Based Concurrency through Linear Logic,
Iliano Cervesato and Andre Scedrov,
IC 2009.
Connects forward-chaining substructural logic programming to the formalisim of multiset rewriting, and describes an extended multiset rewriting language, ω, based on this analogy.
-
Substructural operational semantics as ordered logic programming,
Frank Pfenning and Robert J. Simmons,
LICS 2009.
Introduces Ollibot.
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.
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.