equational proof checker for lambda calculus?

[Gérard Huet]

Le samedi, 15 nov 2003, à 18:19 Europe/Paris, jhines at haverford.edu a 
écrit :

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

The problem with looking at beta-reduction/expansion as a relation over 
terms is
that you lose the residual structure. You have coincidences like:
(\x.x (\x.x y))
= beta-reduce
(\x.x y)
indeed, but you lose the crucial information of which redex is reduced.
If you keep this information, like in
(\x.x (\x.x y))
= beta-reduce at occ (with the proper notion of occurrence as a path in 
the reduced term)
(\x.x y)
then you have a non-ambiguous notion, and the advantage is that you do 
not need a proof
checker anymore, it becomes an exercise in deterministic programming.
Furthermore, once you have it, you can easily write the iterator on all 
positions in
a term, and thus answer your original problem, which is an existential 
statement over
a finite domain. Thus no proof assistant needed.
You will find such programs, written in Objective Caml, at my site
http://pauillac.inria.fr/~huet/CCT/
Cheers
GH