[POPLmark] Meta-comment

[Kevin Watkins]

On 5/11/05, danwang at cs.princeton.edu <danwang at cs.princeton.edu> wrote:
> Let me make this analogy with call-cc. One certianly does not need to use call-
> cc at all, just CPS convert your entire program!
> 
> Twelf allows for nice proofs, because it offers many advanced features that can
> be used to encode object logics. Of course you don't have to use any of them,
> but that just defeats all the reasons to use Twelf.
> 
> Personally, If I wanted to use first-order encodings I might as well be using,
> Coq, Isabell, or HOL. They are more mature than Twelf and I'd say more
> appropiate for first-order encodings.

My inner snot can't resist pointing out that "mature" is as mature
does.  Let's see a few solutions in the other systems Dan Wang
mentioned, and compare.  There seems to be a lot of talk about other
systems, and few complete solutions.

Perhaps it's not worth mentioning, because it sounds as though Dan has
made his mind up, but I'll point out that even setting aside HOAS, the
LF (and therefore Twelf) method is quite different from Isabelle, say.
 In Twelf one writes, in an explicit notation, the computational
content of the proof itself.  In Isabelle, which of the three Dan
mentions I have the most experience with, one tends to write tactics
that enable the Isabelle system to discover the proof, rather than the
proof itself.  Although I have zero experience with Coq as a proof
development system, it looks to me as though Jerome Vouillon's proof,
at least, is in the latter style--I see tactics that presumably act on
intermediate proof search states, rather than a concrete
representation of the proofs themselves.

Of course, there will be unending disputation over which of these
modes of proof is better, but I don't think it's possible to have a
sensible discussion about it without recognizing this essential
difference, which shows up whether or not one is using HOAS to
represent the terms of the language.  For example, if anyone here has
looked at the correctness proofs of Mini-ML compilers that I referred
to the other day (in the examples/compile directory of the Twelf
distribution), they will recognize that HOAS is being used, at the
meta-level, to manipulate deductions of evaluation steps in the
low-level abstract machines, even though the machines themselves are
based on de Bruijn terms.

Here's a question for the assembled luminaries reading this list: is
there any proof development environment other than Twelf in which one
routinely represents things like typing derivations, or evaluation
derivations, as explicit syntactic objects?

Another question, maybe directed at Jerome Vouillon: I know how to go
through a Twelf proof, and, clause by clause, transform it into a
series of lemmas, each of which is based on a rule induction of the
sort that one sees in POPL papers.  Each clause becomes one case of
such an induction.  The mapping is easy to explain, and in fact, many
proofs you have seen in papers written by CMUers recently have arisen
as just such translations of Twelf proofs.  Is there a similarly
clean, simple, line-by-line interpretation of the Vouillon solution? 
For example, just to pick a line at random, does the phrase

"simpl; intro H3; rewrite H; trivial; generalize H3; case (get_bound
e' X); simpl; trivial; intros; discriminate"

correspond to a proof step that one would usually see in a
pencil-and-paper rule induction?  Can someone (without finding the
particular place in the Vouillon solution from which this example was
drawn) tell me precisely what it means?  Or is it only comprehensible
in terms of the imperative effect it has on Coq's internal proof
search state at the moment it's invoked?  Can someone explain what the
effect of, say, reversing "trivial; intros" to "intros; trivial" would
be?

It may be that my example is unfair because I haven't given enough
context for the phrase to be understandable in isolation.  (In Twelf,
of course, one can't understand a clause without seeing the type
declarations for the syntax that's mentioned in it, and the type
declarations and modes of the relations used in it.  Presumably in Coq
one would at least need to see the definitions of the inductive types,
and such.)  In that case, I'd be interested to know how much context
is necessary to make the phrase sensible.

Kevin