Olli Implementation in λProlog

Olli is a logic programming language based on ordered linear logic (see my dissertation for details of ordered linear logic). Olli is a conservative extension of (pure) Lolli, which is a linear logic programming language in the style of λProlog.

Here are the judgements and derivation rules which comprise a formal description of Olli. This system is motivated, explained, and proved correct in my dissertation.

I have implemented Olli (i.e. the above-mentioned derivation rules) in λProlog.
Here is the signature for the implementation of Olli, and here is the actual implementation code.

The code uses many cuts. Some of the cuts are just to achieve faster execution by getting rid of extraneous choice points which would not be satisfied. However, some of the cuts- the ones in the resid, aseq, and sseq predicates in particular- are necessary for correctness since I do not have an explicit atomic formula constructor.

I have also coded the following example Olli programs:

Translating between named-variable and deBruijn lambda terms

This shows how Olli allows an elegant specification of the translation between named-variable lambda terms and deBruijn lambda terms. The code uses HOAS representation for named-variable lambda terms and thus has no explicit substitution machinery. This code uses the ordered context as a stack.
Here are the sig and mod files.

Breadth-first tree numbering

Olli code to take an arbitrary tree and return a tree labelled with breadth-first traversal numberings. This code uses the ordered context as a queue.
Here are the sig and mod files.

Merge-sort

Olli code implementing a merge-sort. Uses ordered context as a queue.
Here are the sig and mod files.

Natural Language Parser Fragment

Shows how ordered linear logic can elegantly specify filler-gap dependencies in English.
Here are the sig and mod files.

Here is a tarball containing all the code files and instructions for how to use and setup (assuming Teyjus already installed).