[Prev][Next][Index][Thread]
Re: equational proof checker for lambda calculus?
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
Le samedi, 15 nov 2003, à 18:19 Europe/Paris, jhines@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