The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Nov 8, 2007, at 1:22 PM, Moez A. Abdel-Gawad wrote:

> In my quest to learn Coq, I started playing with a personal  
> implementation of lambda calculus.

If you are seeking to implement lambda-calculus as is normally done  
"on paper," then it is worth noting that you have not defined capture- 
avoiding substitution.  For example, the following holds:

Lemma subs_can_capture :
  subs "x" (Abs "y" (Var "x")) (Var "y") = (Abs "y" (Var "y")).
Proof. reflexivity. Qed.

I'm not sure if you intended this behavior or not.


> It was also nice to know that there is an ongoing project that is  
> trying to solve this deficiency (which is a deficiency that exists,  
> it seems to me, in most semi-automated theorem provers in general,  
> not only in Isabelle and Coq).

Representing syntax with binding (e.g., the lambda calculus) and  
working with such representations is a well-known problem that has  
received considerable attention over the past years.  It takes some  
thought and care to be completely formal and correct about statements  
such as "by the Barendregt Variable Convention, we assume that ..."  
and actions such as causally renaming terms to alpha-equivalent  
ones.  For example, if you want to be able to rename an arbitrary  
term to an alpha-equivalent one and treat the two terms as equal,  
then you have to show that any function you apply to that term  
respects alpha-equivalence.

--Brian