[plt-scheme] lambda calculus

Yeap!!



On Aug 11, 2009, at 8:39 AM, Chris Stephenson wrote:

> 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ı