[plt-scheme] lambda calculus

On Aug 11, 2009, at 2:07 AM, Chris Stephenson wrote:

(Your student asks general questions, so he's getting general answers.)


> But Barendregt's trick of renaming all bound variables to have  
> different
> names from all free variables simplifies some proofs, but obscures the
> issue of scope for those who interested in Lambda calculus as a model
> for programming languages.

The phrase you're alluding to has been misunderstood by many many  
computer scientists. Due to copying it isn't enough to distinguish  
free/bound variables in the original term. You have to do so at every  
step of the reduction. Barendregt knows this as the Yellow book  
shows. Computer science papers seem to not understand this on  
occasion. So yes, you're right :-) Use de Bruijn indices.

-- Matthias