|
![](/i/fill.gif) |
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
|
![](/i/fill.gif) |