README.txt

Overview

I read the following papers for background:

- "Working with Linear Logic in Coq" (WLLC)
- chapters 1 and 3 of Pfenning's linear logic notes (PLL)
- "Toward Language-Based Verification of Robot Behaviors" (LBV)
- "Structural Analysis of Narratives with the Coq Proof Assistant" (SAN)
- Wadler's linear logic notes

Each file contains detailed comments on the contents, as well as TODOs. Here's a high-level summary of what I did.

- Learned linear logic
- Picked a version of linear logic to use (intuitionistic; sequent calculus with the cut rule)
- Encoded its connectives, rules, and notations
- This required combining environment techniques from SAN with the rules from PLL and the scenario from WLLC
- Represented the environment as a multiset of linear logic props; learned how to do setoid rewrites
- Formalized the blocks world example: objects, axioms, and proved* the main lemma, SwapAB
- Formalized a new example, that of the box-pushing game Sokoban, and proved* a small Sokoban game

* There are many admitted lemmas throughout the files. They relate almost entirely to manipulating the environment.
  Dealing with interactions between union, singleton, and the connective (**) required a lot of work, and it got tedious.
  The structure of the proofs should be evident though, since I used the linear logic rules, only admitting the env lemmas.

Difficulties

- The environment, setoid rewrites, and dealing with the (**) connective.
  - I think it would make life a lot easier to use a dedicated linear logic proof assistant instead of my shallow embedding of ILL.
    For example, Coq has the context, which is basically the environment e in a sequent (in "e |- g").
    That takes away all the work of dealing with commutativity, associativity, etc. of things in the environment.
- Inversion on linear logic proofs, or doing induction on them, didn't really work. 
  I found it unusually hard to prove things like the following:
  {{ A ** B }} |- g 
  ->
  A :: B :: emptyBag |- g
- Short proofs were long and tedious; could use a lot more automation (to discharge env subgoals) and proof search (to apply ILL rules).

Future directions

- Dedicated ILL proof assistants (Twelf?).
- Invariants of ILL proofs, corresponding to story or game invariants. Some examples:
  There exists a proof such that block C never moves. Or, for all proofs, resource X is always consumed.
  Or, for all proofs of a well-formed Sokoban level (that is, all traces of playing that level), 
  the player never goes out of bounds of the walls.