On 21-6-2009 20:00, Orchid XP v8 wrote:
> Darren New wrote:
>> when I read something like this...
>>
>> http://www.irregularwebcomic.net/
> 
> Why thank you. :-/
> 
> In a stunning turn of events, I was just in the middle of having a 
> conversation about whether assigning unique indicies to every variable 
> in a Lambda expression enables its reduction sequence to be computed 
> without name clashes. :-P
> 
There is alpha conversion to prevent that, but I guess you are talking 
about an implementation not the theory. ;)

I seem to remember that labelling just with the level of the nesting is 
enough. If you have unique identifiers throughout your program, that 
certainly works.

On a similar note, assigning unique indices to the lambdas gives an 
almost trivial way to prove that lambda calculus is Church-Rosser. At 
least I think so, I have never seen that in a paper, so there might be a 
complication that I missed.

Post a reply to this message