[Haskell-cafe] Slightly off-topic: Lambda calculus

[Brent Yorgey]

On Sun, Jun 21, 2009 at 07:48:30PM +0100, Andrew Coppin wrote:
> Andrew Coppin wrote:
>> Well anyway, the obvious thing to do is after each reduction, strip off 
>> all the variable indicies and rerun the labeller to assign new indicies. 
>> But does this solution work properly in general?
>
> No.
>
> Supposing some Lambda expression eventually reduces to, say,
>
>  \x1 -> \x2 -> x1 x2
>
> Now strip off all the indicies:
>
>  \x -> \x -> x x
>
> ...and recompute them...
>
>  \x1 -> \x2 -> x2 x2
>
> FAIL.
>
> To make it worth properly, I would have to (at least) make the renamer 
> respect any indicies which are already present. It's nontrivial, but 
> doable. Of course, the £1,643,264 question is... would it work even then?

I reiterate the pointers to reading material that I gave earlier.  A
lot of really smart people have spent a lot of time thinking about
this already; it's likely not worth any more of your time to try
figuring it out yourself.  (It's definitely worth some initial time
struggling with it, so that you can properly appreciate the
solutions---but it sounds like you've already done that!)

Briefly, the key operation is substitution---*while* doing a
substitution you have to somehow check that names aren't clashing, and
possibly rename some things if necessary (or if using de Bruijn
indices, you may need to shift some indices around while doing
substitution).  If you wait until *after* doing a substitution to fix
up the names, it's too late.  But don't take my word for it, go read
about it somewhere. =)

-Brent