equational proof checker for lambda calculus?

jhines@haverford.edu · Sat, 15 Nov 2003 12:19:47 EST

[----- 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.

Am I correct in believing that, (though not usable in general), it could
be useful for (the homework for) those few lectures where one talks about 
programming in the pure lambda calculus (i.e. natural numbers, booleans,
pairs)?

In reading Paul Hudak's School of Expression, he seemed to imply that
this kind of proof (proof-by-calculation) is useful for programming in
Haskell, and he does not routinely use a proof checker.

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.

Thanks for any information you could send me.

Johnicholas Hines