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.
k-qy/linear-logic
An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
Coq