[POPLmark] A "locally nameless" solution in Coq
Xavier.Leroy at inria.fr
Mon Oct 10 12:47:36 EDT 2005
The interesting discussions at ICFP and Merlin two weeks ago finally
motivated me to clean up and put online my (partial) solution to the
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":
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...
- 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.
- Xavier Leroy
More information about the Poplmark