equational proof checker for lambda calculus?

Mitchell Wand <wand@ccs.neu.edu> · Wed, 19 Nov 2003 16:05:46 -0500

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

Yes, Greg Sullivan and I wrote something like that around 1993. We
called it MSTP (Mitch's Simple Theorem Prover).  The basic idea was to
allow simple rules, not just beta, and to check a proof using
alpha-matching (ie, pattern-matching that is aware of scoping and
alpha-conversion). 

We wrote a short paper about it, which was never published.  We
managed to prove some simple things with it, but we eventually decided
that it was not going to extend to the examples we wanted to do, so we
dropped it.

I've put up the directory at
http://www.ccs.neu.edu/home/wand/research/mstp .  It's in Scheme.

WYSISWYG. YMMV.  No warranties or Guarantees.  Good luck, though if
you're really interested I can try to help.

--Mitch Wand