equational proof checker for lambda calculus?

Thorsten Altenkirch <txa@Cs.Nott.AC.UK> · Thu, 20 Nov 2003 21:39:46 +0000

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

When reasoning about programs you usually reason about total functions
(although frequently the intended domain is not expressible using
simple types) and then beta equality is decidable. Indeed proof tools
based on type theory such as COQ decide beta-equality automatically
and they also unfold functional definitions.

I personally find reasoning by induction (and coinduction) more
natural than reducing everything to equational reasoning (proof-by
calculation). Having said, this equational reasoning certainly has got
its place as well.

Cheers,
Thorsten

-- 
Dr. Thorsten Altenkirch		   phone : (+44) (0)115 84 66516
Lecturer			   http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT	   University of Nottingham