[POPLmark] A "locally nameless" solution in Coq
Xavier Leroy
Xavier.Leroy at inria.fr
Mon Oct 10 12:47:36 EDT 2005
Dear all,
The interesting discussions at ICFP and Merlin two weeks ago finally
motivated me to clean up and put online my (partial) solution to the
POPLmark challenge:
http://cristal.inria.fr/~xleroy/POPLmark/locally-nameless/
This solution covers only part 1a of the challenge (algorithmic
subtyping, no record types). It is written in Coq, and uses a
"locally nameless" representation for binders: variables bound within
terms are represented by de Bruijn indices, but variables free in
terms are represented by names. I was inspired by Randy Pollack's
talk, "Reasoning About Languages with Binding":
http://homepages.inf.ed.ac.uk/rap/export/bindingChallenge_slides.pdf
Some good things about this representation:
- Alpha-equivalence is term equality, which makes life much simpler in Coq.
- The statements (and even the proofs) of the main theorems are quite
close to what one would write on paper.
- Despite not being completely nominal, it still illustrates some of
the key aspects of fully nominal approaches, especially the
"forall/exists" equivalence for the choice of fresh variables.
Some bad things about this representation:
- There is a lot of boilerplate involved before getting to the meat
of the proof: two substitution functions (of names and of de Bruijn
variables), computation and properties of free names, swaps,
commutation of swaps with many definitions, the "forall/exists"
theorems, etc. Consequently, the development is larger than a pure
de Bruijn solution.
- Extending this approach to part 2 of the challenge exceeds my fortitude:
two sorts of names, six substitution functions, even more swaps,
commutation theorems all over the place, ... Enough is enough :-)
One good thing about my solution:
- It is heavily commented, then typeset using the coqdoc tool.
Message to my fellow solution submitters: you, too, can write
good English; don't be shy.
One bad thing about my solution:
- My Coq proof scripts do not have the conciseness and elegance
of Jérôme Vouillon's. Sorry, I've been using Coq for only 6 years...
Final thoughts:
- If the purpose is just to solve the challenge and be done with it,
I would rather go for pure de Bruijn.
- However, this could change if some of the nominal boilerplate was
built into the logic or at least into the prover.
- The exercise has some educational value, to me at least.
Enjoy,
- Xavier Leroy
More information about the Poplmark
mailing list