[plt-scheme] lambda calculus

Matthias Felleisen wrote:
> 
> 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.
> 

But isn't it the case that even with de Bruijn indices the "problem"
does not go away? You still have to check one thing at every
substitution: if a term containing an instance free in the term (dB
number greater than its lexical depth in the term) is substituted into
another term and that instance is bound in some scope enclosing both the
substituted and substituted-into terms (again you can define that in
terms of dB number and lexical depth), then you have to do a trickyish
calculation to change the dB number for that instance so that it "works"
in its new position.

So, whether you rename or number, there is no free lunch.

-- 
Chris Stephenson

İstanbul Bilgi Üniversitesi
Bilgisayar Bilimleri Bölüm Başkanı