richardmoot / linearone Goto Github PK

Add many more examples from the papers of Morrill e.a. and Kubota & Levine as additional test cases.

Implement cut elimination

The variable renaming can produce inconsistent results in complex cases. This needs to be corrected.

Add translation of first-order linear logic proof (natural deduction and/or sequent calculus) into Displacement calculus proofs.

Forall links have the property that no atom containing the eigenvariable of a link can every be identified with a node which dominates the forall link of this variable. Adding this constraint would reduce the search space and make testing the forall contraction less complicated.

Allow specification of constraints of the form X=<Y. These constraints will help with the treatment the reflexives of the Displacement calculus, but they are a simple and powerful mechanism in general.

The constraint-like implementation will essentially be the following
X =< X <=> true
X =< Y, integer(X), integer(Y) <=> Prolog's X =< Y for integers (evaluates to true or false)
X =< Y, Y =<X <=> X = Y
X =< Y, Y =< Z => X =< Z (only rule which adds constraint)

Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to produce eta-normal proofs as well.

Add an (optional) proof transformation step which transforms long normal form proofs into beta-eta-normal proofs.

Implement smarter axiom link strategy, selecting the axiom which has the least possible partner (similar to the Grail 3 strategy and to Knuth's general Dancing Links algorithm).

The beta version allows a predicate to have only variable or constant terms. Some of the more subtle applications of first-order linear logic require complex terms. For example, the treatment of associativity and scope restrictions in my 2014 Lambek paper uses "integer-like" terms (of the forms s(X), s(s(X), etc.)

One of the most basic applications of first-order linear logic is its application for linguistic features such as Case, Gender, Number etc. Though this is easily implemented in first-order linear logic itself, it would be useful to add the possibility of incorporating features into the translation functions for the Displacement calculus and hybrid type-logical grammars

Add additives together with a contraction condition as proposed by Maieli.

This will be a major update/rewrite since it will complicate (at least) the axiom linking component: it will allow an atom to not be linked at all (if a plus link "erases" it) or to be linked multiple times (if it has a contraction link as a parent).