equational proof checker for lambda calculus?

Michael Norrish <Michael.Norrish@nicta.com.au> · Thu, 20 Nov 2003 09:39:58 +1100

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

jhines@haverford.edu writes:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

> Does there exist a simple proof checker for equational proofs
> with format something like this?

> ( (\x. (x x)) (\y. (y (\z. z))) )
> = beta-reduce
> ( (\x. (x (\y. y))) (\z. (z (\w. w))) )
> = beta-reduce
> ( (\x. (x (\y. y))) (\z. z) )
> = beta-reduce
> ( (\x. x) (\y.y) )
> = beta-expand
> ( (\x. (x x)) (\y.y) )

> The format would be something like a sequence of (closed?) lambda-terms,
> related one to the next by beta (or eta) reduction/expansion.

> I've read a paper by Michael Norrish ("Mechanising Hankin and
> Barendregt using the Gordon-Melham Axioms"), which discusses
> mechanising some much more sophisticated lambda-calculus
> proofs. This makes me think that I could do this kind of proof in
> HOL, but HOL is scary; I think I could write a checker more quickly
> than I could become comfortable in HOL.

There are two ways in which you could do this sort of thing with HOL.
One way would be to fire up an interactive session and use the general
support HOL has for doing interactive proof to get your goal out.  For
such a specialised application, this is not very desirable as the
end-user would have to learn HOL's proof methods.

A better solution would be to do some programming, and to create a
parser for the proof language you propose, and to then link this
front-end to HOL.  The developer has to do some proof-programming but
the end-user then doesn't need to interact with HOL at all.  HOL would
be linked as part of a standalone application that checked equational
proofs and did nothing else.

I admit HOL is scary, but there are two possible advantages to taking
this latter approach.  1. Soundess: you could be sure that if your
checker said a step was correct, it would be.  (Though you still have
to trust your parser.)  2. Extensibility: there's a lot else available
under HOL's hood, so that if you wanted to extend your reasoning to
cover other things, the system should be easy to adjust to allow
this. 

Incidentally, one of the features of the work I describe in the
article you mention is that I used a "name-carrying" model of the
lambda calculus.  If you were implementing the second approach above,
you wouldn't need to be translating to name-carrying terms however.
You could just as well translate to a model using de Bruijn indices.
Nor is HOL the only possible proof assistant for the job.  Mechanising
the equational theory with de Bruijn indices is not so difficult, so
I'd imagine most of the existing proof-assistants / theorem-proving
systems out there could do much the same things. 

If you're interested in having a go at this in HOL, please let me know
if I can be any help.

Regards,
Michael.